Arrochar Frontiers/Project Abductor
Can a machine reason backwards from an outcome?An abductive reasoning engine: start from the ending, work back to every self-consistent set of premises, and mark the ones nobody can yet define.
Most reasoning machines run forwards, from premises to a conclusion. Project Abductor runs the other way. Given an outcome, it works back to every self-consistent set of things that would have to be true, invents a placeholder wherever a needed piece has no definition, and ranks the results by how little they assume. It learns nothing from text. Its only rules are the meanings of the words used to state the problem.
- Field
- Abductive reasoning
- Status
- Engine built, first test run
- Started
- October 2026
- Current model
- Engine version 0.1, 11 October 2026
Mark Macfarlane, principal researcher
Where the problem stands
There are three ways to reason. Deduction runs from premises to a conclusion and is what proofs do. Induction runs from many observations to a general rule and is what statistics and machine learning do. Abduction runs from an observed outcome back to the premises that would best explain it, and is what a detective does. It is the least automated of the three, and it is the one a research programme needs most, because a research programme begins with an outcome it wants and no account of how to reach it.
Language models cannot do this honestly. They are trained on what has been written, so they inherit every assumption the literature carries, including the ones a frontier project exists to question. A model asked why an impossible outcome cannot happen will repeat the reasons the field has already given. That is useful for a survey and useless for finding the gap.
The alternative is symbolic. Abductive logic programming, formalised in the early 1990s, gives a machine a goal, a small set of definitions and a list of contradictions to avoid, and lets it search for the sets of assumptions that would make the goal hold. Where a needed fact has no definition, the machine assumes it and says so. Every conclusion can be traced line by line to a rule a person wrote. Nothing is learned, nothing is statistical, and the machine knows exactly as much about the world as it was told, which is the point.
The one rule the engine keeps
Logic cannot run with no rules at all, because inference is itself a rule. What the engine can do is strip the rules to the meaning of the words in the question and nothing else: no physics, no precedent, no received opinion. Everything domain-specific enters either as a fact the researcher asserts or as a hole the engine is forced to leave open. That is as free of borrowed assumptions as reasoning gets, and it is why the output is a map of holes rather than an answer.
A0, the master hypothesis
Given an outcome and only the meaning of the words used to state it, a symbolic reasoner can enumerate every self-consistent set of premises that would produce that outcome, and the premises it is forced to leave undefined are the open questions of the field, no more and no fewer.
It can be falsified
A0 fails if the engine, run on a problem whose open questions are already documented by people who did not write the engine's rules, returns a minimal explanation whose undefined pieces do not match those questions, or leaves one out. A single clean mismatch on a blind test closes the hypothesis as stated. The engine would still be useful as a consistency checker, and the page would say so, but the claim that it finds the research programme would be withdrawn.
The first test passed, and that is weak evidence
On 11 October 2026 the engine was run against the hypothesis register of Project Chrononaut, with the stages of that project's model encoded as word definitions and its open hypotheses deliberately left undefined. With everyday chronology assumed, no explanation survived, and the one belief every candidate broke on was the belief that project had already named as its master hypothesis. With that belief dropped, exactly one minimal explanation survived, and the pieces it left undefined lined up with the open questions already in the register, adding none and missing none. It also ranked the information-only demonstrator as cheaper than a passenger-carrying one by precisely the questions the register says separate them. The test is encouraging and it proves little: the rules and the register were written by the same hands, so the engine was holding a mirror up to a model, not discovering one.
What the hypothesis commits us to
If A0 holds, every Frontiers project gains an instrument: state the outcome, run the engine, and read the holes before spending anything on construction. If it fails, we learn precisely how a formalisation smuggles assumptions in, which is itself worth knowing. Either way the engine never reasons about the world. It reasons about the argument, and it is the argument we most need checked.
The experiments that can start now
The register is ordered so that the test most likely to kill A0 comes first. Four lines can start now. They need a documented problem the engine's authors have never seen, an off-the-shelf constraint solver, and an afternoon with a language model used strictly as a translator. None needs new theory.
- 01
Run it blind on a register it did not come from
Take a published problem whose open questions are documented by an independent group, encode only the meaning of its terms, and run the engine without reading the questions first. Then compare. Candidates are drawn from physics, medicine and engineering failure analysis, where the literature already lists what is unexplained.
What settles it. Whether the engine finds a field's open questions or merely reflects its author's. This is the test that can falsify A0 outright.
- 02
Replace the hand-built solver with an industrial one
Version 0.1 is a few hundred lines of plain Python, written so that every step can be read. Re-express the same problems in a satisfiability solver and an answer-set solver, and check that all three return the same explanation sets.
What settles it. Whether the results are a property of the method or an artefact of one small program.
- 03
Teach it time and quantity
The engine currently checks orderings for loops and treats every invented placeholder as distinct. Real outcomes need intervals, durations, budgets and the possibility that two unknowns are the same thing. Add arithmetic over the placeholders and re-run the first cases.
What settles it. Whether the explanation sets survive contact with numbers, or whether the clean result depended on the engine not being able to count.
- 04
Measure what translation adds
A researcher states an outcome in prose. Something has to turn that into formal statements, and today that something is a person. Use a language model as a translator only, never as the reasoner, and measure how often the translation adds an assumption the researcher did not make.
What settles it. Whether the front door of the method is as assumption-free as the engine behind it. If translation leaks, A0 holds only for people who can write logic by hand.
The objective
A reasoner that shows every step
The near-term objective is a demonstrator in which anyone can state an outcome, see the complete tree of assumptions the engine built, and read exactly which rule produced each one. No weights, no training, nothing a reviewer cannot follow. If it cannot be followed by a sceptic with a pencil, it has not met the bar.
Three gates decide everything
- 1Does it find a blind register's open questions without being told them? If not, A0 is false as stated and the engine is a consistency checker, not an instrument of discovery.
- 2Do independent solvers agree with it? If not, the first results were an artefact of one program.
- 3Does the prose-to-logic step add assumptions? If it does, the method is only as clean as the person operating it.
Where the project stands
A working engine exists, written on 11 October 2026 in a few hundred lines with no dependencies, no training data and no learning of any kind. It has been run on one problem, Project Chrononaut, with rules written by the same people who wrote that project's model. The result was consistent with A0 and is not evidence for it. It has never been run blind. It cannot count, it cannot tell two placeholders apart, and its search is capped at a depth that suits toy problems. None of this is a reason to stop. All of it is the reason the blind test comes first.
What we publish and what we keep
We publish the method, the master hypothesis and the next experiments. The engine's source and the problem encodings it has been run on stay internal for now, as do the Chrononaut inputs, which belong to that project. If A0 falls on a blind test, this page will say so and the engine will be described as what it then is: a checker, not a finder.
The reading behind the project
Every claim on this page traces to one of the sources below. The published books and papers are public. The two Arrochar documents are internal and are not published.
- 1Public
Abductive Logic Programming, Journal of Logic and Computation 2(6), 719 to 770
A. C. Kakas, R. A. Kowalski and F. Toni, 1992
- 2Public
Abduction in Logic Programming, in Computational Logic: Logic Programming and Beyond
M. Denecker and A. C. Kakas, Springer, 2002
- 3Public
Logic for Problem Solving
R. A. Kowalski, North-Holland, 1979
- 4Public
Collected Papers of Charles Sanders Peirce, volumes 5 and 6 (on abduction as the logic of hypothesis)
C. S. Peirce, Harvard University Press, 1934 to 1935
- 5Arrochar-owned
Abductive reasoning engine, version 0.1, with run outputs
Arrochar Labs, Mark Macfarlane, 11 October 2026. Internal. Not published.
- 6Arrochar-owned
Time Travel Capability Model Hypothesis, version 4.0 (the first test case)
Arrochar Labs, Mark Macfarlane, 13 September 2026. Internal. Not published. See Project Chrononaut.
Working on any of this?
The next experiments need a spectroscopy group, quantum-simulator time, a cryobiology collaborator and a mathematician. If that is you, or you think the hypothesis is wrong and can show why, we want to hear it.