In 1969, Cordell Green described planning as deduction: encode actions and situations in first-order logic, state a goal existentially, then extract a sequence of actions from a proof. The idea is beautifully general. A logical theory can represent action preconditions, effects, object identities and incomplete knowledge in one language. But blind proof search does not inherit the practical guidance developed by half a century of classical planners.

STRIPS took a specialised route. It represented states extensionally and actions by add and delete lists, turning planning into graph search. Later systems such as FF and Fast Downward combined careful compilation with informative heuristics. Their speed made propositional grounding: the creation of every relevant ground action before search: a standard choice, even when the domain was originally written with variables.

Soutchanski and Young place both traditions in one machine. TPLH uses Reiter’s situation calculus and a Basic Action Theory as the semantics. It explores situation terms with A*. A delete-relaxation heuristic, inspired by FF and Graphplan, estimates distance to the goal. The result is theorem proving whose proof order is chosen by planning knowledge.

The revival matters because grounding can be expensive or impossible in richer first-order settings. TPLH keeps action schemas lifted and finds ground instances only when their preconditions hold in the current state. The authors also seek a route towards theories with incomplete initial information, successor-state axioms containing context conditions and fewer closed-world assumptions.

This is a research prototype, not a victory claim over mature planners. Its evidence is more discriminating: despite extreme runtime overhead, it often expands markedly fewer situations than Fast Downward expands states while producing plans of comparable length. That separation between guidance quality and implementation speed is the paper’s central empirical tension.

The distinguished constant S₀ denotes the initial situation. If action a occurs in situation s, the function term do(a,s) denotes the result. A sequence [a₁,…,a_n] abbreviates a nested term whose outermost layer is the latest action. In Prolog, S₀ can be the empty list and a successor a list extended by one action.

This construction forms a tree. Every non-initial situation has one predecessor, and a situation cannot be its own ancestor. Different action sequences never merge merely because they produce the same fluent valuation. That property eliminates duplicate situation terms from the open queue: no distinct search paths create the same history.

Yet “no duplicate situations” is not “no repeated states”. Move a block away and back, or inspect an object twice without changing anything, and distinct histories may describe identical current facts. State-space planners can detect and merge that equivalence; TPLH deliberately retains it because situations are histories in the semantics.

A fluent is a predicate or function whose final argument is a situation. On(A,B,s) can change with history; an atemporal relation such as A≠B does not. The world at s is not stored as an autonomous node in the logical language. It is what the theory entails about fluents at s.

This distinction explains the memory policy. TPLH stores the initial state and action histories. When it removes a situation from the queue, it progresses the initial state along that history to reconstruct the current valuation. Less state memory is retained, but previous effects may be replayed many times.

The foundational axioms Σ describe situations: S₀ has no predecessor, do constructs successors, and induction reaches every situation. Action precondition axioms D_ap state when each action is possible. For action schema A(x), poss(A(x),s) is equivalent to a formula Π_A(x,s) uniform in s.

Successor-state axioms D_ss solve the representational frame problem. Instead of separate non-change axioms for every action–fluent pair, one biconditional states all ways a fluent becomes true and all ways it remains true because no terminating action occurred. Effects and persistence share one formula.

Unique-name axioms D_una say distinct action function symbols denote different actions and, where required, distinguish object names. The initial theory D_S0 supplies facts and constraints about the starting world. Together: D=Σ∧D_ss∧D_ap∧D_una∧D_S0.

Consider holding(x). Pickup makes it true; Drop makes it false; other actions preserve it. The successor-state axiom is not merely an update rule. It is a logical biconditional defining exactly when holding(x,do(a,s)) follows.

The formal account is broader than the implementation. Results for proper-plus initial theories and local-effect BATs can support incomplete information without declaring every unnamed fact false. The ECLiPSe Prolog prototype, however, requires domain closure and a closed-world assumption. That limit belongs to the software, not to every theorem-proving planner licensed by the formalism.

A situation is executable if S₀ is executable and each successor do(a,s) is executable only when s is executable and poss(a,s) holds. For a sequence α₁,…,α_n, Theorem 1 expands that recursion into precondition claims at every preceding situation.

Given goal formula G(s) and upper bound N, planning asks whether D entails an s whose length is at most N, whose history is executable and whose final situation satisfies G. A witness is not just an action list ending in a goal valuation. The logical query certifies each transition.

Theorem 3 connects the existential statement to search. A ground situation term of length at most N is a solution exactly when one can choose action-schema indices and grounding substitutions such that the theory entails the goal after their composition and the possibility formula at every prefix.

This licenses lifted branching. Suppose Load(x,t,l) has variables. At a situation, the planner asks which substitutions make its precondition true: perhaps x=crate7, t=truck2 and l=depot. Only those ground instances become successors. It need not construct every crate–truck–location combination first.

Soundness and completeness are bounded. If N is at least the shortest solution length and the finite tree is searched faithfully, a solution can be found. If every solution is longer, failure proves only that the chosen horizon contains none. The bound is a termination device and an evidential limit.

The priority queue begins with S₀. Every situation has f=g+h: its history length plus estimated remaining distance. Unit action costs make g exactly Length(s). The queue removes the lowest value, with implementation-specific tie handling.

On removal, the planner progresses the initial database along the history to obtain Now. If the goal holds, it returns the situation, readable as an action list. Otherwise it finds action instances whose preconditions are satisfied there.

For each possible A_i, TPLH constructs do(A_i,s), progresses across that action, checks the length bound and evaluates its heuristic with remaining lookahead d=N−Length(s). Qualifying successors enter the queue.

There is no closed list for duplicate situations because histories are unique. That saves comparison but admits equivalent fluent states under multiple histories. Nor does every queue node cache a state. Reconstructing Now after a pop trades space for repeated progression work.

The pseudocode exposes useful modularity. D defines legal worlds, progression answers what is true now, FindAllPossibleActions supplies lifted successors, H estimates distance and the priority queue imposes policy. Improving one component need not rewrite the semantics.

A propositional planner commonly compiles every parameterised action against compatible objects. In logistics, even impossible package–vehicle–location triples can appear before reachability pruning. That expense occurs regardless of which states are later visited.

TPLH queries action preconditions against Now. For Load(p,t,l), it solves at(p,l), at(t,l) and empty(t) to obtain substitutions supported by the current database. A package elsewhere never combines with the truck here. The action is ground when added, but grounding is delayed and contextual.

The approach resembles theorem proving because unification and query answering produce substitutions. It exposes richer future possibilities: preconditions could contain formulas that do not compile neatly into a fixed propositional operator set. The formal account is designed with that extensibility in view.

The prototype narrows the promise. Benchmark preconditions are conjunctions, optionally including negative equalities; successor-state axioms lack context conditions; goals are conjunctions of ground fluents. Domains are essentially STRIPS tasks translated from PDDL. Possible-action generation can itself be a bottleneck.

Lifted does not automatically mean small. If a state satisfies a schema many ways, the query returns many instances. Nor does run-time grounding erase repeated work across equivalent states. Its value depends on how selectively current preconditions constrain variables and how efficiently answers are indexed.

At each relaxed layer, the algorithm finds possible actions in the relaxed state. It retains relevant actions: those with at least one positive effect not already present: and progresses by adding all positive effects. Deletes are omitted. Each fact layer contains its predecessor.

Expansion stops when all goal literals appear or remaining lookahead is exhausted. If the bound d is crossed without reachability, the implementation returns a penalty beyond the visible horizon. Heuristic computation is tied to bounded search rather than pretending the relaxed problem is unlimited.

Ignoring deletes makes progress easier. A key can remain held after an imagined action that consumes it; mutually exclusive properties can coexist. The graph offers directional evidence, not an executable plan. It may underestimate interactions requiring restoration of deleted conditions.

The design is FF-inspired and Graphplan-like, but reaching a layer is not the final estimate. A second recursive phase selects supporting actions and their preconditions, approximating how many supports are required.

Actions adding nothing novel are filtered. They cannot improve a later monotonic fact layer. This simple relevance test prevents the relaxed graph filling with applicable operations that do not move any reachable fact frontier.

Once the graph reaches the goal, recursion examines newly achieved literals at the latest relevant layer. For each, it collects actions whose positive effects support that literal and whose preconditions held in the preceding relaxed state.

Candidate supporters differ because their preconditions become subgoals. The procedure estimates each candidate and chooses a best supporting action. Preconditions from selected supporters are unioned into the next goal set. Facts already available require no added support.

Shared support matters. One action may add two goals; two selected actions may require one common precondition. Unions avoid treating identical subgoals as unrelated. The result is still approximate, but it extracts a causal skeleton instead of returning layer number alone.

This recursion is expensive. The authors report that heuristic computation consumes more than 95 per cent of runtime. Subproblems can be recalculated, making memoisation an obvious target. Indexing possible actions and improving progression are others.

FF-style relaxed-plan estimates are not guaranteed admissible lower bounds for optimal A*. The paper uses them to seek short plans and reports resulting lengths. “A*” describes the queue; it does not certify optimality when h lacks admissibility.

TPLH was compared with Fast Downward and Best First Width Search. TPLH and Fast Downward used eager A* with an FF heuristic and sought short unit-cost plans. BFWS used default greedy best-first search, so faster search and potentially longer plans were expected.

The machine was an Intel i7-3770 at 3.40 GHz. TPLH ran inside ECLiPSe CLP 7.0 #63 on x86-64 Linux; competitors were compiled executables. Every TPLH problem had a 30-minute timeout and a 50 MB global-stack limit.

Across Barman, BlocksWorld, ChildSnack, Depot, FreeCell, Grippers, Logistics, Miconic and PipesWorld, mean TPLH plan-length ratio to Fast Downward was approximately one. It visited fewer situations than Fast Downward states on eight of nine averages; PipesWorld, with six retained cases, was the exception.

Against BFWS, average TPLH plans were shorter in all nine. Expansion results varied: lower in four domain averages and worse in five. Means sometimes hid majority wins because severe losses dominated, so the paper also reports the fraction of instances where TPLH was no worse.

Runtime reverses the favourable picture. “Time per step” ratios place TPLH roughly 10²–10³ above Fast Downward and 10³–10⁴ above BFWS. These figures combine interpreted execution, preprocessing, repeated progression, lifted queries and expensive heuristic recursion; they do not isolate one cause.

PDDL-to-Prolog domain translation took under a tenth of a second, but initial hash construction cost about 1.5 seconds per BlocksWorld problem and nearly ten per Barman problem. Total time includes it. Removing preprocessing helps easy instances but does not erase the wider gap.

The main horizon was N=100 for instances generally solved within twenty steps. Varying N over 25, 50, 75, 100, 125 and 150 changed time by under 0.5 per cent and left plan length and visits unchanged in tested domains. That local robustness is not a theorem that N never matters.

The dataset began with roughly one hundred generated cases in eight domains and ten pre-existing PipesWorld problems. Timeouts and zero-step exclusions left unequal samples: from 119 Logistics to six PipesWorld. Small cells deserve caution.

Plan length partly reflects policy. TPLH and Fast Downward shared eager A* with FF guidance; BFWS used greedy best-first. TPLH’s shorter plans than BFWS are useful, but do not isolate representation from objective.

The ratio r=plan length divided by visited situations diagnoses search shape. Near one means few situations outside a final route. ChildSnack’s interleavable actions and late goal atoms weaken relaxed guidance; FreeCell’s sequential dependencies strengthen it. The ratio is not runtime or absolute difficulty.

Door chain has a causal corridor: take key, unlock and enter. Harmless Wave and repeatable Look histories do not advance the relaxed goal frontier. Relevance drives the corridor first.

Distractor workshop requires measuring, cutting and assembly. Polish and Photograph add attractive but irrelevant facts. They never support the goal’s relaxed ancestry.

Consumed resource exposes optimism. Pour creates full; Drink consumes full and creates empty; Refill restores full; Serve needs full and empty. Relaxation imagines full surviving Drink and underestimates restoration.

Every node is keyed by its full action list, never its fact set. The display may contain different histories with equal current facts. That is deliberate situation search, not state deduplication.

The displayed h is minimum relaxed fact-layer distance, simpler than the paper’s recursive supporting-action count. It preserves monotonic add effects and ignored deletes while making every value inspectable. Tests concern the architecture, not a false claim of source-code reproduction.

First reproduce the STRIPS-compatible subset: conjunctive preconditions, optional negative equality, context-free successor-state axioms, ground conjunctive goals and unit costs. Translate the same IPC instances and record every exclusion producing retained samples.

Log plan length, situations popped, possible-action answers, progression calls, heuristic calls, unique relaxed subproblems, preprocessing, search time, timeout and memory. Domain means need distributions so catastrophic losses cannot conceal majority wins.

Then ablate engineering: compile Prolog; cache progressed states; memoise recursive heuristic values; index precondition predicates; optionally keep a valuation-keyed closed table. Each answers a separate question and should not disappear inside one opaque optimised system.

To test lifting, scale object counts while reachable bindings remain sparse. Compare pre-grounding size, run-time action answers and memory. Include weakly constrained schemas showing where lifted queries only defer explosion.

Finally extend semantics one dimension at a time: incomplete proper-plus initial theories, removal of domain closure, context conditions, arbitrary costs and richer goals. Add soundness tests and compare with contemporary lifted planners, absent from the 2023 experiment and left for future work.

Review one: formal reconstruction. The companion was checked against the twelve-page v3 source. It retains the situation-tree ontology, five BAT components, recursive executability, bounded entailment, Theorem 3’s schema-and-substitution characterisation, Algorithm 1’s A* loop and Algorithms 2–3’s relaxed support logic.

The main risk was collapsing situations into states. The page states that histories never merge while valuations may repeat. A second risk was presenting relaxation as proof or admissible optimal distance. It is guidance only; exact possibility and goal entailment remain authoritative.

Review two: evidence and delivery. Hardware, interpreted-versus-compiled disparity, horizon, cap, preprocessing, retained counts and competitor policies remain attached to claims. Ratios are TPLH divided by comparator, and time per step is never confused with total time or visits.

The favourable result: fewer expansions than Fast Downward in eight domain averages: is paired with PipesWorld, severe runtime cost and no comparison with recent lifted planners. Figures have titles, descriptions and captions. Animation respects reduced motion; the laboratory labels its simplified h and publishes three exact tests.

Cavrel, Pellier and Fiorino retain temporal constraints while delaying concrete scheduling. Soutchanski and Young retain first-order action semantics while importing relaxed reachability. Both ask what must stay authoritative and what expensive detail may be approximated during search.

A formal representation is not only a language for solutions; it selects the nodes a heuristic sees, duplicates it recognises, computations it repeats and future extensions it can absorb. HTEP nodes are constraint-rich partial plans. TPLH nodes are complete action prefixes with implicit states.

Canon 0089 moves from planning representation to algorithm selection. Moreno-Scott, Ortiz-Bayliss, Terashima-Marín and Conant-Pablos ask whether features of a constraint-satisfaction instance can predict its best heuristic. Guidance shifts up a level: from ranking nodes to choosing who conducts search.

Relaxation may imagine incompatible achievements, but it cannot certify an action. Progression may be slow, but it supplies exact current facts for precondition queries. The returned situation is sound because every prefix was checked in the theory, not because h was accurate.

Fewer visited situations show that the guess often points well. Comparable plan lengths show useful direction. Slow time per step shows that exact and approximate reasoning are implemented expensively. None cancels the others.

The durable contribution is a clean experimental object: logically grounded, lifted, bounded proof search with a familiar planning heuristic. It lets researchers ask how much modern performance can be recovered without surrendering expressive semantics that specialised grounding simplifies.