Method List
-
#deepen Sequent
-
#depth Sequent
-
#derivation_left Prover
-
#derivation_left_and Prover
-
#derivation_left_for_all Prover
-
#derivation_left_implies Prover
-
#derivation_left_not Prover
-
#derivation_left_or Prover
-
#derivation_right Prover
-
#derivation_right_and Prover
-
#derivation_right_for_all Prover
-
#derivation_right_implies Prover
-
#derivation_right_not Prover
-
#derivation_right_or Prover
-
#eql? Implies
-
#eql? Expression
-
#eql? ForAll
-
#eql? Variable
-
#eql? And
-
#eql? Predicate
-
#eql? Or
-
#eql? Function
-
#eql? Sequent
-
#eql? ThereExists
-
#eql? Not
-
#eql? UnificationTerm
-
#formula Not
-
#formula ForAll
-
#formula Remove
-
#formula Axiom
-
#formula ThereExists
-
#formula Lemma
-
#formula_a Implies
-
#formula_a Or
-
#formula_a And
-
#formula_b Or
-
#formula_b And
-
#formula_b Implies
-
#free_unification_terms Implies
-
#free_unification_terms UnificationTerm
-
#free_unification_terms Predicate
-
#free_unification_terms Expression
-
#free_unification_terms Function
-
#free_unification_terms Variable
-
#free_unification_terms ThereExists
-
#free_unification_terms ForAll
-
#free_unification_terms Sequent
-
#free_variables Not
-
#free_variables Implies
-
#free_variables And
-
#free_variables Sequent
-
#free_variables Function
-
#free_variables ThereExists
-
#free_variables Variable
-
#free_variables Expression
-
#free_variables UnificationTerm
-
#free_variables Predicate
-
#free_variables ForAll
-
#get_unifiable_pairs Sequent
-
#get_variable_name Sequent
-
#initialize Or
-
#initialize Remove
-
#initialize Predicate
-
#initialize Axiom
-
#initialize Lemma
-
#initialize Not
-
#initialize Function
-
#initialize Sequent
-
#initialize Implies
-
#initialize ThereExists
-
#initialize ForAll
-
#initialize Term
-
#initialize And
-
#left Sequent
-
#left_add Sequent
-
#left_formula Sequent
-
#left_get_depth Sequent
-
#left_remove Sequent
-
#left_set_depth Sequent
-
#name Predicate
-
#name Term
-
#occurs Expression
-
#occurs ForAll
-
#occurs Implies
-
#occurs ThereExists
-
#occurs Or
-
#occurs Variable
-
#occurs UnificationTerm
-
#occurs Not
-
#occurs And
-
#occurs Predicate
-
#occurs Function
-
#prove Prover
-
#prove_formula Prover
-
#replace Or
-
#replace Expression
-
#replace Not
-
#replace Function
-
#replace Variable
-
#replace ForAll
-
#replace Implies
-
#replace And
-
#replace ThereExists
-
#replace Predicate
-
#replace UnificationTerm
-
#right Sequent
-
#right_add Sequent
-
#right_formula Sequent
-
#right_get_depth Sequent
-
#right_remove Sequent
-
#right_set_depth Sequent
-
run RoverProver::Main
-
#set_default_instantiation_time Sequent
-
#set_instantiation_time Variable
-
#set_instantiation_time Function
-
#set_instantiation_time Expression
-
#set_instantiation_time UnificationTerm
-
#set_instantiation_time Predicate
-
#set_instantiation_time ThereExists
-
#set_instantiation_time ForAll
-
#set_instantiation_time Implies
-
#siblings Sequent
-
#terms Function
-
#terms Predicate
-
#time Term
-
#to_s Variable
-
#to_s Function
-
#to_s Not
-
#to_s And
-
#to_s Or
-
#to_s ForAll
-
#to_s Expression
-
#to_s Sequent
-
#to_s UnificationTerm
-
#to_s Predicate
-
#to_s Implies
-
#to_s ThereExists
-
#trivial? Sequent
-
#unify Function
-
#unify Variable
-
#unify Expression
-
#unify UnificationTerm
-
#unify Predicate
-
#unify_all Unifier
-
#unify_list Unifier
-
#variable ForAll
-
#variable ThereExists