module RoverProver::Main
Public Class Methods
run()
click to toggle source
# File lib/rover_prover.rb, line 7 def self.run message = <<~MSG Rover: First-Order Logic Theorem Prover 2019 Koki Ryu 2014 Stephan Boyer Terms: x (variable) f(term, ...) (function) Formulae: P(term) (predicate) not P (complement) P or Q (disjunction) P and Q (conjunction) P implies Q (implication) forall x. P (universal quantification) exists x. P (existential quantification) Enter formulae at the prompt. The following commands are also available for manipulating axioms: axioms (list axioms) lemmas (list lemmas) axiom <formula> (add an axiom) lemma <formula> (prove and add a lemma) remove <formula> (remove an axiom or lemma) reset (remove all axioms and lemmas) Enter 'exit' command to exit the prompt. MSG puts message axioms = [] lemmas = {} prover = Prover.new while true do begin print("\nRover> ") cmd = gets if cmd.nil? puts 'Bye' return end cmd_token = RoverParser.parse(RoverLexer.lex(cmd)) if cmd_token.is_a?(Axioms) axioms.each { |axiom| puts axiom.to_s } elsif cmd_token.is_a?(Lemmas) lemmas.keys.each { |lemma| puts lemma.to_s } elsif cmd_token.is_a?(Axiom) axioms.push(cmd_token.formula) puts "Axiom added: #{cmd_token.formula.to_s}" elsif cmd_token.is_a?(Lemma) result = prover.prove_formula(axioms | lemmas.keys, cmd_token.formula) if result lemmas[cmd_token.formula] = axioms.dup puts "Lemma proven: #{cmd_token.formula.to_s}" else puts "Lemma unprovable: #{cmd_token.formula.to_s}" end elsif cmd_token.is_a?(Remove) result = axioms.reject! { |axiom| axiom.eql?(cmd_token.formula) } if result.nil? puts "Not an axiom: #{cmd_token.formula.to_s}" else puts "Axiom removed: #{cmd_token.formula.to_s}" bad_lemmas = lemmas.keys.select { |key| lemmas[key].any?{ |lemma| lemma.eql?(cmd_token.formula) } } puts "Dependent axioms are also removed:" bad_lemmas.each do |lemma| lemmas.delete(lemma) puts lemma.to_s end end elsif cmd_token.is_a?(Reset) axioms = [] lemmas = {} elsif cmd_token.is_a?(Exit) puts 'Bye' return else result = prover.prove_formula(axioms | lemmas.keys, cmd_token) if result puts "Formula proven: #{cmd_token.to_s}" else puts "Formula unprovable: #{cmd_token.to_s}" end end rescue Interrupt next rescue RLTK::LexingError => e puts "Error: Unable to parse #{e.remainder}" next rescue RLTK::NotInLanguage puts 'Error: Invalid command' next end end end