class Not

Attributes

formula[R]

Public Class Methods

new(formula) click to toggle source
# File lib/rover_prover/language/formula/not.rb, line 6
def initialize(formula)
  @formula = formula
end

Public Instance Methods

eql?(exp) click to toggle source
# File lib/rover_prover/language/formula/not.rb, line 35
def eql?(exp)
  return false unless exp.is_a?(Not)
  @formula.eql?(exp.formula)
end
free_unification_terms() click to toggle source
# File lib/rover_prover/language/formula/not.rb, line 14
def free_unification_terms
  @formula.free_unification_terms
end
free_variables() click to toggle source
# File lib/rover_prover/language/formula/not.rb, line 10
def free_variables
  @formula.free_variables
end
occurs(unification_term) click to toggle source
# File lib/rover_prover/language/formula/not.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/not.rb, line 18
def replace(old, new)
  return new if eql?(old)
  Not.new(@formula.replace(old, new))
end
set_instantiation_time(time) click to toggle source
# File lib/rover_prover/language/formula/not.rb, line 23
def set_instantiation_time(time)
  @formula.set_instantiation_time(time)
end
to_s() click to toggle source
# File lib/rover_prover/language/formula/not.rb, line 31
def to_s
  "¬#{@formula.to_s}"
end