class ForAll
Attributes
formula[R]
variable[R]
Public Class Methods
new(variable, formula)
click to toggle source
# File lib/rover_prover/language/formula/for_all.rb, line 6 def initialize(variable, formula) @variable = variable @formula = formula end
Public Instance Methods
eql?(exp)
click to toggle source
# File lib/rover_prover/language/formula/for_all.rb, line 40 def eql?(exp) return false unless exp.is_a?(ForAll) @variable.eql?(exp.variable) && @formula.eql?(exp.formula) end
free_unification_terms()
click to toggle source
# File lib/rover_prover/language/formula/for_all.rb, line 15 def free_unification_terms @formula.free_unification_terms end
free_variables()
click to toggle source
# File lib/rover_prover/language/formula/for_all.rb, line 11 def free_variables @formula.free_variables.reject{ |var| var.eql?(@variable) } end
occurs(unification_term)
click to toggle source
# File lib/rover_prover/language/formula/for_all.rb, line 27 def occurs(unification_term) @formula.occurs(unification_term) end
replace(old, new)
click to toggle source
# File lib/rover_prover/language/formula/for_all.rb, line 19 def replace(old, new) return new if eql?(old) ForAll.new( @variable.replace(old, new), @formula.replace(old, new) ) end
set_instantiation_time(time)
click to toggle source
# File lib/rover_prover/language/formula/for_all.rb, line 31 def set_instantiation_time(time) @variable.set_instantiation_time(time) @formula.set_instantiation_time(time) end
to_s()
click to toggle source
# File lib/rover_prover/language/formula/for_all.rb, line 36 def to_s "(∀#{@variable.to_s}. #{@formula.to_s})" end