Propositional logic and entailment by model checking

The concept

A knowledge-based agent stores what it knows as sentences in a formal language and uses inference to derive new sentences. Propositional logic is the simplest such language. Its sentences are built from proposition symbols, such as rain and wet, with the connectives not, and, or, implies, and if and only if. The meaning of a sentence is given by its truth value in each model, where a model assigns true or false to every symbol.

Entailment is the central relation. A knowledge base KB entails a sentence α, written KB ⊨ α, when α is true in every model in which KB is true. The simplest way to check it is model checking: enumerate all 2ⁿ assignments to the n symbols and test that no model makes KB true and α false. This procedure is sound, because it only reports entailments that really hold, and complete, because it reports all of them. Its cost grows exponentially, which is why practical solvers use SAT algorithms such as DPLL and CDCL even though deciding satisfiability is NP-complete in general.

The example knowledge base says that rain implies wet and that it is raining. It has exactly 2 models, one for each value of the unmentioned symbol cold. It entails wet, which is modus ponens, but it does not entail cold. A contradictory knowledge base has no models at all, so it entails every sentence, vacuously. That last case is why consistency of a knowledge base matters.

Code example

from itertools import product


def implies(a, b):
    return (not a) or b


def models_of(symbols, formula):
    assignments = (dict(zip(symbols, values)) for values in product([False, True], repeat=len(symbols)))
    return [model for model in assignments if formula(model)]


def entails(symbols, kb, query):
    return all(query(model) for model in models_of(symbols, kb))


symbols = ["rain", "wet", "cold"]
kb = lambda m: implies(m["rain"], m["wet"]) and m["rain"]
print(len(models_of(symbols, kb)))
print(entails(symbols, kb, lambda m: m["wet"]))
print(entails(symbols, kb, lambda m: m["cold"]))
print(entails(symbols, lambda m: False, lambda m: m["cold"]))

2
True
False
True

Follow the code

Open the walkthrough to inspect the example one step at a time.

—

2

2
True

2
True
False

2
True
False
True

Behind the scenes

Cost and common mistakes

Time is O(2ⁿ · |KB|) for n symbols. SAT solvers use search with clause learning and are far faster on real instances, though the worst case remains exponential.

• Entailment is about every model of KB, not about a single scenario. A conclusion that is merely possible is not entailed.
• Model checking costs 2ⁿ evaluations, so it is only practical for small numbers of symbols.
• In logic, 'if a then b' (implication) is true whenever a is false. It does not claim a causes b.

Try it yourself

Does the knowledge base entail the sentence 'rain or cold'?

Further reading

• Artificial Intelligence: A Modern Approach (Russell and Norvig), 4th edition (external)
• Knowledge Representation and Reasoning (Brachman and Levesque) (external)