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