class UnificationTerm
Public Instance Methods
eql?(uni)
click to toggle source
# File lib/rover_prover/language/term/unification_term.rb, line 29 def eql?(uni) return false unless uni.is_a?(UnificationTerm) @name == uni.name end
free_unification_terms()
click to toggle source
# File lib/rover_prover/language/term/unification_term.rb, line 8 def free_unification_terms [self] end
free_variables()
click to toggle source
# File lib/rover_prover/language/term/unification_term.rb, line 4 def free_variables [] end
occurs(unification_term)
click to toggle source
# File lib/rover_prover/language/term/unification_term.rb, line 17 def occurs(unification_term) eql?(unification_term) end
replace(old, new)
click to toggle source
# File lib/rover_prover/language/term/unification_term.rb, line 12 def replace(old, new) return new if eql?(old) self end
set_instantiation_time(time)
click to toggle source
# File lib/rover_prover/language/term/unification_term.rb, line 21 def set_instantiation_time(time) @time = time end
to_s()
click to toggle source
# File lib/rover_prover/language/term/unification_term.rb, line 25 def to_s @name end
unify(term)
click to toggle source
# File lib/rover_prover/language/term/unification_term.rb, line 34 def unify(term) return nil if term.occurs(self) || term.time > @time { self => term } end