class Satre::Formula
Public Instance Methods
<=>(other)
click to toggle source
# File lib/satre/formula/formula.rb, line 5 def <=>(other) self.to_s <=> other.to_s end
atoms()
click to toggle source
# File lib/satre/formula/formula.rb, line 9 def atoms fail 'abstract' end
entails?(other)
click to toggle source
# File lib/satre/formula/formula.rb, line 44 def entails?(other) And.new(self, Not.new(other)).unsatifiable? end
eval(_valudation)
click to toggle source
# File lib/satre/formula/formula.rb, line 28 def eval(_valudation) fail 'abstract' end
on_all_valuations?()
click to toggle source
# File lib/satre/formula/formula.rb, line 13 def on_all_valuations? valudation = Hash[self.atoms.map { |x| [x, true] }] truthtable = [valudation] valudation.length.times do |i| v = {} (valudation.length - i).times do |j| v = valudation.dup v[v.keys[j]] = ! v[v.keys[j]] truthtable << v end valudation = v end truthtable.all? { |v| self.eval(v) } end
satifiable?()
click to toggle source
# File lib/satre/formula/formula.rb, line 40 def satifiable? not unsatifiable? end
tautology?()
click to toggle source
# File lib/satre/formula/formula.rb, line 32 def tautology? on_all_valuations? end
unsatifiable?()
click to toggle source
# File lib/satre/formula/formula.rb, line 36 def unsatifiable? Not.new(self).tautology? end