{"path":"research/tools-for-checking-inferences/report-parsers-to-logic.md","content":"# Report: deterministic software that turns sentences into logic, for checking an inference's form\n\n*A research helper's report (Sonnet 5.5, 2026-10-24), saved verbatim on arrival, as it returned it. Brief:\nwhich parsers, controlled languages and natural-logic provers could check that a case is the rule's\ncondition said of the term, and the conclusion its outcome, more robustly than exact strings and without a\nmodel's judgement; English and Swedish. Numbers and links are the helper's, with its read tags; none was\nre-checked when this was saved. Home: `../tools-for-checking-inferences.md`.*\n\n---\n\nREPORT: deterministic / symbolic NL tools for checking \"case = rule condition with term put in; conclusion = rule outcome with term put in\"\n\nSource tags: [FULL] I read the paper text or README myself in this run. [PART] I read an excerpt or table via a fetch tool. [ABSTRACT] abstract or search snippet only. [SECONDARY] aggregator, PyPI, wiki or search summary. \"Not found\" means I looked and did not find it. I wrote no files and ran no downloaded code (I only piped PDFs through pdftotext).\n\nBOTTOM LINE (3 lines)\n1. No off-the-shelf tool does \"is sentence A the instance of template B with term t\" end to end. The nearest ones are theorem provers for NLI (LangPro, MonaLog, NeuralLog) and UD-to-DRS parsers (UD-Boxer). All are English-only or English-first.\n2. The only Swedish-capable deterministic path is Universal Dependencies. A UD parser (Stanza or spaCy) gives a structure that code can compare. UD-Boxer shows the DRS route over UD works for German, Italian and Dutch with a few language-specific rules; Swedish would need those rules written.\n3. Logic-based provers are high-precision, low-recall (precision about 97.7%, recall about 58 to 62% on SICK, no abduction, [FULL]). That is the profile of a gate that refuses unless proven, but it also means they would refuse roughly 40% of true paraphrases on SICK-style text.\n\nNOT FOUND, and it matters: no measurement of LangPro, MonaLog, NeuralLog or UD-Boxer on HANS-style or any other near-miss/adversarial set. Whether their proofs resist the \"near-miss wording reads as entailment\" failure of NLI cross-encoders is therefore unmeasured. Their mechanism (a proof must exist; no overlap heuristic) argues for resistance, but that is my inference, not a result.\n\n1. NATURAL-LOGIC AND TABLEAU PROVERS\n\nLangPro (Abzianidze). https://github.com/kovvalsky/LangPro ; paper https://arxiv.org/abs/1708.09417 (EMNLP 2017 demo); learning-as-abduction paper https://arxiv.org/abs/2010.15909\n- Input: premise sentence(s) plus hypothesis, English. Pipeline: CCG parser (C&C, EasyCCG or depccg) -> logical-form generator with aligner -> tableau prover for natural logic, implemented in Prolog. Output: entailment, contradiction or neutral, with a proof tree.\n- Language: English only. Last release/commit: not shown on the README page (281 commits on the `nl` branch). Latest paper I read is 2020.\n- Numbers: 2017 paper, FraCaS (commonly used sections) 87% and SICK 82.1% accuracy; about 100 SICK problems in 3.5 s given ready CCG derivations, 8 x 2.4 GHz CPUs [FULL]. 2020 paper, Table 3, SICK test, no abduction: precision 97.6 to 97.8, recall 58.0 to 62.2, accuracy 81.1 to 83.0 depending on parser; with abduction: precision 94.3 to 94.9, recall up to 67.9, ensemble of three parsers 84.4% accuracy [FULL]. Dropping WordNet relations cost 2.44% accuracy, so lexical synonymy knowledge is what makes paraphrase work [FULL]. The author notes SICK gold labels are noisy, so true precision may be higher [FULL].\n- Verdict: the best symbolic candidate for \"does sentence A entail sentence B\" (run twice: case entails instantiated condition, instantiated outcome entails conclusion). Cost: Prolog + Perl + a CCG parser install, English only, and about 40% recall loss on SICK-style paraphrase (not measured on our near-identical sentence pairs, where recall may be higher). Strengthens the slot check; does not replace the term-not-in-rule and known-earlier-sentence checks.\n\nMonaLog (Hu, Chen, Kyle, Moss). https://arxiv.org/abs/1910.08772 ; polarity tool https://github.com/huhailinguist/ccg2mono\n- Monotonicity-based natural logic engine over CCG trees, English. SICK test: precision 83.75, recall 70.66, accuracy 77.19 (uncorrected labels); on the corrected SICK 89.91 / 74.23 / 81.66 [PART, table read via ar5iv, cross-checked against Abzianidze's Table 3 row 83.8/70.7/77.2 [FULL]].\n- Verdict: lighter than LangPro, but lower precision. Not preferable for a gate.\n\nNeuralLog (Chen, Gao, Moss, *SEM 2021). https://arxiv.org/abs/2105.14167 ; https://github.com/eric11eca/NeuralLog ; polarity tool Udep2Mono https://github.com/eric11eca/Udep2Mono\n- Hybrid: monotonicity inference engine with a neural phrase aligner and beam search. SICK accuracy 90.3 [FULL]; MED 93.4 [SECONDARY]; removing the syntactic-variation module drops SICK accuracy by 18.9 points [FULL]. English only (Stanza v1.2+ with a replacement English parser model). Install per README: git clone, pip install -r requirements.txt, then swap Stanza's depparse model. Last commit year not shown.\n- Verdict: reject for our purpose. It reintroduces neural fuzziness exactly where you do not want it. Useful only because its Udep2Mono shows a UD-tree-based monotonicity marker exists (English only).\n\nNatLog (Stanford) was not examined. Udep2Mono's abstract says it outperformed NatLog and ccg2mono on a small dataset [ABSTRACT].\n\n2. SEMANTIC PARSERS TO LOGIC / DRS\n\nUD-Boxer (Poelman, van Noord, Bos, COLING 2022). Paper https://aclanthology.org/2022.coling-1.367 ; code https://github.com/WPoelman/ud-boxer (mirror https://github.com/adaamko/ud-boxer)\n- Input: a sentence, or an existing UD parse in CoNLL format. Output: a DRS in Simplified Box Notation (variable-free), Penman or PNG. It is rule-based: 19 language-independent graph-transformation rules plus 4 language-specific rules per language, written in GREW, over any off-the-shelf UD parser (Stanza and Trankit tested) [FULL].\n- Languages: English, German, Italian, Dutch (the PMB languages). Swedish not covered; a Swedish port would mean writing the language-specific rules and accepting no word-sense disambiguation.\n- Numbers (PMB 4.0, macro F1, Smatch-style) [FULL, Table 2]: English about 82 (Stanza); German 77 to 78; Italian 76 to 79; Dutch about 75.5. A neural parser trained on all data gets 92.5 on English but 71.6 to 75.4 elsewhere. The authors state the rule-based parser does not hallucinate output. Ill-formed DRS rate for UD-Boxer was 0.3% or less on English.\n- Install per README: opam-install grew.1.8.1, grewpy.1.8.0, libcaml-grew.1.9.2 (newer GREW versions break it), then pip install -r requirements/requirements.txt [FULL]. Last commit year not shown.\n- Verdict: strongest bilingual-leaning structured option. DRS graphs make negation and quantifier scope explicit, which plain dependency triples miss. Cost: roughly 82 F1 on English means about 18% of the graph is off even before comparison, and a Swedish port needs real work.\n\nBoxer / ccg2lambda. Boxer (Bos) builds DRSs from CCG derivations with lambda calculus and ships with the C&C tools; neural DRS parsers (van Noord et al., Bos 2023 Sequence Box Notation, https://arxiv.org/abs/2404.12698) exist but are neural and English-first [ABSTRACT/SECONDARY]. ccg2lambda https://github.com/mynlp/ccg2lambda: CCG -> lambda terms -> Coq for entailment; English (C&C) and Japanese (Jigg); the README itself says the install guide and Dockerfile are not maintained. Its SICK result appears in Abzianidze's table as precision 97.1, recall 63.6, accuracy 83.1 [FULL, secondary row]. I did not find a FraCaS overall number in this run. Verdict: not recommended; LangPro dominates it for our need and ccg2lambda is poorly maintained.\n\ndepccg (CCG parser used by LangPro and ccg2lambda): English and Japanese; CCGbank unlabelled/labelled F1 94.0/88.8 (basic) and 94.98/90.51 (ELMo variant) [SECONDARY, PyPI page]; last release 2.0.3, July 2021 [SECONDARY]. Install: pip install cython numpy depccg.\n\nA newer typed UD semantics, UD Type Calculus (https://arxiv.org/abs/2403.01187, code https://github.com/McGill-NLP/ud-to-meaning), claims language-independent logical forms from UD and \"comparable\" meanings to its baseline; no scores on the page [ABSTRACT]. Not tested; worth a look only if UD-Boxer disappoints. UDepLambda (Reddy et al. 2017, https://arxiv.org/abs/1702.03196, https://github.com/sivareddyg/UDepLambda): UD to lambda logical forms for English, German and Spanish, evaluated on Freebase QA, not entailment, and depends on Stanford CoreNLP [ABSTRACT/SECONDARY]. Not suitable.\n\nAMR: SPRING-type parsers reach about 83 to 86 Smatch on AMR 3.0, 73.7 on New3, 77.3 on Little Prince [SECONDARY]. AMR parsers are neural, English-only, and I found no AMR-to-logic entailment checker in this run. Verdict: not useful here.\n\nA 2025 test of neural semantic parsers through a first-order prover (https://arxiv.org/abs/2510.11225) found that models good on graph matching (Smatch) often produce non-equivalent logic, with variable binding and predicate naming the dominant failures [ABSTRACT]. Relevant warning: a graph-similarity score is not logical equivalence, so any structural comparison must be exact on the pieces that matter.\n\n3. CONTROLLED NATURAL LANGUAGES\n\nAttempto Controlled English: APE (parser) https://github.com/Attempto/APE ; RACE (reasoner).\n- Input: ACE text (a restricted English subset); output: DRS, first-order logic, TPTP, OWL/SWRL, RuleML, paraphrase [FULL README]. Needs SWI-Prolog; `make install`. Interfaces: command line, socket, HTTP, Prolog/Java.\n- Ambiguity is excluded or resolved by fixed interpretation rules (for example a relative clause attaches to the nearest noun phrase), and every noun needs a determiner [SECONDARY]. RACE proves that one ACE text is a logical consequence of another and justifies the proof [SECONDARY]. I did not find RACE release information.\n- Maintenance: ACE 6.7 announced 2013; the SWI-Prolog pack lists APE 6.7.180715, i.e. July 2018 [SECONDARY]. English only.\n- Verdict: the strongest semantic guarantee, since our rule (\"Every thing that smells of decomposition is dead\") plus case plus conclusion is exactly a universal-instantiation step APE and RACE can check. Cost: the writer must produce valid ACE, and unknown words need lexicon entries. I found no measured LLM-to-ACE translation fidelity. Choose this only if you accept forcing the writer into ACE. No Swedish.\n\nPENG / PENG-ASP (Schwitter): chart parser plus unification grammar, DRS to ASP; implementation and binary not public per the 2023 CNL2ASP paper [SECONDARY]; no 2024 to 2026 updates found. Not usable. CNL2ASP (https://github.com/dodaro/cnl2asp, https://arxiv.org/abs/2311.10505): English CNL to ASP for combinatorial problems [FULL]; wrong domain.\n\nNaproche / ForTheL (https://github.com/naproche/naproche): proof checking of controlled-English mathematics, English, uses E, Vampire or SPASS provers; 2,499 commits, last-commit date not shown [FULL README]. Wrong domain (math), heavy install (Isabelle, Mercurial). Visored (arXiv 2606.17581, June 2026) is a similar CNL-to-Lean prover for LLM-written math; claims 222 of 244 miniF2F problems checked, a coverage figure not a held-out score [SECONDARY, aggregator]. Not relevant to commonsense steps.\n\nGrammatical Framework (GF): the one CNL toolkit with real English plus Swedish. The Resource Grammar Library has a Swedish concrete syntax and a shared abstract syntax [SECONDARY]. Ljunglöf and Siverbo's FraCaS treebank has all FraCaS sentences in English and Swedish, with about 86% of Swedish translations judged grammatical and natural [ABSTRACT, 2011/2012]; it is open source. GF 3.12 released on 3 August (year not on the page; 3.11 was July 2021), with the RGL no longer in binary packages, so you must clone gf-rgl and compile [SECONDARY]. I found no 2024 to 2026 work combining GF and LLMs. Verdict: only worth it if you want to define a narrow bilingual fragment in which the writer's slot sentences are generated from abstract syntax, so \"the same case in two languages\" is exact. High cost (grammar plus lexicon writing).\n\n4. spaCy / Stanza AND PARAPHRASE-ROBUST DETERMINISTIC MATCHING\n\n- Stanza UD parsing: Swedish Talbanken UAS 90.32 / LAS 87.85, lemmas 97.92; Swedish LinES LAS 85.25; English EWT LAS 86.77, lemmas 96.63 (UD 2.12, Stanza 1.5.1) [FULL, Stanza performance page]. spaCy has Swedish pipelines (sv_core_news_sm and larger) trained on UD Talbanken v2.8 and SUC v3.0 [SECONDARY]; no published LAS for them found (an older KB-Lab Swedish spaCy pipeline reported 93.51 UAS / 90.74 LAS [SECONDARY]).\n- spaCy DependencyMatcher: Semgrex-style patterns over dependency trees, needs a parser [SECONDARY, docs]. The third-party spacy-pattern-builder (https://github.com/cyclecycle/spacy-pattern-builder) generates such patterns from example sentences, which fits \"build a pattern from the rule's condition with the slot left open, match it against the case\" [SECONDARY].\n- PredPatt (https://github.com/hltcoe/PredPatt; reimplemented in the `decomp` package): rule-based predicate-argument extraction from UD, evaluated on gold UD English EWT and WSJ; the decomp version needs pre-parsed UD input [SECONDARY]. A deterministic way to get predicate plus argument heads per sentence in any UD language.\n- Synonymy: WordNet via NLTK for English. LangPro's WordNet ablation (-2.44%) shows it is the thing doing paraphrase work [FULL]. Swedish: the Open Multilingual Wordnet Swedish (SALDO-based) has 6,796 synsets; Swesaurus is CC-BY-4.0, 12.16 MB LMF file dated 2017-09-19; no synset count found [SECONDARY].\n- No existing off-the-shelf package ties these together. You would write a small normaliser: lemmatise, extract predicate-argument tuples, canonicalise content words through synonym/hypernym classes, then compare structures with the term substituted. Swapping the term for a different reference class (squirrel vs animal) fails unless the lexicon says they are equivalent, so the reference-class error is refused by default. My inference on parse noise: both sentences are near-identical, so a parser tends to make the same mistake on both, but that is not measured.\n\n5. CHECKING LLM-WRITTEN STEPS BY PARSING\n\n- VeriCoT (Feng et al., ICLR 2026, https://arxiv.org/abs/2511.04662): LLM translates each step to first-order logic in SMT-LIB, Z3 checks entailment from premises. Table 1: share of chains that could be verified (pass rate) 45.2% on ProofWriter, 25.3% on BioASQ, 15.2% on LegalBench-SARA; verifier precision 94.1, 84.3 and 87.0 respectively [FULL]. So most LLM chains fail to translate and verify, and the translation itself is a fuzzy LLM step.\n- Explanation-Refiner (Quan et al., https://arxiv.org/abs/2405.01379, code https://github.com/neuro-symbolic-ai/explanation_refinement): LLM translation into Isabelle/HOL with neo-Davidsonian events; with theorem-prover feedback GPT-4 logical validity rose 36% to 84% (e-SNLI), 12% to 55% (QASC), 2% to 37% (WorldTree), and syntax errors in autoformalisation fell 68.67%, 62.31% and 55.17% on average [FULL, abstract]. It also reports that human-written explanations contain logical errors [FULL].\n- \"Grammars of Formal Uncertainty\" (NeurIPS 2025, https://arxiv.org/abs/2505.20047): SMT autoformalisation accuracy moved +34.8% on ProofWriter and -44.5% on FOLIO [SECONDARY]. \n- Takeaway: with an LLM in the translation step the error rates are large and dataset-dependent; the deterministic-only route removes that fuzziness but is limited by the parser (about 82 F1 for UD-Boxer English).\n\nRANKED SHORTLIST (try in this order)\n\n1. UD dependency-triple normaliser on spaCy or Stanza (own roughly 100 lines), with a DependencyMatcher or PredPatt-style extraction and WordNet/Swesaurus synonym classes. Why first: cheapest, covers English and Swedish, deterministic, and refuses reference-class changes by default. Compare (lemma, relation, argument-head) tuples after substituting the term; refuse on extra or missing content words, flipped negation, or different quantifier words. Install: \n   pip install spacy stanza nltk\n   python -m spacy download en_core_web_trf\n   python -m spacy download sv_core_news_lg\n   python -c \"import stanza; stanza.download('sv'); stanza.download('en')\"\n   python -c \"import nltk; nltk.download('wordnet'); nltk.download('omw-1.4')\"\n   (Model names are the standard spaCy names; sv_core_news_sm is confirmed in [SECONDARY], the larger ones I did not check.)\n\n2. LangPro as a strict English verifier of the two substitution checks (case entails instantiated condition; instantiated outcome entails conclusion). Evidence: precision 97.6 to 97.8, recall 58 to 62 on SICK, no abduction [FULL]. Run it as an extra gate behind option 1 so a disagreement is flagged, not silently accepted. Install: `git clone https://github.com/kovvalsky/LangPro` and follow the repo wiki (Prolog, Perl and a CCG parser; I did not see a published one-line install). Unknown: recall on our sentence pairs, and any near-miss resistance.\n\n3. UD-Boxer, to get an explicit DRS (negation and quantifier boxes) from the same UD parse and compare the DRS graphs after substitution. Evidence: about 82 F1 English, 75 to 78 German/Italian/Dutch, no hallucinated output [FULL]. Install per README: `opam install grew.1.8.1 grewpy.1.8.0 libcaml-grew.1.9.2`, then `git clone https://github.com/WPoelman/ud-boxer && pip install -r requirements/requirements.txt` (versions pinned; newer GREW breaks it). Swedish needs 4 language-specific rules written by you. If you can control the writer's language instead, APE+RACE (`git clone https://github.com/Attempto/APE`, SWI-Prolog, `make install`) gives an exact check but forces ACE and has no Swedish; treat it as the alternative to option 3.\n\nNOT RECOMMENDED: NeuralLog and VeriCoT-style LLM autoformalisation (a model back in the loop), AMR tools, Naproche and Visored (wrong domain), PENG (not public), PredPatt as a stand-alone (needs a UD parser anyway), GF unless you want to write a bilingual grammar.\n\nCAVEATS\n- Several repo pages show no commit dates; I give \"not shown\" rather than guessing. GF 3.12's year is unconfirmed.\n- Numbers for SICK-style datasets are on natural but noisy label sets; our task is closer to pairs differing by one substituted word, where results are unknown.\n- The spaCy Swedish accuracy is not found; the Stanza Swedish figures are from the official performance page.\n\nKey files and links: no files written. Sources are the URLs given inline above.\n"}