Logitration

Research: the landscape

“Logical orchestration” is not a standard field. What exists has other names: neurosymbolic work, automatic planning, BDI agents, logic programming, answer set programming, Datalog for permissions, rule engines, workflows, formal verification and classic multi-agent systems.

A web search for “logic orchestration” and “logical orchestration” with variants, restricted to 2020-2026 and run on 5 November 2026, found no field, book or standard with that name [Term search]. All these families answer the same question with different tools: who does what, when, and whether it is allowed. This page walks through them and declares no winner. Most works were read in full text; those marked with a dagger (†) in the references were read only as abstracts or summaries, and their claims are worded accordingly.

Map of the families

Each row is a family, in the words of this survey: what the logic decides, what the language model does, and the works behind it.

FamilyWhat the logic decidesWhat the LLM doesSources
Translate and solveA solver or planner computes the answer from what the model formalised.Translates the problem into PDDL, logic or constraints; in some systems rewrites after solver errors.[LLM+P] [SatLM] [Logic-LM] [LINC] [ProSLM]
Propose and criticiseExternal critics accept or reject each proposal; the model revises.Proposes plans or writes the search code.[LLM-Modulo] [LLM-Modulo travel] [Thought of Search] [Generalized planning]
Planning and the question “can models plan?”A planner or validator produces or checks the plan.Alone, or in a loop, it proposes plans; it is the thing being measured.[PlanBench] [Planning abilities] [o1 on PlanBench] [Chain of Thoughtlessness] [Frontier LLMs vs planners] [ChatHTN] [HTN-MCP]
Policies and checked actionsRules veto, enumerate or verify actions and permissions.Proposes the action; sometimes translates the policy to a formula.[AgentSpec] [Z3 on tool calls] [FormalJudge] [Formal-LLM] [Cedar] [OPA]
Model orchestrates, logic computes and recordsLogic computes over the data and keeps a replayable trace.Chooses the tools, plans, replans and writes the answer.[VADAOrchestra] [MCP-Solver] [PrologMCP]
Agent classicsBeliefs and plans, situation calculus, contract protocols.Absent from the classics; in recent work, a language actuator.[BDI systems] [ChatBDI] [Golog] [Contract Net] [Blackboard]
Rule engines, constraints and verificationRules, constraints or a model checker decide or verify.Mostly absent; one design-time use.[clingo] [Soufflé] [Rule engines] [TraceFix] [Temporal] [LangGraph]
Expert systems and explanationThe rule base and engine decide and can answer how and why.Interface, or called when the rules reach an impasse.[MYCIN how/why] [Explainable BDI] [Contrastive BDI] [AgentSpeaX] [CogRec]

Translate and solve

Four works from 2023 share one idea: the model does not solve the problem, it translates it. LLM+P turns a planning problem into PDDL and hands it to a classical planner [LLM+P]; SatLM writes a declarative specification for a satisfiability solver [SatLM]; Logic-LM formalises the problem in symbolic logic, calls a solver and uses the solver’s error messages to rewrite the formalisation [Logic-LM]; LINC translates to first-order logic and leaves the deduction to a theorem prover [LINC]. ProSLM, from 2024, uses Prolog with a domain knowledge base to give context and to validate answers [ProSLM], and a 2025 proposal has the model write the plan in Prolog [Prolog plans].

The authors report that LLM+P finds optimal plans in most of its problems while the model alone does not give feasible ones [LLM+P]; that Logic-LM improves on standard prompting by 39.2% and on chain of thought by 18.4% on average over five datasets [Logic-LM]; that SatLM beats PAL by about 26 points on the hard GSM-Sys subset [SatLM]; and that StarCoder+ (15.5B parameters) with LINC beats GPT-4 with chain of thought by 10 points on ProofWriter [LINC]. Read in full, the picture is more qualified: guaranteed-optimal plans in LLM+P hold in three of its seven domains and fail in Floortile; the Logic-LM figures match only for GPT-4 and as relative percentages; SatLM does not win on ordinary GSM; LINC with GPT-4 scores 72.5 on FOLIO against 75.3 for chain of thought. The weak point is the translation: the solver decides well about something that may have been translated badly. These are laboratory logic and planning sets, and the figures are the authors’, not reproduced here.

Propose and criticise

LLM-Modulo is a position paper: the model proposes a plan and a set of external critics checks it; the plan is accepted only if all the hard critics approve, while soft critics may themselves be language-model based [LLM-Modulo]. The authors argue that the model cannot plan or verify itself alone but is a broad, approximate source of knowledge. On travel planning, GPT-4-Turbo goes from 4.4% to 20.6% success (180 validation queries) and GPT-3.5-Turbo from 0 to 5% [LLM-Modulo travel].

Two neighbours move the work into code. In Thought of Search the model writes the search code (successor and goal test) with a person validating it, reaching 100% on four problems with one to three interactions per component [Thought of Search]. Silver and co-authors have GPT-4 write a Python planner for seven PDDL domains; two training tasks are often enough, but in two domains (Miconic and Spanner) the result is very low [Generalized planning]. The limits are that someone must write the critics, absolute success in the travel case stays low, and these are preprints, workshop papers and specific benchmarks.

Planning, and whether models can plan

Automatic planning describes the world as states and actions with preconditions and effects; PDDL is the usual language and HTN planning decomposes tasks into subtasks [LLM+P] [ChatHTN]. In ChatHTN the HTN planner leads and queries ChatGPT only when a method is missing [ChatHTN]; another preprint has an HTN planner generate a verifiable cross-server plan once, executed deterministically by middleware [HTN-MCP].

Whether models plan on their own has been measured repeatedly. In 2023 the authors of PlanBench found about 3% average autonomous success on planning-competition domains [PlanBench] [Planning abilities]; in 2024 they saw a large improvement with o1, still far from saturating the benchmark [o1 on PlanBench], and showed that chain of thought helps only with very problem-specific examples [Chain of Thoughtlessness]. A 2025 study with new tasks and a plan validator reports Gemini 3.1 Pro solving 245 of 360 against 234 for the best reference planner, and GPT-3.5 solving none [Frontier LLMs vs planners]. The readings measure different models and years and do not contradict each other fully. What stands is that a plausible plan is not a valid plan, which is why a validator checks it. Whether the 2025 result holds in other domains is not confirmed.

Policies and checked actions

A recent line puts formal rules between the model and the action. AgentSpec is a rule language with triggers, predicates and enforcement mechanisms [AgentSpec]; Winston, Winston and Just translate policies to SMT-LIB, with a model’s help and human review, and check every tool call with Z3 [Z3 on tool calls]. FormalJudge uses the same machinery as supervision after the fact: the model decomposes the intent into facts and Dafny with Z3 composes the verdict over the finished trajectory [FormalJudge]. Formal-LLM computes with a pushdown automaton which actions are valid at each step, and the model chooses among them [Formal-LLM].

For permissions there are small engines without surprises. OPA uses Rego, a language inspired by Datalog, and is a graduated CNCF project according to its documentation [OPA]. Cedar, from Amazon, separates permissions from code; a forbid always beats a permit, and its engine was modelled in Lean with proved properties. Its paper deals only with authorization and does not mention language models [Cedar]. Mangle extends Datalog but states that it is not an official product [Mangle]. Related preprints enforce a Datalog policy over an event graph [Datalog policy], an SMT authorizer [FAVA], temporal-logic contracts [ContrAgent] and more [Agentao]; they veto or authorize, they do not direct the flow.

Reported results: AgentSpec’s abstract claims over 90% of unsafe code executions prevented (its Table 3 sums to 78.9%, or 91.5% excluding two categories), 0% of dangerous tasks executed in the embedded agent at a cost in safe tasks (58.6% to 54.3%), and 1.4 ms of analysis [AgentSpec]. The Z3 work reports, on 50 airline tasks of τ²-bench, pass^4 rising from 0.34 to 0.46 with the solver [Z3 on tool calls]. FormalJudge reports an average gain over an LLM judge; in its Table 1 the mean over 21 cells is 17.8 points [FormalJudge]. Turning the written norm into a formula is the bottleneck: with rules generated by a model, AgentSpec has 95.56% precision but 70.96% recall on robots, and in driving o1’s rules avoid 5 of 8 scenarios against 100% for hand-written ones [AgentSpec]. No external replications were found.

The model orchestrates, logic computes and records

In VADAOrchestra the language model chooses the tools, plans, replans and writes the answer, while a Datalog± engine (Vadalog) computes over the data. Its logical trace is a record of what was executed, written as rules and reproducible without the model; there are no rules deciding the flow and no permissions [VADAOrchestra]. On 278 questions the authors report an exact-match score of 0.58 for Llama-3.3-70B with the engine against 0.50 with plain tool calling, and 0.65 against 0.63 for GPT-4o, without intervals or seeds [VADAOrchestra].

MCP-Solver exposes MiniZinc, PySAT and Z3 to a model through the Model Context Protocol; the model decides whether to call the solver, and the paper gives transcripts rather than a quantitative evaluation [MCP-Solver]. PrologMCP offers a trace_goal tool that returns the proof tree, but again the model decides what to call [PrologMCP]. An SWI-Prolog MCP package and a community server also exist [SWI-Prolog MCP]. The guarantee is that the result comes from the engine and that the facts and rules used can be seen; the cost is that the model still decides what is asked.

Agent classics

A BDI agent has three boxes: what it believes, what it wants and what it has committed to do. Jason (with AgentSpeak), JADE and 2APL are the best known systems [BDI systems]. The cycle perceives, updates beliefs, picks a plan whose context holds and acts; every action has its reason. The cost is that plans are written by hand and scale badly to many agents. ChatBDI puts a language model inside this cycle as the agent’s “language actuator”; it is an interface, not a task allocator [ChatBDI].

In the situation calculus each action takes the world from one situation to another; Golog writes programs with holes that the reasoner fills by search, and an action happens only if its precondition holds [Golog]. The cost is formalising the world, including what does not change. Contract Net has a manager announce a task, contractors bid and the manager choose; FIPA standardised it with messages such as cfp, propose, accept-proposal and reject-proposal [Contract Net]. The blackboard is a shared space where specialists leave clues [Blackboard]. Their costs are much talk before allocating and a heavy shared ontology.

Rule engines, constraints and verification

Answer Set Programming states what is valid and not how to compute it; clingo returns all the solutions that satisfy the rules and answers UNSAT when there is none [clingo]. Soufflé compiles Datalog to parallel C++ for static analysis [Soufflé]. Rule engines such as Drools, CLIPS and Jess keep facts in a memory and look for matching rules; BPMN draws a process flow and DMN decides with tables [Rule engines]. They read well for people who do not program, and auditing is reading the rule that fired. The cost is a fixed flow and, with hundreds of rules, an order that matters.

For verification, Petri nets and TLA+ explore every state and return the exact path to a deadlock. TraceFix uses TLA+ at design time so that a model repairs agent protocols: verified protocols lowered deadlocks and livelocks from 31.1% to 14.1% over 15 tasks and 270 runs. At run time its monitor checks only the topology and does not enforce step order; it is a single paper without replication [TraceFix]. On the execution side, Temporal runs durable workflows that resume after failures [Temporal] and LangGraph organises steps as a graph with conditional edges, where a code function chooses the next node: a rule or a model call [LangGraph]. Neither writes the rules for you or checks they are good.

Expert systems and explanation

A classic expert system has a rule base, an inference engine and an explanation facility. MYCIN answered WHY (why is this datum being asked) and HOW (how was this subgoal achieved); repeating WHY climbs the chain of reasoning [MYCIN how/why]. MYCIN consults and does not act, so it is not an agent. Explainable BDI agents explain behaviour through beliefs and goals [Explainable BDI]; a 2026 paper adds contrastive explanations and found that explaining did not always help [Contrastive BDI]; AgentSpeaX puts a Prolog-based explainer on Jason agents [AgentSpeaX]; argumentation-based agents explain how and why a desire did or did not become an intention [Argumentation agents].

With language models: one work has GPT-4 phrase the explanation of a legal rule system, where the engine decides [Legal rules + LLM]; another has the model write the Prolog base with a person validating it [LLM writes Prolog]; another generates CLIPS code with agents, without how or why [LLM writes CLIPS]. CogRec lets the Soar architecture decide and calls the model at an impasse; the model’s answer is compiled into a permanent rule and the trace stays symbolic. On three recommendation datasets it reports, for example, HR@10 of 0.3124 on MovieLens-1M against 0.2956 for GPT4Rec; the text has no significance tests or seeds, and it is one agent [CogRec]. The pieces exist separately; no system was found where a rule base, an engine and a how-and-why dialogue are the core that decides, with the model as interface and several agents as sources of facts. That is a search result, not proof of absence.

Trade-offs: what logic gives and what it costs

What it gives

  • Determinism: the same input gives the same output.
  • Auditability: the rule that fired can be read.
  • Explanation: a proof or trace comes with the answer.
  • Verification: properties can be checked on the rules or the model.

What it costs

  • Rigidity: the unforeseen does not fit.
  • Modelling: someone writes and maintains the rules, domains and specifications.
  • Scale: with hundreds of rules, order matters and they tangle.
  • Translation: turning natural language into logic has no guarantee.

There is no winner. Where each works best depends on the problem, on the team that maintains the rules and on the cost of being wrong. As a rough guide drawn from the works above: sharing out work under capacity, skill and cost constraints suits constraint programming (CLP(FD) in Prolog, clingo or Z3); a sequence with preconditions and effects suits a PDDL planner or a search over actions with a validator; who may do what with which resource suits a policy language such as Cedar or OPA, or Datalog; a long flow that must survive failures suits durable execution or a graph of steps, with the logic inside [clingo] [Z3 on tool calls] [Cedar] [OPA] [Temporal] [LangGraph].

What is still not known

Who decides? LLM, logic or both

For each work we asked three questions: who chooses the tool or action that comes next, what role the logic has, and who gives permission. Five arrangements come out, from “the model decides” to “the logic decides”. It is our reading of each text, not a measurement, and one paper can fit two boxes.

Five arrangements of who decides Five stacked boxes from top to bottom, going from the language model decides to the logic decides. 1: the model decides, logic computes or records, for example VADAOrchestra and MCP-Solver. 2: the model translates, a solver resolves, for example LLM+P, SatLM, LINC and Logic-LM. 3: the model proposes, logic vetoes or checks, for example LLM-Modulo, AgentSpec and Z3 on tool calls. 4: logic enumerates, the model chooses, for example Formal-LLM. 5: logic directs, the model fills in, for example ChatHTN and the HTN-MCP preprint. 1 · The model decides; logic computes or recordsVADAOrchestra, MCP-SolverThe trace can be replayed without the model. 2 · The model translates; a solver resolvesLLM+P, SatLM, LINC, Logic-LMOne shot; Logic-LM retries with the solver’s errors. 3 · The model proposes; logic vetoes or checksLLM-Modulo, AgentSpec, Z3 on tool calls, FormalJudgeBefore acting, or afterwards on the finished trajectory. 4 · Logic enumerates; the model choosesFormal-LLMA pushdown automaton lists the valid actions. 5 · Logic directs; the model fills inChatHTN, HTN-MCP (read as abstracts only)
From the model deciding (amber) to the logic deciding (teal). Placement is our reading of each work.

In the first arrangement the model decides whether to introduce new tool calls (section 4.2.7 of VADAOrchestra), the Datalog± engine computes and the trace records [VADAOrchestra]; MCP-Solver decides only whether to call the solver [MCP-Solver]. In the second, translation and solving happen in one shot [LLM+P] [SatLM] [LINC] [Logic-LM]. In the third, hard critics and policy rules veto before acting [LLM-Modulo] [AgentSpec] [Z3 on tool calls] or judge afterwards [FormalJudge]. In the fourth the logic enumerates what is valid and the model picks [Formal-LLM]; Cedar decides permissions only [Cedar]. The fifth is populated mostly by works read only as abstracts: a planner leads and the model fills a gap [ChatHTN] [HTN-MCP] [Blueprint First]. TraceFix uses logic at design time and only watches the topology at run time [TraceFix].

The permission-oriented systems veto and do not direct. No work was found with Golog and a model, ASP task assignment with a model, or commitments with model checking and a model, and none with all four pieces together (logic that decides the flow, permissions, an explanation, and a model as subordinate). Not finding them does not prove they do not exist [Golog] [Datalog policy] [FAVA] [HTN-Orchestrate] [Symbolic planning with LLMs].

References

† read only as an abstract, a catalogue entry or a summary. Items without a link are cited by title because the survey notes give none. Items from general knowledge are marked as such.