class ThereExists
Attributes
formula[R]
variable[R]
Public Class Methods
new(variable, formula)
click to toggle source
# File lib/rover_prover/language/formula/there_exists.rb, line 4 def initialize(variable, formula) @variable = variable @formula = formula end
Public Instance Methods
eql?(exp)
click to toggle source
# File lib/rover_prover/language/formula/there_exists.rb, line 38 def eql?(exp) return false unless exp.is_a?(ThereExists) @variable.eql?(exp.variable) && @formula.eql?(exp.formula) end
free_unification_terms()
click to toggle source
# File lib/rover_prover/language/formula/there_exists.rb, line 13 def free_unification_terms @formula.free_unification_terms end
free_variables()
click to toggle source
# File lib/rover_prover/language/formula/there_exists.rb, line 9 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/there_exists.rb, line 25 def occurs(unification_term) @formula.occurs(unification_term) end
replace(old, new)
click to toggle source
# File lib/rover_prover/language/formula/there_exists.rb, line 17 def replace(old, new) return new if eql?(old) ThereExists.new( @variable.replace(old, new), @formula.replace(old, new) ) end
set_instantiation_time(time)
click to toggle source
# File lib/rover_prover/language/formula/there_exists.rb, line 29 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/there_exists.rb, line 34 def to_s "(∃#{@variable.to_s}. #{@formula.to_s})" end