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