class Satre::Entails

A propositional logic ‘and’ value

Attributes

knowledge_base[R]
logical_consequence[R]

Public Class Methods

new(knowledge_base, logical_consequence) click to toggle source
# File lib/satre/formula/propositional_logic/entails.rb, line 11
def initialize(knowledge_base, logical_consequence)
  fail(ArgumentError, 'Argument must be a Formula') unless knowledge_base.is_a?(Formula)
  fail(ArgumentError, 'Argument must be a Formula') unless logical_consequence.is_a?(Formula)
  @knowledge_base = knowledge_base.dup.freeze
  @logical_consequence = logical_consequence.dup.freeze
end

Public Instance Methods

atoms() click to toggle source
# File lib/satre/formula/propositional_logic/entails.rb, line 36
def atoms
  atoms = knowledge_base.atoms + logical_consequence.atoms
  atoms.uniq || []
end
eval(*) click to toggle source
# File lib/satre/formula/propositional_logic/entails.rb, line 32
def eval(*)
  And.new(knowledge_base, Not.new(logical_consequence)).unsatifiable?
end
hold?(domain, func, predicate, valudation) click to toggle source
# File lib/satre/formula/propositional_logic/entails.rb, line 27
def hold?(domain, func, predicate, valudation)
  fail 'not implemented'
  #And.new(knowledge_base, Not.new(logical_consequence)).unsatifiable?
end
to_s() click to toggle source
# File lib/satre/formula/propositional_logic/entails.rb, line 18
def to_s
  "(#{knowledge_base} ⊨ #{logical_consequence})"
end
wellformed?(sig) click to toggle source

p |= q is wellformed if p and q are well-formed

# File lib/satre/formula/propositional_logic/entails.rb, line 23
def wellformed?(sig)
  knowledge_base.wellformed?(sig) && logical_consequence.wellformed?(sig)
end