2.1 Propositional Logic, Horn Rules, and First-Order Representation: Logical Derivation Does Not Imply Truth

“The ground is wet, so it must have rained last night” treats one possible cause as the only cause. Rain → Wet and Wet do not entail Rain: sprinklers, leaks, and cleaning can also wet the ground. Logic can reject the inference; finding who left the tap running takes a separate investigation.

A knowledge system must distinguish clearly between: facts in the real world, statements in language, assumptions in a knowledge base, and what inference rules allow us to derive.

Learning Objectives

• Distinguish between syntax, interpretation, models, entailment, and derivation;
• Correctly apply implication, modus ponens, and contraposition;
• Implement forward chaining with multiple premises and proof traces using Horn clauses;
• Understand the boundaries of first-order logic variables, quantifiers, predicates, and unification.

1. Syntax and semantics are two layers

In propositional logic, atomic propositions such as Rain and Wet are true or false under a given interpretation. Connectives define the structure of compound statements:

• $\mathrm{\neg }P$: not;
• $P\wedge Q$: and;
• $P\vee Q$: or (typically inclusive);
• $P\to Q$: if P then Q;
• $P\leftrightarrow Q$: if and only if.

A knowledge base $KB$ entails a sentence $\alpha$, written $KB\models \alpha$: every interpretation that makes $KB$ true also makes $\alpha$ true. This is a semantic relationship.

An inference system writes $KB⊢\alpha$ to indicate that $\alpha$ can be derived using a set of formal rules. Whether this system is reliable depends on two properties:

• Soundness: everything derivable is semantically entailed;
• Completeness: everything semantically entailed can be derived (relative to the language and proof system).

Input facts may be incorrect, and rules might not apply in certain domains. A formally valid derivation does not guarantee the accuracy of the knowledge base.

2. Implication Easily Misleading in Natural Language

From $P\to Q$ and $P$, we derive $Q$, this is modus ponens.

Deriving $\mathrm{\neg }P$ from $P\to Q$ and $\mathrm{\neg }Q$ is modus tollens. Contraposition refers to the classical equivalence of $P\to Q$ and $\mathrm{\neg }Q\to \mathrm{\neg }P$.

The following two forms do not hold:

• Affirming the consequent: $P\to Q,Q\therefore P$;
• Denying the antecedent: $P\to Q,\mathrm{\neg }P\therefore \mathrm{\neg }Q$.

"The ground is wet if it rains" does not imply "the ground is only wet when it rains." If a business truly intends to express a bidirectional condition, it must explicitly state both sufficient and necessary conditions and verify edge cases.

3. Horn clauses make rule inference executable

A definite Horn rule can be written as:

$$p_1\wedge p_2\wedge \cdots \wedge p_k\to q.$$

Forward chaining starts with facts and adds a conclusion once every premise is known. This Python 3.9+ function fragment (partial) accepts string facts and a finite collection of Rule objects. missing counts premises whose effects have not yet been propagated from the queue; each fact propagates once. Empty-premise rules seed facts directly. See Berkeley CS 188 on forward chaining for the counting method.

from collections import defaultdict, deque
from dataclasses import dataclass

@dataclass(frozen=True)
class Rule:
    premises: frozenset[str]
    conclusion: str
    rule_id: str

def forward_chain(initial_facts, rules):
    rules = list(rules)
    known = set(initial_facts)
    proof = {fact: ("given", ()) for fact in known}
    waiting = defaultdict(list)
    missing = {}

    for i, rule in enumerate(rules):
        missing[i] = len(rule.premises)
        for premise in rule.premises:
            waiting[premise].append(i)

    agenda = deque(sorted(known))
    fired = set()
    for i, rule in enumerate(rules):
        if not rule.premises:
            fired.add(i)
            if rule.conclusion not in known:
                known.add(rule.conclusion)
                proof[rule.conclusion] = (rule.rule_id, ())
                agenda.append(rule.conclusion)

    while agenda:
        fact = agenda.popleft()
        for i in waiting[fact]:
            missing[i] -= 1
            if missing[i] == 0 and i not in fired:
                fired.add(i)
                rule = rules[i]
                if rule.conclusion not in known:
                    known.add(rule.conclusion)
                    proof[rule.conclusion] = (
                        rule.rule_id,
                        tuple(sorted(rule.premises)),
                    )
                    agenda.append(rule.conclusion)

    return known, proof

With initial facts {A} and rules A→B and A∧B→C, the result should be {A,B,C}. A multi-premise rule requiring B must not fire from A alone. With no initial facts but a True→A rule, A should still be derived. Subtracting known facts from the count and subtracting them again on removal can cause missing or premature conclusions.

Proof records enable the system to answer "why." Implementing production rules also requires handling rule versions, fact sources, time validity, retraction, and conflicts; monotonic forward chaining only adds facts and cannot naturally retract previous conclusions.

4. Closed-world vs. Open-world

Open-world assumption: The knowledge base lacking P does not imply ¬P. Suitable for scenarios with incomplete knowledge.

Closed-world assumption: Treat queries involving P as false if not found, commonly used in controlled, integrity-guaranteed databases or logical programs.

The distinction is whether an absent record is sufficient evidence for a negative conclusion.

For example, if the equipment registration database has a complete asset list, "can't find the device" can trigger a check for non-existence; however, if a public knowledge graph cannot find someone's certificate, it cannot be asserted that the person doesn't have one.

5. Backward chaining From goal to premises

To prove Slippery, backward chaining searches for rules whose conclusion matches the goal, then recursively proves the premises of those rules. It is well-suited for queries with few goals but must handle:

• Multiple optional rules;
• Cyclic dependencies;
• Repeated subgoals;
• Variable substitutions;
• Deep search depth and resource constraints.

Memoization or tabling can prevent redundant proofs of the same subgoals and assist in managing recursive rule structures.

6. Propositional Symbols Cannot Reuse Structure

To express:

All teams that need rescue and have a known location should receive support.
Team-7 needs rescue.
Team-7's location is known.

manually writing separate propositions for each team leads to excessive bloat. First-order logic introduces:

• Constants: team_7;
• Variables: x;
• Predicates: NeedsRescue(x);
• Functions: LocationOf(x);
• Universal and existential quantifiers: $\mathrm{\forall },\mathrm{\exists }$.

These rules can be written as:

$$\mathrm{\forall }x(NeedsRescue(x)\wedge LocationKnown(x)\to Dispatch(x)).$$

7. Unification Matching Structures

Unification finds a substitution that makes two expressions equal, for example:

NeedsRescue(x)
NeedsRescue(team_7)

Yields {x ↦ team_7}. This is not fuzzy string matching; predicate arities, constants, nested terms, and occurs checks all affect correctness.

General first-order logic reasoning is semi-decidable and computationally expensive. Restricted languages like Datalog achieve termination and query realizability by disallowing arbitrary function terms and enforcing safe rules. When selecting a representation language, one must balance expressiveness, decidability, and interpretative cost.

8. Conflicts, Time, and Default Rules

Real-world rules often look like this:

Status = Completed → Settlement is allowed
Unresolved disputes exist → Settlement is not allowed

In classical logic, deriving both a proposition and its negation leads to inconsistency. Engineering systems must define:

• Whether rule priorities are grounded in domain-specific reasoning;
• How default rules are revoked when exceptions arise;
• The validity period of facts and the observation window for those facts;
• Whether conflicts are blocked, escalated, or resolved using paraconsistent reasoning;
• Who has the authority to modify rules and facts.

Do not implicitly treat the order of code in if/elif as a policy priority.

Common Misconceptions

• "Wet ground implies rain": This is affirming the consequent.
• "If something is derivable, it proves reality is true": It only shows that the statement holds within the knowledge base and rules.
• "Forward chaining equals a sequence of if statements": It also requires multiple premises, saturation, cycles, and provenance tracking.
• "No record means negation": This depends on world assumptions and data integrity assumptions.

Exercise

1. Construct one valid or invalid example for each of the four types of implication reasoning.
2. Add multi-premise rules to forward chaining and generate a complete proof tree.
3. Compare query results from a certificate store under open-world and closed-world assumptions.
4. Rewrite the repeated propositions from three teams into first-order predicates and rules.

Summary

The way knowledge is represented determines which structures can be clearly expressed, and the inference rules determine which conclusions can be proven. Logic provides guarantees relative to assumptions, it does not take responsibility for verifying the input facts or the underlying real-world mechanisms.

The next lesson replaces "proving a proposition" with "satisfying a set of constraints": scheduling, graph coloring, and Sudoku are all examples of constraint satisfaction problems (CSPs), but their performance depends heavily on the order of constraint propagation and search.