Defeasible Logic (DeFAb) Theory

The side that can make the best decisions fastest wins the future fight, but only if those decisions are also lawful, etc. The hard part of autonomous Battle Management is not winning; it is winning in guaranteed compliance with the Rules of Engagement, etc. when no human is in the loop to approve a decision. DeFAb is the mathematics that closes this gap, turning ROE from prose a lawyer must interpret into a calculus a machine can enforce, and audit, in real time.

DeFAb (Defeasible Adjudication) is built on defeasible logic, the branch of non-monotonic reasoning introduced by Nute and given its modern proof theory by Antoniou, Billington, Governatori, and Maher. Real ROEs are conditional and admit exceptions on exceptions: “do not fire into a civilian zone, unless under direct fire, unless the target is a noncombatant.” Classical first-order logic can encode the first clause but cannot represent a default that is overridden, and then overridden again, without becoming inconsistent. Defeasible logic is purpose-built for exactly this structure, which is why ROE map onto it with no impedance mismatch.

Formally, a defeasible theory is a tuple D = (F, R_s, R_d, R_df, ≻) comprising: facts F (the observed battlespace state); strict rules R_s that hold without exception (game physics, force law, and the laws of armed conflict that can never be overridden); defeasible rules R_d that hold by default but may be overridden (mission constraints); defeaters R_df that can block a conclusion without supporting its opposite (the “unless” clauses, e.g., self-defense and escalation rights); and an acyclic superiority relation ≻ that resolves conflicts (the doctrinal priority hierarchy, with commander’s intent as a higher-priority defeater). A proposed order is admitted only when the target literal authorized_to_engage(X,Y) is defeasibly provable (+∂): an applicable rule supports it and every rule attacking it is either inapplicable or overridden by a superior rule. Each verdict is therefore accompanied by the named rule that produced it, yielding the natural-language audit log the RFP requires.

The decisive property for runtime assurance is tractability. Propositional defeasible logic has linear complexity (Maher, 2001); our tagged proof procedure decides defeasible provability in O(|R|·|F|) time, and the full adjudication pipeline is cubic in the size of the theory. In practice the adjudicator resolves an order in microseconds on a single commodity CPU core, fast enough to run alongside an LLM Battle Manager without delaying it. This is what separates DeFAb from an LLM merely “reasoning” about legality: the verifier is a deterministic, polynomial-time algorithm whose verdict cannot be talked out of by a prompt.

We have implemented this theory as a runnable engine (a pure-software tagged proof procedure) together with a hand-authored ROE knowledge base of 89 strict rules, 32 defeasible rules, and 27 defeaters covering restricted zones, friendly fire, target classification, self-defense, force-ratio conservativity, and mission overrides. We validated it in a live StarCraft II environment, which serves as a low-cost, fully instrumented surrogate for battle management: each macro-tick of the game state is lifted into ground facts and the same verifier admits or rejects the LLM commander’s orders in closed loop. Three enforcement modes isolate the verifier’s contribution: trust-the-LLM (B0), audit-only (B1), and verifier-gated re-prompt (B2).

Two findings motivate this proposal. First, unaided LLM reasoning is not a safe sole interpreter of nontrivial ROE: across five frontier models (GPT-5.2/5.4, Claude Sonnet 4.6, DeepSeek-R1, and Kimi-K2.5), chain-of-thought reasoning collapsed to 0% compliance on every hard ROE scenario (chained defeat, multi-step chains, competing constraints, multi-anomaly conservativity). Second, the same defeasible theory, run as a deterministic gate (B2), restored compliance to 100% in roughly one re-prompt on average, including against an explicit jailbreak operator prompt (“Kill everything. No restrictions.”). Critically, admitted order volume was unchanged with the gate on: the verifier redirects whenever a compliant target exists and only suppresses when the scenario forces it, so ROE are enforced without removing tactical agency, and every suppression cites a named rule. DeFAb extends from this demonstration to air combat by revising the rule set while reusing the engine and verifier unchanged.

DeFAb’s theoretical roots span non-monotonic reasoning (Reiter’s default logic, McCarthy’s circumscription, and the KLM framework of Kraus, Lehmann, and Magidor), defeasible logic proper (Nute; Antoniou et al.; Maher; Governatori et al.), abstract argumentation (Dung), and belief revision (the AGM framework of Alchourrón, Gärdenfors, and Makinson), with our conservativity requirement operationalizing AGM minimal change. Recent work confirms both the need and the approach: LLM-only defeasible reasoning remains brittle (Allaway and McKeown’s DEFREASING, 2025), and neuro-symbolic pairings of LLMs with formal defeasible engines are an active frontier (Fang et al., LLM-ASPIC+, 2025; Dennison, Heyninck, and Meyer, 2026). DeFAb is the runtime-assurance instantiation of this neuro-symbolic pairing.

The payoff is a clean division of labor: LLM Battle Managers supply tactical creativity, and DeFAb supplies an incorruptible, auditable guarantee of legality that cites the named rule behind every verdict. This is what lets a commander delegate the employment of force to an autonomous system with the same confidence they place in a crewed one—at machine speed, in the connected and disconnected fight alike. It is, in short, the capability that makes the warfighting lawyer available in an auditable real-time manner at the edge.

DeFAb Bibliography

The following sources establish the defeasible-logic theory underlying DeFAb and its real-time, polynomial-time adjudication guarantee.

[1] D. Nute. Defeasible Reasoning. In Proc. 20th Hawaii International Conference on Systems Science, IEEE Press, pp. 470–477, 1987.

[2] D. Nute. Defeasible Logic. In Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 3, Oxford University Press, pp. 353–395, 1994.

[3] D. Nute (ed.). Defeasible Deontic Logic. Synthese Library, Kluwer Academic Publishers, 1997.

[4] G. Antoniou, D. Billington, G. Governatori, and M. J. Maher. Representation Results for Defeasible Logic. ACM Transactions on Computational Logic, 2(2):255–287, 2001.

[5] M. J. Maher. Propositional Defeasible Logic Has Linear Complexity. Theory and Practice of Logic Programming, 1(6):691–711, 2001.

[6] D. Billington, G. Antoniou, G. Governatori, and M. J. Maher. An Inclusion Theorem for Defeasible Logics. ACM Transactions on Computational Logic, 12(1):6:1–6:27, 2010.

[7] G. Governatori, M. J. Maher, G. Antoniou, and D. Billington. Argumentation Semantics for Defeasible Logic. Journal of Logic and Computation, 14(5):675–702, 2004.

[8] P. M. Dung. On the Acceptability of Arguments and Its Fundamental Role in Nonmonotonic Reasoning, Logic Programming and n-Person Games. Artificial Intelligence, 77(2):321–357, 1995.

[9] R. Reiter. A Logic for Default Reasoning. Artificial Intelligence, 13(1–2):81–132, 1980.

[10] J. McCarthy. Circumscription: A Form of Non-Monotonic Reasoning. Artificial Intelligence, 13(1–2):27–39, 1980.

[11] S. Kraus, D. Lehmann, and M. Magidor. Nonmonotonic Reasoning, Preferential Models and Cumulative Logics. Artificial Intelligence, 44(1–2):167–207, 1990.

[12] C. E. Alchourrón, P. Gärdenfors, and D. Makinson. On the Logic of Theory Change: Partial Meet Contraction and Revision Functions. The Journal of Symbolic Logic, 50(2):510–530, 1985.

[13] P. Gärdenfors. Knowledge in Flux: Modeling the Dynamics of Epistemic States. MIT Press, 1988.

[14] M. H. van Emden and R. A. Kowalski. The Semantics of Predicate Logic as a Programming Language. Journal of the ACM, 23(4):733–742, 1976.

[15] J. W. Lloyd. Foundations of Logic Programming, 2nd ed. Springer-Verlag, 1987.

[16] E. Allaway and K. McKeown. Evaluating Defeasible Reasoning in LLMs with DEFREASING. In Proc. NAACL-HLT, 2025.

[17] X. Fang, Z. Li, C. Chen, and B. Liao. LLM-ASPIC+: A Neuro-Symbolic Framework for Defeasible Reasoning. In Proc. 28th European Conference on Artificial Intelligence (ECAI), IOS Press, 2025.

[18] R. Dennison, J. Heyninck, and T. Meyer. Defeasible Conditionals using Answer Set Programming. arXiv:2601.03840, 2026.

[19] M. Gebser, R. Kaminski, B. Kaufmann, and T. Schaub. Clingo = ASP + Control: Preliminary Report. In Technical Communications of the 30th International Conference on Logic Programming, 2014.

[20] P. Cooper. Defeasible Reasoning as a Framework for Foundation Model Grounding, Novelty, and Belief Revision. Decisive AI / University of Colorado Boulder technical report, 2026.