Chapter 10 — Putting an LTMS to Work (LTRE)

Turning the propositional LTMS into a usable reasoning engine: facts, rules, assumptions, proofs, and search. companion index

The big idea

The LTMS of chapter 9 speaks only propositional clauses over abstract nodes. To use it you need a layer that lets you talk about facts — ground statements like (human socrates) — and rules that fire when patterns match, while the LTMS quietly does all the propositional bookkeeping underneath.

That layer is the LTRE (Logic-based Tiny Rule Engine), src/ltms/ltre.py. The division of labour is clean:

  • the LTRE does universal instantiation — matching rule patterns against the fact database and firing rule bodies;
  • the LTMS does all propositional reasoning — clause normalization, BCP, belief revision, contradictions.

On top of that sit three classic facilities — indirect proof, closed-world assumptions, and dependency-directed search — each a small program that exploits the LTMS’s contradiction-handler stack.

Concepts, step by step

One datum, one node

Every ground proposition is interned as a Datum that owns exactly one LTMS TmsNode. Belief is read straight off the node’s label. Crucially, negation is a sign, not an object: (not P) and P share one node; a query for (not P) just inverts P’s label. The stored form is always the unsigned proposition.

assert vs. assume (the load-bearing asymmetry)

  • assert! installs a formula as permanent clauses by direct translation: simple propositions become their nodes, connectives stay, and the result is normalized to CNF. No node is created for the compound — it is just constraints.
  • assume! must be retractable, so it is different. For a simple proposition it makes the node an assumption directly. For a compound formula it creates a guard node N_F and installs N_F → formula; disabling N_F switches the whole formula off. This asymmetry is deliberate and important.

Rules and the enqueue bridge

A rule has a trigger pattern, a condition, and a body (a Python callable receiving the match bindings). The condition is one of:

  • INTERN — fire as soon as a matching datum exists, regardless of belief;
  • TRUE / FALSE — fire only when the matched proposition is believed true/false.

A belief-conditioned rule that matches before the label is decided is parked on the node. The connection back to the LTMS is the enqueue procedure: when BCP labels a node, it pushes that node’s parked rules onto the LTRE’s queue, which run_rules later drains. So rules wake up exactly when belief changes — the single wire that couples the two layers.

Conjunctive (“A and B”) rules are built by nesting: matching the first pattern installs a rule for the second (capturing the first’s bindings), and so on — the same technique the TRE uses, now belief-aware.

Three facilities built on the handler stack

All three work by pushing a contradiction handler, making some assumptions, running rules, and reacting to whatever conflict arises:

  • Indirect proof (indirect.py): to prove a fact, assume its negation and run. If that assumption participates in a contradiction, retract it and install a nogood that forces the fact. (Proof by contradiction, mechanized.)
  • Closed-world assumptions (cwa.py): assume false every currently-undecided instance of a predicate (negation as failure), as retractable assumptions under one informant, so the closure can be withdrawn cleanly and any later positive evidence surfaces as a contradiction.
  • Dependency-directed search (dds.py): assign mutually-exclusive choice sets depth-first; on a conflict, identify the responsible choices via assumptions_of_clause and learn a nogood that forces the dead choice false — so the search never re-explores it.

The examples, explained

  • Forward chaining with belief. A rule (human ?x) →[TRUE] assert (mortal ?x) plus assert (human socrates): asserting human socrates makes it believed, which wakes the rule, which asserts mortal socrates.
  • Propositional reasoning for free. Assert (p ∨ q) and ¬p; the LTMS forces q with no rule involved — the engine layer inherits all of BCP.
  • Belief revision. assume rain, derive wet ground via rain → wet ground, then retract rain and watch wet ground go UNKNOWN — unless a second support (a sprinkler) keeps it. This is the examples/kb/belief_revision.kb walkthrough.
  • Proof by cases via indirect proof. From (p ∨ q), p → r, q → r, plain BCP cannot get r, but try_indirect_proof(r) assumes ¬r, derives ¬p and ¬q, hits the contradiction with (p ∨ q), and concludes r.

Exercises walk-through

Full set: ../exercises/ch10/; runnable in solutions.py.

  • Why (:TRUE (:NOT ?x)) can’t be a trigger — there is no node/datum for a negation, so nothing is ever filed under that pattern. Use a FALSE trigger on ?x instead.
  • Adding XOR — no new machinery needed; it is the derived expansion (a ∨ b) ∧ ¬(a ∧ b), shown as a one-line term macro (and as a .kb file).
  • NEEDS (abduction) — one-step: for each clause mentioning the goal literal, the other literals pinned false form a candidate support set; deeper abduction recurses. Minimum-cost abduction (LABDUCE) layers a cost search on top.
  • N-queens via DD-search — one choice set per row, a nogood per attacking pair; dd_search returns all solutions (counts 4→2, 5→10, 6→4). Cryptarithmetic and zebra-style logic puzzles are the same shape on a richer constraint set.

Try it in this repo 

. .venv/bin/activate
python exercises/ch10/solutions.py                          # XOR, NEEDS, N-queens counts
python examples/run_kb.py exercises/ch10/kb/belief_revision.kb
python examples/run_kb.py exercises/ch10/kb/modus_chain.kb
python examples/coloring_dds.py                             # map coloring via DD-search

A minimal session in Python:

from ltms.ltre import LTRE
e = LTRE()
e.assert_(("implies", ("rain",), ("wet", "ground")))
e.assume(("rain",), "guess")
assert e.is_true(("wet", "ground"))
e.retract(("rain",), "guess")
assert e.is_unknown(("wet", "ground"))     # belief revised

Or describe the world in a data file (the DSL) with no Python theory at all:

rain         -> wet ground
sprinkler on -> wet ground
assume rain
expect wet ground true

Takeaways

  • The LTRE adds facts and rules; the LTMS still does all the logic.
  • One datum per proposition; negation is a sign; assert is permanent, assume is guarded and retractable.
  • Rules and belief are coupled by a single enqueue-on-label-change bridge.
  • Indirect proof, closed-world assumptions, and dependency-directed search are all small programs over the contradiction-handler stack — the real power of a TMS-backed engine.

Back to the companion index · previous: Chapter 9 — LTMS.

This site uses Just the Docs, a documentation theme for Jekyll.