Chapter 7: Peer Agents and Proof Reconstruction

Mix.install([
  {:shot_tx, "0.1.0"},
  {:kino, "~> 0.19.0"}
])

Overview

The observation Chapter 6 closed on was not developed there: once closure evidence is published rather than called for, a second consumer costs nothing. The workers broadcast, $\mathcal{CA}$ subscribes, and any further process registering on the same topic sees the same stream without a line of the worker changing. This chapter develops the three components on the other side of that stream.

Two of them are the peer agents Chapter 6 placed but did not open. $\mathcal{SA}$ turns evidence about one branch into a cheap instantiation hint for another. $\mathcal{MA}$ turns a saturated branch into a satisfiability probe against an external model finder. Neither is required for the calculus to be complete, and both are ablatable, which is what makes them measurable in Chapter 8.

The third component reads a different shared table. Every branch writes its own derivation history to :traces as it proceeds, and a session ending in a verdict has, in that table, what is needed to rebuild the derivation as a textbook object. Proof reconstruction makes the result of the concurrent search checkable: whatever route the population of workers took, the artefact returned is an ordinary tableau proof.

The lineage of this design is set out in § Agent-Based and Cooperative Proof Search: $\Omega$-Ants and its resource-adaptive form OANTS [BS98, Sor01, BSJK08], the cooperative use of an external reasoner in LEO-II [BSJK05, BPTF08], and the agent framework of Leo-III on the LeoPARD substrate [SWB16, BSW17, WSB15]. Two differences bear on the agents of this chapter. In $\Omega$-Ants the blackboard is the coordination point and the agents exist to fill it, whereas here the shared tables are passive and coordination happens through a broadcast, so an agent is added by subscribing rather than by registration with a scheduler. $\Omega$-Ants agents also suggest the next command to a proof planner, whereas $\mathcal{SA}$ and $\mathcal{MA}$ never direct the search: one publishes hints that workers may ignore, the other answers a question the search did not ask.

The Suggestion Agent

A branch never applies a substitution to itself. Chapter 3's rules are binding-free by construction and Chapter 6's workers may not commit to a value for any free variable, so the pre-unifier $\Theta$ closing the tableau lives in $\mathcal{CA}$'s solution and arrives, if it arrives, at the end. The consequence is easily overlooked: the branch never observes the structure that applying $\Theta$'s substitution $\theta$ would have introduced. Once $X$ becomes $t$, new redexes appear, heads that were flexible become rigid, and formulae that were opaque become decomposable. Each of those is a rule application the branch could have made, and a closing pair it could have found. This is the cost at which rigidity secures soundness under parallel search.

The calculus can still reach that structure. It reaches it through $\gamma$, which enumerates instances, and through primitive substitution, which enumerates general bindings. Both are the most expensive rules in Chapter 3's cost table, and both enumerate blindly. $\mathcal{SA}$ reaches the same structure at lower cost, by taking a substitution that another branch's evidence has already shown plausible and offering it here as an ordinary instantiation step.

Definition (Instantiation Hint). Let $\varphi, \psi$ be a disagreeing literal pair reported by some branch, and let $\sigma$ be a pre-unifier of that pair. For each binding $X \mapsto t$ in $\sigma$, let $\Phi$ be the matrix of the rule that introduced $X$ and $B_0$ the branch on which it was introduced. The pair $(\Phi, t)$ is an instantiation hint originating on $B_0$. A branch $B$ admits the hint if $B_0$ is a prefix of $B$, and applying it adds $\Phi(t)$ to $B$ as an ordinary instance.

The definition rests on three conditions, and each is a point at which no hint is produced.

The first is the matrix. A hint is meaningful only if the quantifier that introduced $X$ can be identified again, which is what the :provenance table records: for every fresh variable, the matrix, the source formula, the originating branch, and whether the variable came from $\gamma$ or from a prim-subst hole. Without that record a unifier is a statement about terms; with it, a unifier becomes a statement about a rule that some branch still has available.

The second is the originating branch, which is what makes reuse of a hint sound. Hints are keyed by branch prefix, and a worker splices only those originating on an ancestor of the branch it holds. A hint originating on a sibling is not admitted, since the matrix it names need not exist there.

The third is the type. A hint is applied as an application of the matrix to the term, so the term must inhabit the matrix's argument type. A well-typed $\sigma$ does not guarantee this, because the holes of a general binding carry the binding's types rather than the quantified variable's. Mismatches are dropped at publication.

The pipeline is five steps over one table. $\mathcal{SA}$ ingests {:local_clashes, branch_id, pairs} from the topic $\mathcal{CA}$ also reads. It unifies each pair on its own and takes at most one solution, since a multi-pair regime would be the CSP and the CSP belongs to $\mathcal{CA}$; $\mathcal{SA}$ is therefore weaker than $\mathcal{CA}$ by construction. Each binding of the resulting $\sigma$ is looked up in :provenance, type-checked against the matrix, and written to the :suggestions table under the key {birth_branch, recipe, term} with :ets.insert_new/2, so a hint published twice is stored once. A successful insert dispatches :work_available, which wakes idle workers instead of leaving them to the next scan.

Splicing happens at checkout and at yield rather than at publication. A worker holding a branch traverses its own ancestor prefixes, matches them against the table, and injects {:suggested_instantiate, recipe, term} onto the branch's queue. The synthetic rule is priced at $2$, cheaper than $\gamma$ and far cheaper than prim-subst, but dearer than the atomic rule at $1$, so a hint never preempts closure detection on a branch about to close.

Dropping a type-mismatched hint costs nothing. A hint is a search shortcut, and this one names no formula the branch could hold. Publishing it would raise inside rule application, on a different branch from the one that produced the evidence, and cost that branch its verdict.

Definition (Cascade). A spliced hint may produce fresh disagreements, hence fresh pre-unifiers, hence fresh hints. The cascade depth of a hint is the number of times it has been spliced across all descendants of its birth branch, and splicing is refused once that depth exceeds a fixed ceiling.

The ceiling is suggestion_cascade_ceiling, default $3$. The counter occupies a fixed position in the suggestion row and is bumped with :ets.update_counter/3 at the splice site, in a single atomic operation: two workers racing for the last slot cannot both take it, and no lock is required. This closes the feedback loop between $\mathcal{SA}$ and the workers, which runs from worker to evidence to $\mathcal{SA}$ to the :suggestions table and back to a worker, entirely through shared memory and without touching $\mathcal{CA}$.

$\mathcal{SA}$ never declares closure. Pair-level search cannot witness a multi-branch closure, so :unsat remains $\mathcal{CA}$'s alone, and the worst a wrong hint can do is waste a step. That asymmetry is why the agent is safe to leave on by default: it can only add formulae the $\gamma$-rule was entitled to add.

The ablation is a single flag. Running one problem both ways shows the verdict unchanged and the route different.

import ShotDs.Hol.Sigils
alias ShotTx.Prover
require Logger
Logger.configure(level: :error)

conjecture = with_context ~e[p: $i > $o, a: $i, b: $i], fn ->
  ~f"(![X: $i]: (p @ X)) => ((p @ a) & (p @ b))"
end

for enabled <- [true, false] do
  {micros, result} = :timer.tc(fn -> Prover.prove(conjecture, suggestions_enabled: enabled) end)

  {enabled, Prover.format_result(result), div(micros, 1000)}
end
|> Enum.map_join("\n", fn {e, v, ms} ->
  "* `suggestions_enabled: #{e}` gives `#{v}` in #{ms} ms"
end)
|> Kino.Markdown.new

Both rows report THM. $\mathcal{SA}$ is a heuristic over a complete calculus, so switching it off may cost steps but never the verdict; a discrepancy here would indicate a bug in the splice rather than a property of the problem. Chapter 8 runs the comparison across the TPTP corpus, where the quantity recorded is the number of problems solved; the per-rule counters that would show the $\gamma$-instantiations avoided are not written to the sweep's rows.

The Model Agent

$\mathcal{MA}$ inverts the question. $\mathcal{CA}$ collects evidence towards a global pre-unifier $\Theta$ closing every branch, while $\mathcal{MA}$ takes a single branch that has stopped producing rules and asks an external tool whether it describes a model. A :sat verdict on any branch ends the session, because one satisfiable branch witnesses satisfiability of the whole input. Consulting an external reasoner about a subproblem and integrating the verdict that comes back is the arrangement LEO-II uses for its first-order backend [BSJK05, BPTF08]; what differs here is that the external system is asked for a model rather than for a refutation.

This is a separate agent rather than a check inside the branch because of the boundary drawn in Chapter 3. model_certain? decides an under-approximation of openness using only what the calculus can see, namely identity, bounded unifiability, and the oriented equations of $\mathcal{E}(B)$, and it reports exhausted rather than open whenever extensionality would be needed to settle a pair. $\mathcal{MA}$ decides some of those exhausted branches by asking a tool that decides more than the calculus does.

Definition (Frontier Projection). Write $\mathrm{Fr}(B)$ for the frontier of a branch and $\mathrm{Def}(B)$ for its definition map. The frontier projection of $B$ is the problem whose axioms are $\mathrm{Fr}(B)$, whose definitions are $\mathrm{Def}(B)$, and which has no conjecture. A model of the projection is a model of $B$.

The projection ships the frontier rather than $\mathrm{Lit}(B)$, which is what the frontier exists for. The frontier tracks what the branch commits to: a rule consuming its source replaces it there, while $\gamma$ and prim-subst leave their sources in place, because a fresh instance is a hint rather than a new commitment. Paramodulants and $\gamma$-fresh atoms therefore reach $\mathrm{Lit}(B)$ without entering the frontier, which suits a model finder, since they are consequences and shipping them would enlarge the vocabulary the tool must interpret. Constant declarations are derived from the axioms, with constants occurring only in definitions added afterwards so their types are not lost, and the axiom order is sorted so the emitted problem is deterministic.

The agent is a timer loop. Each element of it keeps an expensive external call from becoming a bottleneck.

• It scans the live branches on a tick, reading them out of the shared work and idle queues and discarding any whose ancestor has been tombstoned.
• A branch is eligible when its frontier is neither too small nor too large, when its frontier version has advanced since the last probe of that branch, and when no probe for it is in flight. Versioning stops the agent from re-asking the same question, since a branch that has not changed its commitments will not answer differently.
• Eligible branches are dispatched up to a cap on concurrent probes, each on a supervised, monitored task.
• Verdicts arrive asynchronously. :sat ends the session, a backend error clears the recorded version so the next tick retries, and anything else is dropped.

Both frontier bounds concern the model finder rather than the prover. A frontier below model_agent_min_frontier ($3$) carries no information, since a branch asserting a single atom is trivially satisfiable, and one above model_agent_max_frontier ($100$) exceeds what finite model finders handle, since they scale poorly in vocabulary. model_agent_max_in_flight ($2$) reflects that an Isabelle server serialises model finding, so further concurrency only fills a queue.

Failure isolation is why the probes are async_nolink and monitored. A crashing backend must not take the agent with it, and the :DOWN handler removes the branch from the in-flight map so it becomes eligible again rather than remaining stuck. This applies the supervision argument of Chapter 6 at the finest granularity the system has, where the unit of failure is one probe on one branch.

The backend is a behaviour with two callbacks, split so a probe never blocks the agent's mailbox: a dispatch returning a handle immediately, and a wait on that handle bounded by a time budget. Three implementations exist. :none is the default, under which the agent starts, logs once, and never schedules a tick, so the layer costs one idle process. A stub returning :unknown unconditionally is the safe choice for tests. The Isabelle/Nitpick backend [BN10] sends the projected problem to a warm server and runs nitpick[satisfy], which consumes the shape the projection produces, namely axioms without a conjecture. Because the behaviour is a plain callback module, a different finder is a new module and nothing further.

When $\mathcal{MA}$ is about to declare :sat it checks whether the session has already been decided, and logs an error and emits telemetry if so. A simultaneous :sat from $\mathcal{MA}$ and :unsat from $\mathcal{CA}$ on a consistent problem is impossible, so the check does not guard against a race. It is an alarm for a soundness bug in the frontier or in atom decomposition, placed where such a bug would first become visible.

With the backend at its default, satisfiability is still reported for branches the calculus can settle by itself, and the result carries a model rather than a derivation.

import ShotDs.Hol.Sigils
alias ShotTx.Prover

csa = with_context ~e[p: $i > $o, a: $i, b: $i], fn ->
  ~f"(p @ a) => (p @ b)"
end

Prover.prove(csa)
|> Prover.format_result()
|> then(&Kino.Markdown.new("```\n#{&1}\n```"))

The verdict is CSA. The branch separates $p,a$ from $\neg(p,b)$ at an argument position holding two distinct rigid base-type constants, which is the configuration a free term model satisfies, so § Global and Local Tableau States calls the branch open without an external probe. $\mathcal{MA}$ exists for the branches that fail that test and are reported exhausted.

Proof Reconstruction

The prover returns more than a verdict. On :unsat it returns a derivation tree, which is rebuilt after the search from the trace records the branches wrote as they proceeded. Recovering a readable derivation from a compact record of a search is the problem expansion trees [Mil87] address for higher-order proofs.

Definition (Trace). The trace of a branch is the sequence of entries $(s, r, \bar{p})$, oldest first, where $r$ is a rule applied on that branch, $s$ the formula it was applied to, and $\bar{p}$ the formulae it produced. A branch that closed conditionally carries a final entry naming the pair whose unification closes it.

Traces live in the :traces table, keyed by branch id, and are written by the worker at every lifecycle event rather than at the end. A branch that is split or instantiated publishes each child's trace and deletes the parent's, so the table holds the current leaves and never accumulates a redundant interior. The history each branch carries is recorded inside rule application, after the rule has run, so the produced list is exact rather than predicted, and a closed branch's trace includes the step that closed it. Reconstruction reads the table once, at the end, from $\mathcal{CA}$'s own state.

Rebuilding a tree from a set of leaf traces takes two steps. The first turns a trace into a linear sequence of events, discarding bookkeeping that has no place in a derivation. The second merges those sequences into a tree by shared prefix.

Definition (Linearisation). The linearisation of a branch's trace is the sequence of events obtained by mapping each entry to the formula it contributes to this branch, dropping entries that contributed none. For a branching rule the contribution is the alternative this branch took, selected by consuming one segment of the branch identifier.

Branch identifiers encode the path through every split as suffixes, _A and _B for the two sides of a $\beta$-rule and _I{idx} for the $\mathrm{idx}$-th child of an $(\mathrm{inst})$, so linearisation reads the identifier as a stack and pops one segment at each branching entry. A trace can therefore be interpreted without the tableau, because the identifier records the position.

Several entries linearise to nothing, and each corresponds to a step the calculus did not take. A $\gamma$ or prim-subst firing that produced no instances is a rule parked at its limit. A tautology or contradiction verdict produced no formula. An $(\mathrm{inst})$ with an empty enumeration is the degenerate case of § Literal Processing, where the rule reduces to plain admission. The atomic rule appears only where it unfolded a definition, which is why the definition unfolding of Chapter 3 surfaces in the finished proof as its own $\mathrm{unfold}$ step.

Definition (Derivation). Given the linearisations of all closed branches, the derivation is built by grouping the sequences on their first event: sequences agreeing there share a single step, and the construction recurses on their tails. A step whose group splits into several distinct first events acquires one child per group.

Sharing by prefix is what merges the parallel runs into one derivation. Two branches diverging at a $\beta$-rule share every step above it once and fork below it, and a run without branching stays a single chain. The initial formulae, the assumptions together with the negated conclusion, become given steps chained above the whole derivation, and each step is numbered as it is created, so the sources of a step are line numbers in the ordinary sense. Closure leaves cite the pair that closed them, and a countermodel leaf carries the branch's atoms and definitions instead of a formula. The seeded $\top$ and $\neg\bot$ of § Literal Processing are stripped from that leaf and from every reported model, so the two entries every branch starts with are never mistaken for facts the search established.

The conjecture Chapter 6 proved end to end can be rendered as text rather than as a diagram, which shows the numbering and the sources directly.

import ShotDs.Hol.Sigils
alias ShotTx.Prover

theorem = with_context ~e[p: $i > $o, a: $i], fn ->
  ~f"![X: $i]: (p @ X) => p @ a"
end

{:thm, proof} = Prover.prove(theorem, simplification: :none)

proof
|> ShotTx.Proof.to_text()
|> then(&Kino.Markdown.new("```\n#{&1}\n```"))

The proof object carries both components of the pre-unifier $\Theta = (\theta, C)$ found by $\mathcal{CA}$: the substitution $\theta$ and the residual flex-flex set $C$. The tableau is closed under $\theta$, and $C$ belongs to the answer rather than being omitted from it, since by the definition of Chapter 4 every unifier of $C$ extends $\theta$ to a unifier of the closing equations. Chapter 6's rendering of the same object as a Mermaid tree presents this data under a different formatter.

Discussion

The three components of this chapter differ in function and agree in how they attach to the search. $\mathcal{SA}$ reads the evidence stream and writes a table that workers consult. $\mathcal{MA}$ reads the branch queues and writes to the Manager. Reconstruction reads a table and writes nothing. None of them is called by the search, none can block it, and each can be disabled by a flag or simply left unread.

This bears out the property claimed in Chapter 6 rather than establishing a new one: where closure is published rather than requested, an additional consumer costs close to nothing. What remains open is whether these particular consumers reduce search cost enough to justify their overhead, which Chapter 8 addresses for $\mathcal{SA}$ and $\mathcal{CA}$ by switching each off against a fixed baseline. $\mathcal{MA}$ ran at model_agent_backend: :none throughout that study, so neither its cost nor its contribution is measured.

Chapter References

• [BN10] Jasmin Christian Blanchette and Tobias Nipkow. Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In Interactive Theorem Proving (ITP 2010), LNCS 6172, pages 131–146. Springer, 2010.
• [BPTF08] Christoph Benzmüller, Lawrence C. Paulson, Frank Theiss, and Arnaud Fietzke. LEO-II: A cooperative automatic theorem prover for classical higher-order logic (system description). In Automated Reasoning (IJCAR 2008), LNCS 5195, pages 162–170. Springer, 2008.
• [BS98] Christoph Benzmüller and Volker Sorge. A blackboard architecture for guiding interactive proofs. In Artificial Intelligence: Methodology, Systems, and Applications (AIMSA 1998), LNCS 1480, pages 102–114. Springer, 1998.
• [BSJK05] Christoph Benzmüller, Volker Sorge, Mateja Jamnik, and Manfred Kerber. Can a higher-order and a first-order theorem prover cooperate? In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2004), LNCS 3452, pages 415–431. Springer, 2005.
• [BSJK08] Christoph Benzmüller, Volker Sorge, Mateja Jamnik, and Manfred Kerber. Combined reasoning by automated cooperation. Journal of Applied Logic, 6(3):318–342, 2008.
• [BSW17] Christoph Benzmüller, Alexander Steen, and Max Wisniewski. Leo-III version 1.1 (system description). In LPAR-21 Workshops (IWIL), Kalpa Publications in Computing 1, pages 11–26, 2017.
• [Mil87] Dale A. Miller. A compact representation of proofs. Studia Logica, 46(4):347–370, 1987.
• [Sor01] Volker Sorge. $\Omega$-ANTS: A Blackboard Architecture for the Integration of Reasoning Techniques into Proof Planning. PhD thesis, Universität des Saarlandes, Saarbrücken, 2001.
• [SWB16] Alexander Steen, Max Wisniewski, and Christoph Benzmüller. Agent-based HOL reasoning. In Mathematical Software (ICMS 2016), LNCS 9725, pages 75–81. Springer, 2016.
• [WSB15] Max Wisniewski, Alexander Steen, and Christoph Benzmüller. LeoPARD: A generic platform for the implementation of higher-order reasoners. In Intelligent Computer Mathematics (CICM 2015), LNCS 9150, pages 325–330. Springer, 2015.

Previous: Chapter 6: A Concurrent Actor-Based Architecture  $\cdot$  Contents  $\cdot$  Next: Chapter 8: Evaluation