Class: ForAll
- Defined in:
- lib/rover_prover/language/formula/for_all.rb
Instance Attribute Summary collapse
-
#formula ⇒ Object
readonly
Returns the value of attribute formula.
-
#variable ⇒ Object
readonly
Returns the value of attribute variable.
Instance Method Summary collapse
- #eql?(exp) ⇒ Boolean
- #free_unification_terms ⇒ Object
- #free_variables ⇒ Object
-
#initialize(variable, formula) ⇒ ForAll
constructor
A new instance of ForAll.
- #occurs(unification_term) ⇒ Object
- #replace(old, new) ⇒ Object
- #set_instantiation_time(time) ⇒ Object
- #to_s ⇒ Object
Methods included from Expression
Constructor Details
#initialize(variable, formula) ⇒ ForAll
Returns a new instance of ForAll.
6 7 8 9 |
# File 'lib/rover_prover/language/formula/for_all.rb', line 6 def initialize(variable, formula) @variable = variable @formula = formula end |
Instance Attribute Details
#formula ⇒ Object (readonly)
Returns the value of attribute formula.
4 5 6 |
# File 'lib/rover_prover/language/formula/for_all.rb', line 4 def formula @formula end |
#variable ⇒ Object (readonly)
Returns the value of attribute variable.
4 5 6 |
# File 'lib/rover_prover/language/formula/for_all.rb', line 4 def variable @variable end |
Instance Method Details
#eql?(exp) ⇒ Boolean
40 41 42 43 |
# 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 ⇒ Object
15 16 17 |
# File 'lib/rover_prover/language/formula/for_all.rb', line 15 def free_unification_terms @formula.free_unification_terms end |
#free_variables ⇒ Object
11 12 13 |
# 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) ⇒ Object
27 28 29 |
# File 'lib/rover_prover/language/formula/for_all.rb', line 27 def occurs(unification_term) @formula.occurs(unification_term) end |
#replace(old, new) ⇒ Object
19 20 21 22 23 24 25 |
# 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) ⇒ Object
31 32 33 34 |
# 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 ⇒ Object
36 37 38 |
# File 'lib/rover_prover/language/formula/for_all.rb', line 36 def to_s "(∀#{@variable.to_s}. #{@formula.to_s})" end |