Table of Contents - rover_prover-0.1.1 Documentation
Classes and Modules
- And
- Axiom
- Axioms
- Exit
- Expression
- ForAll
- Formula
- Function
- Implies
- Lemma
- Lemmas
- Not
- Or
- Predicate
- Prover
- Remove
- Reset
- RoverLexer
- RoverParser
- RoverProver
- RoverProver::Main
- Sequent
- Term
- ThereExists
- UnificationTerm
- Unifier
- Variable
Methods
- ::new — And
- ::new — ForAll
- ::new — Implies
- ::new — Not
- ::new — Or
- ::new — Predicate
- ::new — ThereExists
- ::new — Sequent
- ::new — Term
- ::new — Function
- ::new — Axiom
- ::new — Lemma
- ::new — Remove
- ::run — RoverProver::Main
- #apply_left? — Prover
- #deepen — 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_left_there_exists — 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
- #derivation_right_there_exists — Prover
- #eql? — And
- #eql? — ForAll
- #eql? — Implies
- #eql? — Not
- #eql? — Or
- #eql? — Predicate
- #eql? — ThereExists
- #eql? — Sequent
- #eql? — Function
- #eql? — UnificationTerm
- #eql? — Variable
- #eql? — Expression
- #free_unification_terms — And
- #free_unification_terms — ForAll
- #free_unification_terms — Implies
- #free_unification_terms — Not
- #free_unification_terms — Or
- #free_unification_terms — Predicate
- #free_unification_terms — ThereExists
- #free_unification_terms — Sequent
- #free_unification_terms — Function
- #free_unification_terms — UnificationTerm
- #free_unification_terms — Variable
- #free_unification_terms — Expression
- #free_variables — And
- #free_variables — ForAll
- #free_variables — Implies
- #free_variables — Not
- #free_variables — Or
- #free_variables — Predicate
- #free_variables — ThereExists
- #free_variables — Sequent
- #free_variables — Function
- #free_variables — UnificationTerm
- #free_variables — Variable
- #free_variables — Expression
- #get_unifiable_pairs — Sequent
- #get_variable_name — Sequent
- #include? — Sequent
- #left_add — Sequent
- #left_formula — Sequent
- #left_get_depth — Sequent
- #left_remove — Sequent
- #left_set_depth — Sequent
- #occurs — And
- #occurs — ForAll
- #occurs — Implies
- #occurs — Not
- #occurs — Or
- #occurs — Predicate
- #occurs — ThereExists
- #occurs — Function
- #occurs — UnificationTerm
- #occurs — Variable
- #occurs — Expression
- #prove — Prover
- #prove_formula — Prover
- #replace — And
- #replace — ForAll
- #replace — Implies
- #replace — Not
- #replace — Or
- #replace — Predicate
- #replace — ThereExists
- #replace — Function
- #replace — UnificationTerm
- #replace — Variable
- #replace — Expression
- #right_add — Sequent
- #right_formula — Sequent
- #right_get_depth — Sequent
- #right_remove — Sequent
- #right_set_depth — Sequent
- #set_default_instantiation_time — Sequent
- #set_instantiation_time — And
- #set_instantiation_time — ForAll
- #set_instantiation_time — Implies
- #set_instantiation_time — Not
- #set_instantiation_time — Or
- #set_instantiation_time — Predicate
- #set_instantiation_time — ThereExists
- #set_instantiation_time — Function
- #set_instantiation_time — UnificationTerm
- #set_instantiation_time — Variable
- #set_instantiation_time — Expression
- #to_s — And
- #to_s — ForAll
- #to_s — Implies
- #to_s — Not
- #to_s — Or
- #to_s — Predicate
- #to_s — ThereExists
- #to_s — Sequent
- #to_s — Function
- #to_s — UnificationTerm
- #to_s — Variable
- #to_s — Expression
- #trivial? — Sequent
- #unify — Predicate
- #unify — Function
- #unify — UnificationTerm
- #unify — Variable
- #unify — Expression
- #unify_all — Unifier
- #unify_list — Unifier