{"path":"research/tools-for-checking-inferences/report-engines-per-kind.md","content":"# Report: symbolic engines for checking each kind of inference\n\n*A research helper's report (Sonnet 5.5, 2026-10-24), saved verbatim on arrival, as it returned it. Brief:\nwhich maintained engines implement the logic of each kind the project rules on (normic, statistical,\ninduction, abduction, analogy), so deterministic code can compute what a structured inference implies; and\nwhat is measured about a model translating into them. Numbers and links are the helper's, with its read\ntags; none was re-checked when this was saved. Home: `../tools-for-checking-inferences.md`.*\n\n---\n\n# Symbolic engines for checking the inference kinds (normic, statistical, induction, abduction, analogy)\n\nDate of research: 2026-10-24. No files written, nothing installed, no downloaded code run. Read-status tags: [FULL] = read the page or README text myself; [PART] = read through a summarising fetch of part of a page; [ABSTRACT] = abstract page only; [SECONDARY] = search snippet or a third party; [META] = registry metadata (PyPI JSON or GitHub API) read directly. Rule-with-exception snippets marked \"own illustration\" are my own, written from general knowledge of the languages and not run.\n\n## Bottom line\n\n1. For the normic kind there are three workable routes: clingo (ASP, Python-native), s(CASP) (returns justification trees), and ASPIC+ engines (PyArg in Python, Arg2P on the JVM). All three represent \"rule plus exception\" natively.\n2. The statistical kind has good inference engines (ProbLog, cplint, pgmpy). It has no software for the reference-class problem; I found none.\n3. For induction, FOLD-R++ and FOLD-RM learn \"default plus exceptions\" rules directly. Popper learns rules from examples, but I did not verify that it learns exceptions.\n4. For abduction there is no packaged \"enumerate rival explanations\" tool I could confirm. The standard method is a choice-rule encoding in clingo, which is my own knowledge and unverified here. DeFAb (2026) publishes polynomial-time checks for derivation, conservativity and minimality that look borrowable.\n5. For analogy there is no maintained Python structure-mapping engine. SME exists only in Common Lisp and Clojure. The inference kind as you define it, \"alike in R, so alike in Q\", reduces to checking a rule and a fact, so it needs no analogy engine.\n6. I found no paper measuring how often an LLM correctly writes rule-with-exception structure into s(CASP), ProbLog or ASPIC+. The closest evidence is end-task accuracy for LLM-to-ASP and LLM-to-ProbLog (section 7).\n\n## 1. Normic and defeasible rules\n\n**clingo** (Potassco). https://github.com/potassco/clingo ; `pip install clingo`.\n- Kind: ASP, stable-model semantics; defaults and exceptions via negation as failure, plus enumeration of models and brave/cautious consequences.\n- Input: ASP text. Own illustration: `flies(X) :- bird(X), not ab(X). ab(X) :- penguin(X).`\n- Output: answer sets via a Python API. Justification only through add-ons: `xclingo` 2.0b24 (MIT, 2026-05-15) and `clingexplaid` 1.5.1 (MIT, 2026-10-04) on PyPI [META].\n- Maintenance: PyPI 5.8.2 released 2026-08-14; repo pushed 2026-10-24; MIT [META].\n- Verdict: best fit as the checking core. Python-callable, actively maintained, and it can compute whether an exception defeats a rule for a given case.\n\n**s(CASP)**, SWI-Prolog port: https://github.com/SWI-Prolog/sCASP [FULL README].\n- Kind: query-driven ASP with constraints. It returns bindings, a model and a justification tree (query operators `?-+`, `?++`; `scasp/2` returns model and tree as Prolog terms).\n- Input: Prolog-style ASP with `not`. Same default pattern as above, via `not abnormal(X)`. Exceptions are encoded with negation as failure, and the compiler builds a \"not exception\" predicate [SECONDARY, search snippet].\n- Python: no s(CASP) Python package found. `janus-swi` 1.5.3 (BSD-2, 2026-06-24) [META] is the generic SWI-Prolog-to-Python bridge, not verified here to drive s(CASP). Subprocess calls to the `scasp` executable also work. The README says SWI-Prolog 8.5.6 or later; install is `make` or `pack_install(.)` from the repo directory. I did not verify a registry pack name.\n- Maintenance: repo pushed 2026-10-18; Apache-2.0 [META].\n- Verdict: best fit if you want a human-readable proof tree showing why an exception does or does not fire. The cost is an SWI-Prolog dependency.\n\n**PyArg** (Odekerken, Borg, Berthold; Utrecht). https://github.com/DaphneOdekerken/PyArg ; `pip install python-argumentation` (PyPI 2.0.2, 2024-02-02, repo pushed 2024-09-16, MIT) [META].\n- Kind: ASPIC+ and abstract argumentation (also ABA, per the docs landing page [PART]).\n- Input, from the ASPIC+ examples page [PART]: Python objects. Literals have contraries. `StrictRule('s1', {t, q}, -p)` and `DefeasibleRule('d1', {~s}, t)` are rule constructors. The examples page also adds a literal for each defeasible rule and maps it to that rule's negation (an undercutter). A theory is `ArgumentationTheory(system, axioms, ordinary_premises)`.\n- Output: `all_arguments`, `all_attacks`, `undermines(...)`, abstract framework, `get_grounded_extension`, `get_complete_extensions`. Default preference ordering is last-link elitist [PART]. I could not confirm the \"explanation functions\" the 2022 demo paper advertises beyond the search summary [SECONDARY].\n- Verdict: closest to Deliberus's own shape (rule claim, exception claim as attacker, extension as outcome). Python-native. Not updated since 2024.\n\n**Arg2P** (tuProlog, Bologna). https://github.com/tuProlog/arg2p-kt ; JVM via Maven Central, Node via npm; MIT; repo pushed 2026-10-23 [META, README FULL].\n- Kind: ASPIC+ with burden of persuasion, preferences, labellings.\n- Input, from the wiki syntax page [PART]: `r1 : bird(X), ~(penguin(X)) => flies(X).`, `f1 :=> bird(tweety).`, `f2 :=> penguin(tweety).`. Undercutter: `r1 : some_other => undercut(r0).` Preference: `sup(r1, r2).` Tweety is a penguin, so `flies(tweety)` is OUT.\n- Verdict: the clearest rule-plus-exception syntax found. Not Python; call it through the JVM or a subprocess.\n\n**TweetyProject** (Java). https://github.com/TweetyProjectTeam/TweetyProject ; LGPL-3 per its README (GitHub's API says GPL-3.0; the README says versions from 1.6 are LGPL; I report the discrepancy); pushed 2026-10-24; API docs version 1.31 [README FULL; META].\n- The repo tree contains modules `arg-delp`, `arg-aspic`, `arg-aba`, `arg-prob`, `arg-explanations`, `lp-asp`, `causal`, `logics-pcl`, `logics-mln` [GitHub directory listing].\n- Verdict: the widest single library (DeLP and ASPIC+ in one place), but Java only. I did not test the CLI module for use from Python.\n\n**SPINdle**. Propositional defeasible logic, Java, LGPL-3 per the CSIRO page; a mirror lists 2.2.4 [SECONDARY]. I did not confirm that the official site is live or the release date. Verdict: usable only if you want Nute-style defeasible logic; no maintenance evidence found.\n\n**ErgoAI / Flora-2**. Flora-2 is no longer developed. ErgoAI is its successor, Apache-2.0, development moved to GitHub in April 2023 [SECONDARY]; the ErgoEngine repo was pushed 2026-10-05 [META]. Defeasibility is built on well-founded semantics with rule priorities [SECONDARY]. Its releases page is empty and I could not confirm a Python interface or syntax. Verdict: skip unless you want an F-logic frame language.\n\n**Not found**: DeLP as a standalone maintained engine (only inside Tweety); a TOAST source release (its site says \"Coming soon\" [SECONDARY], and it is a web tool with a REST API); ASPARTIX and ConArg were not checked (they handle abstract frameworks only, not rules with exceptions).\n\n## 2. Statistical rules\n\n**ProbLog**. https://github.com/ML-KULeuven/problog ; `pip install problog` (2.3.0 released 2026-09-09; Apache-2.0; repo pushed 2026-09-14) [META; README FULL].\n- Kind: probabilistic logic programming; marginals given evidence, weighted model counting.\n- Input, own illustration: `0.33::rain :- red_sky.` with `query(rain).`; the stated proportion is the clause weight.\n- Output: probabilities for queries. Verdict: best fit for \"the rule states a proportion, and the case belongs to its class\". It computes what follows, but it does not decide whether the class fits the case.\n\n**cplint** (Riguzzi, SWI-Prolog). https://github.com/friguzzi/cplint ; pushed 2026-08-30; licence field not detected by GitHub [META]. PITA reasoner supports MAP/MPE inference, benchmarked against ProbLog in Bellodi et al., TPLP 2020 [ABSTRACT]. Verdict: Prolog-side alternative.\n\n**pgmpy**. `pip install pgmpy` (1.1.2, 2026-04-30, MIT) [META]. Bayesian networks and causal inference in Python. I did not verify its MAP-query API here. Verdict: fine if a case is better modelled as a network than as clauses.\n\n**Probabilistic Soft Logic**. https://github.com/linqs/psl (Apache-2.0, pushed 2024-06-10); `pslpython` 2.4.1 released 2026-10-06 [META]. Soft truth values, not proportions. Verdict: poor fit.\n\n**Reference-class problem.** I found theory only (Kyburg-style direct inference; Thorn on specific classes; Chiang and Poole's latent-property alternative) and no software [SECONDARY, search snippets]. The check \"pooled cases give the stated band, and this case belongs to the class\" therefore stays your own code. In this project that is already `cases.py`-style Beta arithmetic. The class-membership half is a fact check the LLM must state and a human must contest.\n\n## 3. Induction\n\n**FOLD-R++ / FOLD-RM**. https://github.com/hwd404/FOLD-R-PP ; `pip install foldrpp` (0.0.2, 2023-11-26; GitHub shows no licence) and https://github.com/hwd404/FOLD-RM (`pip install foldrm`, MIT, pushed 2024-05-03) [META; README FULL for FOLD-R-PP].\n- Kind: learns default rules with exceptions from tabular examples (binary for R++; multi-class for RM). Pure Python.\n- Output, from the README: `model.asp()` prints rules such as `label(X,'ckd') :- sc(X,N1), N1>1.2.` The paper description is `label(X,Class) :- Conditions(X), not Exceptions(X)` with exceptions learned by swapping example classes recursively [SECONDARY, search snippet of arXiv 2202.06913 and 2506.19573]. The `ratio` parameter is the threshold of false-positive (exception) to true-positive examples a rule may imply.\n- Verdict: the right tool for \"do the cases pooled under a rule support it, and which cases are the exceptions\". It needs tabular features, not graph claims, so you must flatten cases into rows. Not touched since 2024.\n\n**Popper** (Cropper, Helsinki). https://github.com/logic-and-learning-lab/Popper ; MIT; pushed 2026-10-22 [META; README FULL]. Install: clone, then `uv run popper.py <dir>`; needs SWI-Prolog, GNU coreutils, uv. The PyPI package named `popper` is an unrelated project [META]. Input is three files: positive/negative examples (`pos(grandparent(ann,amelia)).`), background knowledge, and a bias file (`head_pred`, `body_pred`). Supports a noisy mode (MDL cost) and recursion. I did not verify that it learns negation or exceptions. Verdict: learns rules from cases. It tells you whether some rule fits, not whether the rule you wrote holds.\n\n**ILASP**. Learns ASP including defaults and exceptions per its paper [SECONDARY; arXiv 2005.00904]. Releases at https://github.com/ilaspltd/ILASP-releases (last push 2024-11-11; no licence detected); the download page says version 4.0.0 is current [SECONDARY]. Licence terms not verified; the page failed a certificate check when I fetched it. Verdict: powerful, closed binary, unclear terms; second choice after FOLD.\n\n**Metagol**: BSD-3, last push 2021-09 [META]. **Aleph**: not verified (no maintained repo found). Both are stale relative to Popper.\n\nLLM + ILP evidence [SECONDARY, search snippets only]: a 2025 paper on rule induction found Popper sub-optimal and ILASP unable to finish within the time limit as drop-in backends for an LLM pipeline (arXiv 2509.21874); \"Reason Popper-ly\" (2607.23019) uses Popper to patch in-context reasoning. An LLM-as-inducer paper (arXiv 2408.16779) reports the largest LLMs competitive with a state-of-the-art ILP baseline, with long predicate chains harder than theory complexity [ABSTRACT; ILP system not named].\n\n## 4. Abduction\n\n- No packaged abduction tool with a Python API was confirmed. Closest hits: xasp (https://github.com/alviano/xasp, pushed 2026-01-11; explains why atoms hold in an answer set, so explanation of a model, not abduction); Caroprese, Zumpano and Bogaerts, \"Computing Abductive Explanations\" (IEEE Intelligent Systems 2022), which rewrites an abductive theory and observation into a disjunctive program whose stable models are the explanations; no released tool found [SECONDARY].\n- Method, own knowledge, unverified here: in clingo, declare the candidate explanations as choice rules, add a constraint that the observation must follow, and enumerate all models. Each model is one explanation; minimality is checked with cardinality or subset-minimal enumeration. The rival-naming requirement of your abduction kind corresponds to the model set.\n- DeFAb (arXiv 2606.18557, MIT code and data; [ABSTRACT]): a benchmark for defeasible abduction where each proposed hypothesis must pass polynomial-time checks for valid derivation, conservativity and minimality, i.e. override a default without breaking unrelated expectations. Its solver is rule-based and resolves every instance in under 50 microseconds. Best frontier-model score reported is 65%, falling to 23.5% under worst-case-of-four-renderings evaluation. Verdict: a template for your \"a named rival actually explains the observation\" check, at least.\n- Probabilistic abduction: MAP/MPE in cplint/ProbLog (above).\n\n## 5. Analogy\n\n- **SME**: Common Lisp original (Northwestern QRG, SME version 4 with source) [SECONDARY]; Case Mapper GUI around it [SECONDARY]. **SME-clj**: Clojure port, MIT, last push 2011 [META]. No maintained Python implementation found; the GitHub repo `yutaozhou/SME` is unrelated spectroscopy software [META]. PyPI search for obvious names returned nothing [META].\n- Recent hybrid: YARN (arXiv 2603.29997, 2026) has an LLM split narratives into units, abstract them, and hand them to a \"mapping component\"; abstractions improved performance over end-to-end LLM baselines; the implementation behind the mapping component is not named in the abstract [ABSTRACT].\n- Fit: SME aligns relational structure between two domains. Your kind needs only the stated respect R as a rule and the target's possession of R as a fact. That is checkable with clingo or ProbLog, so SME adds nothing unless you want the engine to find the mapping instead of the LLM stating it.\n\n## 6. Which engine is checking what\n\n| Your kind | What to check | Engine |\n|---|---|---|\n| Normic | exception claim defeats the rule for this case | clingo or Arg2P/PyArg; s(CASP) for a readable justification |\n| Statistical | stated proportion, query given case | ProbLog; band arithmetic is your own code |\n| Induction | cases filed under the rule fit the stated band; wider rule | FOLD-R++/RM for default-with-exceptions; plain arithmetic for the band |\n| Abduction | named rival entails the observation, minimal | clingo enumeration; DeFAb-style checks |\n| Analogy | R holds of target; \"alike in R, alike in Q\" | a rule in any of the above |\n\n## 7. LLM-to-engine translation: what has been measured\n\n- **LLM+ASP** (Ishay and Lee, arXiv 2604.27960, ACL 2026 Findings) [PART: HTML, first 100,000 of 138,479 characters, read through a summariser]. Engine: clingo 5.8.0. Six benchmarks: ZebraLogic XL and XXL, SudokuBench, Mystery Blocksworld, MultiLogicNMR (200 problems), BoardgameQA (200). Models: Gemini 2.5 Pro and Flash, o4-mini, DeepSeek R1-0528 and V3; means of 3 trials. Average accuracy 51.3% baseline against 78.0% with LLM+ASP and a compact reference (Table 1); 54.6% without solver-feedback revisions against 78.0% with them, 2.18 revisions on average (Table 3); against LLM+SMT with no reference: overall ASP 72.1% against SMT 58.2%, MultiLogicNMR skeptical 92.9% against 35.8%, credulous 84.3% against 35.0%, BoardgameQA 82.1% against 60.1%; SMT wins on ZebraLogic and Mystery Blocksworld (Table 6). These are end-task accuracies, not rule-translation fidelity, so they do not say how often an exception was written correctly. The abstract states that stable-model semantics let LLMs express defaults and exceptions [ABSTRACT]. Takeaway for you: solver feedback in a loop does most of the work, so run the checker and send its complaint back to the writer.\n- **STAR** (arXiv 2302.03780, 2023): LLM extracts predicates, s(CASP) reasons, with a proof tree [ABSTRACT]. No numbers in the abstract; no measured translation accuracy found.\n- **QUITE** (arXiv 2410.10449) [PART: HTML, summariser; the summariser said the column order was inferred from the garbled table header and text]. Table 4, numeric premises: GPT-4-Turbo writing ProbLog zero-shot 19.2% correct, 4.8% wrong, 76.1% error (no valid numeric answer); fine-tuned Mistral-7B 54.5 ± 4.8 correct, 16.9 ± 5.1 wrong, 28.6 ± 7.1 error. For premises phrased in words of estimative probability: GPT-4-Turbo 0.4 / 8.7 / 90.8; fine-tuned Mistral-7B 1.3 / 32.8 / 65.9; Mistral-7B given already-parsed premises (\"oracle\") 87.3 correct. The abstract says logic-based models beat out-of-the-box LLMs on every reasoning type [ABSTRACT]. Takeaway: zero-shot writing of valid ProbLog failed three times in four on numeric premises, and gave a valid answer about one time in ten on verbal-probability premises.\n- **BLInD** (arXiv 2402.09614): prompting that maps problems to Python, probabilistic algorithms or probabilistic logic programming improves accuracy across LLMs [ABSTRACT]. No figures read.\n- **LLM-ASPIC+** (talk abstract, Univ. Bamberg): 87.1% on BoardGameQA-2 and 82.6% on BoardGameQA-3 [SECONDARY]. It scores answering questions over defeasible rules, not translation. I could not find the arXiv paper.\n- **Legal text to Defeasible Deontic Logic** (arXiv 2506.08899) [ABSTRACT]: generated formalisations \"align closely\" with expert ones on the Australian Telecommunications Consumer Protections Code; the abstract names no engine and gives no numbers.\n- **Exception chain collapse** (arXiv 2607.23386) [ABSTRACT]: frontier LLMs misjudge \"required UNLESS B, UNLESS C overrides B\" chains (225 scenarios, four domains); an SMT execution layer fed rules written by an LLM scored 20/20 on a 20-scenario adversarial set, where one of four frontier configurations also scored 20/20 and the other three failed the same coverage-gap edge case; 949 held-out LegalBench cases, p ≤ 0.003 (combined McNemar). Takeaway: it is evidence that exception chains are where unchecked LLM judgment breaks, and that the writing step then carries the uncertainty. The solver is not named in the abstract.\n- **PYTHEN** (arXiv 2603.15317) [ABSTRACT]: Python framework for defeasible legal rules with exceptions; no evaluation numbers, target solver not stated.\n- **Gap**: no measurement of LLM translation correctness into s(CASP), ASPIC+ or DeLP input found. Everything above is end-task accuracy or an abstract without numbers.\n\n## 8. Ranked shortlist\n\n1. **clingo** (`pip install clingo`, optionally `pip install clingexplaid xclingo` for explanations). Covers normic checks, induction-side exception checks and abduction enumeration in one Python-callable engine, and the one directly relevant measurement (LLM+ASP) used it with a solver-feedback loop.\n2. **ProbLog** (`pip install problog`). The only maintained, Python-native engine that evaluates a stated proportion given evidence; pair it with your own band arithmetic and keep the reference-class judgment explicit as a claim.\n3. **PyArg** (`pip install python-argumentation`). Python-native ASPIC+ that matches your claim graph (rule, exception as undercutter, extension as verdict). Alternative: **s(CASP)** if you want a justification tree and accept SWI-Prolog (`swipl` plus `pack_install(.)` from a clone of https://github.com/SWI-Prolog/sCASP; call from Python with `janus-swi`, not verified for s(CASP)). Arg2P is the clearest syntax but JVM-only.\n\nWorth trying beside the shortlist for the induction kind: `pip install foldrm` (or `foldrpp`).\n\nSources: https://github.com/potassco/clingo · https://github.com/SWI-Prolog/sCASP · https://github.com/DaphneOdekerken/PyArg · https://daphneodekerken.github.io/PyArg/aspic_examples.html · https://github.com/tuProlog/arg2p-kt · https://tuprolog.github.io/arg2p-kt/docs/syntax/ · https://github.com/TweetyProjectTeam/TweetyProject · https://github.com/ML-KULeuven/problog · https://github.com/friguzzi/cplint · https://github.com/hwd404/FOLD-R-PP · https://github.com/hwd404/FOLD-RM · https://github.com/logic-and-learning-lab/Popper · https://github.com/ilaspltd/ILASP-releases · https://github.com/svdm/SME-clj · https://arxiv.org/abs/2604.27960 · https://arxiv.org/abs/2410.10449 · https://arxiv.org/abs/2402.09614 · https://arxiv.org/abs/2302.03780 · https://arxiv.org/abs/2606.18557 · https://arxiv.org/abs/2607.23386 · https://arxiv.org/abs/2603.15317 · https://arxiv.org/abs/2506.08899 · https://arxiv.org/abs/2603.29997 · https://arxiv.org/abs/2408.16779\n"}