7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
# 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
|