class PropLogic::NotTerm
Public Class Methods
new(term)
click to toggle source
# File lib/prop_logic/not_term.rb, line 3 def initialize(term) @terms = [term].freeze @is_nnf = @terms[0].is_a?(Variable) @is_reduced = @is_nnf && ! (@terms[0].is_a?(Constant)) end
Public Instance Methods
nnf?()
click to toggle source
# File lib/prop_logic/not_term.rb, line 13 def nnf? @is_nnf end
reduce()
click to toggle source
# File lib/prop_logic/not_term.rb, line 37 def reduce return self if reduced? reduced_term = @terms[0].reduce case reduced_term when TrueConstant False when FalseConstant True else (~reduced_term).to_nnf end end
reduced?()
click to toggle source
# File lib/prop_logic/not_term.rb, line 33 def reduced? @is_reduced end
Also aliased as: cnf?
to_cnf()
click to toggle source
Calls superclass method
PropLogic::Term#to_cnf
# File lib/prop_logic/not_term.rb, line 50 def to_cnf if reduced? self else super end end
to_nnf()
click to toggle source
# File lib/prop_logic/not_term.rb, line 17 def to_nnf term = @terms[0] case term when NotTerm term.terms[0].to_nnf when Variable self when ThenTerm (~(term.to_nnf)).to_nnf when AndTerm all_or(*term.terms.map{|t| (~t).to_nnf}) when OrTerm all_and(*term.terms.map{|t| (~t).to_nnf}) end end
to_s(*)
click to toggle source
# File lib/prop_logic/not_term.rb, line 9 def to_s(*) "~" + @terms[0].to_s(true) end
tseitin(pool)
click to toggle source
# File lib/prop_logic/not_term.rb, line 58 def tseitin(pool) if nnf? self elsif @terms[0].is_a?(NotTerm) && @terms[0].terms[0].is_a(Variable) @terms[0].terms[0] else raise 'Non-NNF terms cannot be converted to Tseitin form.' + self.to_s end end