Propositional Automated Reasoning

A knowledge base stores sentences; an inference algorithm answers a query using them. The central task is to decide whether every model of the knowledge base satisfies the query. This note follows FIT3080’s progression through model checking, Horn clauses, chaining, and resolution refutation, then adds a small SAT-solving bridge [1][1] Monash, “FIT3080 Artificial Intelligence: Logic, Inference Algorithms, and First Order Logic, Parts I and II,” 2025. Course lecture materials, Semester 2. Part II reading list: AIMA 4th ed., Sections 7.1--7.5, 8.1--8.3, 9.1, 9.2, 9.5., [2][2] S. Russell and P. Norvig, Artificial Intelligence: A Modern Approach, 4th ed. Pearson, 2020.. Read Formal Logic and Natural Deduction first for the distinction between semantic consequence and syntactic derivation.

Throughout this note, the knowledge base $K$ is finite and propositional. When writing $K\land\neg q$, we mean the conjunction of all its sentences with the negated query. The finite propositional restriction is what makes the exhaustive procedures below terminate; it must not be silently transferred to unrestricted first-order logic.

Entailment as a search for a counterexample

The key reduction is

$$K\models q \quad\Longleftrightarrow\quad K\land\neg q\text{ is unsatisfiable}.$$

A satisfying assignment for the right-hand formula is exactly a model of $K$ that falsifies $q$. It refutes the entailment, not necessarily the query in every model. Conversely, proving the formula unsatisfiable rules out every countermodel.

For $n$ propositional variables, truth-table entailment enumerates $2^n$ assignments. For each, evaluate all premises; if they hold, check the query. Return “not entailed” with a countermodel as soon as one is found. If all assignments have been checked without a countermodel, return “entailed.” Evaluation is mechanical, but the number of assignments grows exponentially.

ExampleNot entailed does not mean false

Let $K=\{A\to B\}$ and query $B$. The assignment $A=\mathrm F,B=\mathrm F$ is a countermodel, so $K$ does not entail $B$. But $A=\mathrm T,B=\mathrm T$ also satisfies $K$, so $K$ does not entail $\neg B$ either. The available information leaves the answer undetermined.

A contradictory $K$ entails every query in classical logic. Before interpreting a positive answer as meaningful domain knowledge, distinguish “the query follows from consistent premises” from “the premises have no model.” Checking satisfiability of $K$ separately makes that distinction explicit.

Clauses, CNF, and the goal of a transformation

A literal is an atom or its negation. A clause is a disjunction of literals; CNF is a conjunction of clauses. A clause set represents that conjunction. The empty clause $\square$ is false, whereas the empty clause set is true: an empty disjunction has no successful alternative, and an empty conjunction imposes no constraint.

To obtain an equivalent CNF, remove implications and biconditionals, push negations inward, then distribute disjunction over conjunction. For example,

$$A\to(B\land C) \equiv (\neg A\lor B)\land(\neg A\lor C).$$

The order matters conceptually: CNF is a representation suitable for inference, not a claim that the expression is minimal. Direct distribution can make a formula exponentially larger. SAT encodings often introduce fresh variables with defining clauses to preserve satisfiability efficiently. Such an encoding is equisatisfiable with the original formula, but need not be equivalent as a formula over the enlarged variable set.

ExampleA fresh variable needs its defining clauses

Introduce $z$ to represent $A\land B$. The definition $z\leftrightarrow(A\land B)$ is encoded by

$$(\neg z\lor A)\land(\neg z\lor B) \land(z\lor\neg A\lor\neg B).$$

To assert that this represented formula is true, also require $z$. The definition alone only connects $z$ to the inputs; it does not force the represented expression to hold.

Definite clauses and Horn clauses

A Horn clause contains at most one positive literal. A definite clause contains exactly one, and can be written as a rule with a conjunction of positive atoms as its body and one positive atom as its head:

$$\neg A\lor\neg B\lor C \equiv (A\land B)\to C.$$

A fact $A$ is a definite clause with an empty body. A Horn clause with no positive literal expresses a constraint, such as $A\land B\to\bot$. The simple chaining algorithms below first concern finite propositional definite-clause knowledge bases and positive atomic queries. General Horn satisfiability additionally checks whether any constraint body becomes true.

Use the following original running example:

$$K=\{A,B,\ (A\land B)\to C,\ C\to D,\ (D\land A)\to E\}.$$

The query is $E$. All rules are implications, not equivalences: knowing $C$ does not justify inferring $A$ or $B$ by reversing the first rule.

Forward chaining: facts trigger rules

Forward chaining starts from facts and repeatedly adds the head of a rule whose body has been established. In the example, $A,B$ enable $C$, which enables $D$, and then $D,A$ enable $E$. A fixed point is reached when no new atom can be added.

Algorithm 1 Forward chaining for a finite definite-clause KB

1:procedure ForwardChain(Facts, Rules, q)

2:$Known \gets Facts$

3:while true do

4:if $q \in Known$ then

5:return true

6:end if

7:$Added \gets \emptyset$

8:for all $(Body \to Head) \in Rules$ do

9:if $Body \subseteq Known$ then

10:$Added \gets Added \cup \{Head\}$

11:end if

12:end for

13:$Added \gets Added \setminus Known$

14:if $Added = \emptyset$ then

15:return false

16:end if

17:$Known \gets Known \cup Added$

18:end while

19:end procedure

This deliberately simple version may scan the rules repeatedly. The usual agenda implementation stores, for each rule, the number of unmet body atoms and indexes which rules mention each atom. Processing each newly derived atom once then gives linear-time propagation in the total number of literal occurrences, plus initialization. That bound describes the indexed implementation, not every implementation of the pseudocode.

Each addition is sound by modus ponens. At termination, the derived set is the least model of the definite-clause theory: every model must contain the initial facts and every consequence added from them; the closed set itself satisfies every rule. Therefore a positive atom absent from that set is not entailed. Absence still does not mean its negation is entailed.

Backward chaining: a query generates subgoals

Backward chaining starts with $E$. Its rule requires $D$ and $A$; proving $D$ requires $C$; proving $C$ requires $A$ and $B$, which are facts. A rule body is an AND requirement, while multiple rules with the same head provide OR alternatives. All body goals of one successful alternative must be solved.

A naive depth-first implementation can loop, for example with rules $A\to B$ and $B\to A$. Repeated goals need cycle handling, and shared subgoals benefit from tabling. A goal blocked on the current recursion stack must not be permanently cached as globally false: another rule or later fact may establish it. Finite propositional tabling with fixed-point propagation, or a suitable complete search, can recover all definite-clause consequences. Completeness of the rule system does not make every search order complete.

Forward chaining is useful when many consequences or repeated queries matter; backward chaining can avoid deriving facts irrelevant to a particular query. Neither direction is universally faster. FIT3080 introduces both before moving to general clauses [1][1] Monash, “FIT3080 Artificial Intelligence: Logic, Inference Algorithms, and First Order Logic, Parts I and II,” 2025. Course lecture materials, Semester 2. Part II reading list: AIMA 4th ed., Sections 7.1--7.5, 8.1--8.3, 9.1, 9.2, 9.5..

Resolution refutation

Resolution combines clauses containing complementary literals:

$$\frac{C\lor L\qquad D\lor\neg L}{C\lor D}.$$

If $L$ is false, the first parent requires $C$; if $L$ is true, the second requires $D$. Either way, $C\lor D$ holds. This proves the rule’s soundness. Remove one selected complementary pair, retain the other literals, and discard duplicates. Do not delete several unrelated complementary pairs at once.

ProofA complete propositional refutation

Let $K=\{A\to B,B\to C,A\}$ and query $C$. Convert the premises to clauses and add the negated query.

Clause	Formula	Source
1	$\neg A\lor B$	First premise
2	$\neg B\lor C$	Second premise
3	$A$	Fact
4	$\neg C$	Negated query
5	$B$	Resolve 1 and 3 on $A$
6	$C$	Resolve 2 and 5 on $B$
7	$\square$	Resolve 4 and 6 on $C$

Every step has parent clauses and a selected literal. The empty clause shows that $K\land\neg C$ is unsatisfiable, so $K\models C$.

To turn the rule into a decision procedure, repeatedly generate new resolvents while retaining derived clauses and avoiding duplicates. For finitely many propositional variables there are finitely many distinct non-tautological clauses. A complete saturation procedure either derives $\square$ or reaches a fixed point without it; in the latter case the clause set is satisfiable. A timeout before saturation establishes neither outcome.

Resolution is refutation-complete: an unsatisfiable propositional clause set has a resolution refutation. This does not say that unrestricted forward resolution literally generates every logically implied formula. The algorithm answers an entailment query by negating it first.

ProofPropositional resolution completeness

Induct on the number of atoms. With no atoms, a clause set is unsatisfiable exactly when it contains the empty clause. For the induction step choose $p$. Keep every clause not mentioning $p$, and add every resolvent $C\lor D$ of a pair $p\lor C$, $\neg p\lor D$. Discard tautologies. Call this smaller-variable set $S'$.

Any model of the original restricts to a model of $S'$ by resolution soundness. Conversely take a model of $S'$. A clause $p\lor C$ forces $p$ true only when $C$ is false; a clause $\neg p\lor D$ forces it false only when $D$ is false. Both demands cannot occur, since the corresponding retained resolvent would then be false (and could not be a tautology). Choose $p$ to satisfy the demands, or arbitrarily if there are none. This extends the model to the original set. Thus elimination preserves satisfiability.

If the original is unsatisfiable, so is $S'$. Induction refutes $S'$, whose clauses are originals or one-step resolvents, so prefixing those steps gives a refutation of the original. For $n$ atoms there are at most $3^n$ non-tautological clauses, since each atom is absent, positive, or negative. Saturation without the empty clause is therefore both finite and, by completeness, satisfiable.

SAT search: DPLL as a small decision procedure

A SAT solver asks whether a propositional formula has a satisfying assignment. DPLL works on CNF by simplifying clauses under a partial assignment, applying unit propagation, and branching when necessary. A unit clause forces its remaining literal to be true. An empty clause signals a conflict; no remaining clauses means all original clauses have been satisfied by the partial assignment.

Algorithm 2 DPLL on a finite propositional clause set

1:procedure DPLL(S)

2:$S \gets$ UnitPropagate($S$)

3:if $\square \in S$ then

4:return false

5:end if

6:if $S = \emptyset$ then

7:return true

8:end if

9:Choose an unassigned atom $p$ occurring in $S$

10:if DPLL($S[p:=true]$) then

11:return true

12:end if

13:return DPLL($S[p:=false]$)

14:end procedure

Here restriction removes satisfied clauses and removes falsified literals from the others. Unit propagation repeatedly applies this restriction for a unit literal until no unit remains or a conflict occurs. Each branch assigns a new atom, so the finite search terminates. The pseudocode returns a Boolean; an implementation that reports a model must also retain and return the accumulated assignments.

For $(A\lor B)\land(\neg A\lor C)\land\neg C$, unit propagation first forces $C$ false, then $A$ false, then $B$ true. Every clause is satisfied. Adding $\neg B$ instead forces a conflict, establishing unsatisfiability. Modern SAT solvers add conflict-driven clause learning and other search machinery; this basic procedure supplies the logical foundation rather than an account of modern solver performance.

ProofDPLL correctness

A unit literal must be true in every model, so restricting by it preserves satisfiability. For any remaining atom $p$, every model sets it either true or false; hence the current set is satisfiable exactly when one of the two restricted branches is satisfiable. An empty clause has no model, while an empty clause set accepts every extension of the current assignment. These are the base cases. Induction on the number of unassigned atoms proves that the recursive Boolean answer is correct. Each propagation or branch removes an unassigned atom, so the same finite measure proves termination.

What a small theorem prover must record

A minimal propositional entailment tool needs an input language, a semantics-preserving or appropriately equisatisfiable encoding, an inference or search engine, and an interpretable result. A countermodel should be checked against the original premises and query. A resolution certificate should record parent clauses and pivots, ending at $\square$. A separate checker can verify each step without repeating the original search.

The distinction is between finding a proof and checking one. A valid local inference rule does not guarantee a useful search strategy; a fast search does not justify an unchecked conclusion. SAT, UNSAT, and unfinished search must remain different results. For entailment, SAT of $K\land\neg q$ provides a countermodel, while UNSAT establishes the consequence.

Exercises

ExerciseClassify the fragment

Classify $A$, $\neg A\lor B$, $\neg A\lor\neg B$, and $A\lor B$ as definite, Horn but not definite, or non-Horn.

Show solution

Solution

The first two are definite, each having exactly one positive literal. The third is Horn but not definite and expresses a constraint. The fourth is non-Horn, with two positive literals.

ExerciseDo not reverse a rule

Run forward chaining on $\{A,A\to B,(B\land C)\to D\}$ for query $D$. What follows, and what does failure to derive $D$ mean?

Show solution

Solution

The least model contains $A,B$. Nothing supplies $C$, so $D$ is not derived and is not entailed. This does not entail $\neg D$: setting all four atoms true also satisfies the knowledge base. Inferring $C$ from the rule with head $D$ would reverse an implication without justification.

ExerciseBuild a refutation

Prove $R$ from $P\lor Q$, $P\to R$, and $Q\to R$ using resolution refutation.

Show solution

Solution

The clauses are $P\lor Q$, $\neg P\lor R$, $\neg Q\lor R$, and the negated query $\neg R$. Resolve the second and fourth to obtain $\neg P$, and the third and fourth to obtain $\neg Q$. Resolve $P\lor Q$ with $\neg P$ to get $Q$, then with $\neg Q$ to get $\square$.

ExerciseA cutoff is not a countermodel

A resolution search stops after one hundred steps without deriving the empty clause. May it report that the query is not entailed?

Show solution

Solution

No. A step limit is not saturation, and the missing refutation may require further steps. Report an unfinished or unknown result. A verified satisfying assignment of the negated-query problem would justify “not entailed”; a complete finite saturation procedure can also decide it.

Next: variables, witnesses, and unification

The propositional procedures treat each atom as indivisible. To reason with objects, relations, and quantified rules, we need First-Order Resolution and Theorem Proving. The inference-versus-search distinction remains, but termination is no longer automatic.

References

1. [1] Monash, “FIT3080 Artificial Intelligence: Logic, Inference Algorithms, and First Order Logic, Parts I and II,” 2025. Course lecture materials, Semester 2. Part II reading list: AIMA 4th ed., Sections 7.1--7.5, 8.1--8.3, 9.1, 9.2, 9.5. a b
2. [2] S. Russell and P. Norvig, Artificial Intelligence: A Modern Approach, 4th ed. Pearson, 2020. ↩