class Prover
Public Instance Methods
derivation_left(old, left)
click to toggle source
# File lib/rover_prover/prover/prover.rb, line 61 def derivation_left(old, left) return derivation_left_not(old, left) if left.is_a?(Not) return derivation_left_and(old, left) if left.is_a?(And) return derivation_left_or(old, left) if left.is_a?(Or) return derivation_left_implies(old, left) if left.is_a?(Implies) return derivation_left_for_all(old, left) if left.is_a?(ForAll) return derivation_left_there_exists(old, left) if left.is_a?(ThereExists) [] end
derivation_left_and(sequent, left)
click to toggle source
# File lib/rover_prover/prover/prover.rb, line 92 def derivation_left_and(sequent, left) new = sequent.deepen new.left_remove(left) left_depth = sequent.left_get_depth(left) new.left_add(left.formula_a) new.left_set_depth(left.formula_a, left_depth + 1) new.left_add(left.formula_b) new.left_set_depth(left.formula_b, left_depth + 1) unless new.siblings.nil? new.siblings.push(new) end [new] end
derivation_left_for_all(sequent, left)
click to toggle source
# File lib/rover_prover/prover/prover.rb, line 144 def derivation_left_for_all(sequent, left) new = sequent.deepen(enable_siblings: true) left_depth = sequent.left_get_depth(left) new.left_set_depth(left, left_depth + 1) t = UnificationTerm.new(sequent.get_variable_name('t')) t.set_instantiation_time(sequent.depth + 1) formula = left.formula.replace( left.variable, t ) unless new.left.include?(formula) new.left_add(formula) new.left_set_depth(formula, left_depth + 1) end unless new.siblings.nil? new.siblings.push(new) end [new] end
derivation_left_implies(sequent, left)
click to toggle source
# File lib/rover_prover/prover/prover.rb, line 125 def derivation_left_implies(sequent, left) new_a = sequent.deepen new_b = sequent.deepen new_a.left_remove(left) new_b.left_remove(left) left_depth = sequent.left_get_depth(left) new_a.right_add(left.formula_a) new_a.right_set_depth(left.formula_a, left_depth + 1) new_b.left_add(left.formula_b) new_b.left_set_depth(left.formula_b, left_depth + 1) unless new_a.siblings.nil? new_a.siblings.push(new_a) end unless new_b.siblings.nil? new_b.siblings.push(new_b) end [new_a, new_b] end
derivation_left_not(sequent, left)
click to toggle source
# File lib/rover_prover/prover/prover.rb, line 81 def derivation_left_not(sequent, left) new = sequent.deepen new.left_remove(left) new.right_add(left.formula) new.right_set_depth(left.formula, (sequent.left_get_depth(left) + 1)) unless new.siblings.nil? new.siblings.push(new) end [new] end
derivation_left_or(sequent, left)
click to toggle source
# File lib/rover_prover/prover/prover.rb, line 106 def derivation_left_or(sequent, left) new_a = sequent.deepen new_b = sequent.deepen new_a.left_remove(left) new_b.left_remove(left) left_depth = sequent.left_get_depth(left) new_a.left_add(left.formula_a) new_a.left_set_depth(left.formula_a, left_depth + 1) new_b.left_add(left.formula_b) new_b.left_set_depth(left.formula_b, left_depth + 1) unless new_a.siblings.nil? new_a.siblings.push(new_a) end unless new_b.siblings.nil? new_b.siblings.push(new_b) end [new_a, new_b] end
derivation_left_there_exists(sequent, left)
click to toggle source
# File lib/rover_prover/prover/prover.rb, line 164 def derivation_left_there_exists(sequent, left) new = sequent.deepen new.left_remove(left) left_depth = sequent.left_get_depth(left) variable = Variable.new(sequent.get_variable_name('v')) variable.set_instantiation_time(sequent.depth + 1) formula = left.formula.replace(left.variable, variable) new.left_add(formula) new.left_set_depth(formula, left_depth + 1) unless new.siblings.nil? new.siblings.push(new) end [new] end
derivation_right(old, right)
click to toggle source
# File lib/rover_prover/prover/prover.rb, line 71 def derivation_right(old, right) return derivation_right_not(old, right) if right.is_a?(Not) return derivation_right_and(old, right) if right.is_a?(And) return derivation_right_or(old, right) if right.is_a?(Or) return derivation_right_implies(old, right) if right.is_a?(Implies) return derivation_right_for_all(old, right) if right.is_a?(ForAll) return derivation_right_there_exists(old, right) if right.is_a?(ThereExists) [] end
derivation_right_and(sequent, right)
click to toggle source
# File lib/rover_prover/prover/prover.rb, line 190 def derivation_right_and(sequent, right) new_a = sequent.deepen new_b = sequent.deepen new_a.right_remove(right) new_b.right_remove(right) right_depth = sequent.right_get_depth(right) new_a.right_add(right.formula_a) new_a.right_set_depth(right.formula_a, right_depth + 1) new_b.right_add(right.formula_b) new_b.right_set_depth(right.formula_b, right_depth + 1) unless new_a.siblings.nil? new_a.siblings.push(new_a) end unless new_b.siblings.nil? new_b.siblings.push(new_b) end [new_a, new_b] end
derivation_right_for_all(sequent, right)
click to toggle source
# File lib/rover_prover/prover/prover.rb, line 237 def derivation_right_for_all(sequent, right) new = sequent.deepen new.right_remove(right) right_depth = sequent.right_get_depth(right) variable = Variable.new(sequent.get_variable_name('v')) variable.set_instantiation_time(sequent.depth + 1) formula = right.formula.replace(right.variable, variable) new.right_add(formula) new.right_set_depth(formula, right_depth + 1) unless new.siblings.nil? new.siblings.push(new) end [new] end
derivation_right_implies(sequent, right)
click to toggle source
# File lib/rover_prover/prover/prover.rb, line 223 def derivation_right_implies(sequent, right) new = sequent.deepen new.right_remove(right) right_depth = sequent.right_get_depth(right) new.left_add(right.formula_a) new.left_set_depth(right.formula_a, right_depth + 1) new.right_add(right.formula_b) new.right_set_depth(right.formula_b, right_depth + 1) unless new.siblings.nil? new.siblings.push(new) end [new] end
derivation_right_not(sequent, right)
click to toggle source
# File lib/rover_prover/prover/prover.rb, line 179 def derivation_right_not(sequent, right) new = sequent.deepen new.right_remove(right) new.left_add(right.formula) new.left_set_depth(right.formula, (sequent.right_get_depth(right) + 1)) unless new.siblings.nil? new.siblings.push(new) end [new] end
derivation_right_or(sequent, right)
click to toggle source
# File lib/rover_prover/prover/prover.rb, line 209 def derivation_right_or(sequent, right) new = sequent.deepen new.right_remove(right) right_depth = sequent.right_get_depth(right) new.right_add(right.formula_a) new.right_set_depth(right.formula_a, right_depth + 1) new.right_add(right.formula_b) new.right_set_depth(right.formula_b, right_depth + 1) unless new.siblings.nil? new.siblings.push(new) end [new] end
derivation_right_there_exists(sequent, right)
click to toggle source
# File lib/rover_prover/prover/prover.rb, line 252 def derivation_right_there_exists(sequent, right) new = sequent.deepen(enable_siblings: true) right_depth = sequent.right_get_depth(right) new.right_set_depth(right, right_depth + 1) t = UnificationTerm.new(sequent.get_variable_name('t')) t.set_instantiation_time(sequent.depth + 1) formula = right.formula.replace( right.variable, t ) unless new.right.include?(formula) new.right_add(formula) end new.right_set_depth(formula, right_depth + 1) unless new.siblings.nil? new.siblings.push(new) end [new] end
prove(sequent)
click to toggle source
# File lib/rover_prover/prover/prover.rb, line 16 def prove(sequent) sequent.set_default_instantiation_time(0) unifier = Unifier.new frontier = [sequent] proven = [] while true do frontier = frontier - proven old = frontier.pop break if old.nil? puts "#{old.depth}. #{old.to_s}" if old.trivial? proven.push(old) next end unless old.siblings.nil? pairs_list = old.siblings.map(&:get_unifiable_pairs) if pairs_list.all? { |list| !list.empty? } subst = unifier.unify_all(pairs_list) unless subst.nil? subst.each { |k, v| puts "#{k.to_s} = #{v.to_s}" } proven = proven | old.siblings frontier = frontier - proven next end else old.siblings.delete(old) end end left = old.left_formula right = old.right_formula return false if left.nil? && right.nil? if apply_left?(old, left, right) frontier.push(*derivation_left(old, left)) else frontier.push(*derivation_right(old, right)) end end true end
prove_formula(axioms, formula)
click to toggle source
# File lib/rover_prover/prover/prover.rb, line 5 def prove_formula(axioms, formula) prove( Sequent.new( axioms, [formula], nil, 0 ) ) end
Private Instance Methods
apply_left?(sequent, left, right)
click to toggle source
# File lib/rover_prover/prover/prover.rb, line 273 def apply_left?(sequent, left, right) return true if right.nil? return false if left.nil? sequent.right_get_depth(right) > sequent.left_get_depth(left) end