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