A system of inference based on proof search: an extended abstract
On the map: LLM reasoning → Reasoning benchmarks and evaluation
Abstract (arXiv)
Gentzen designed his natural deduction proof system to ``come as close as possible to actual reasoning.'' Indeed, natural deduction proofs closely resemble the static structure of logical reasoning in mathematical arguments. However, different features of inference are compelling to capture when one wants to support the process of searching for proofs. PSF (Proof Search Framework) attempts to capture these features naturally and directly. The design and metatheory of PSF are presented, and its ability to specify a range of proof systems for classical, intuitionistic, and linear logic is illustrated.
Key facts. No citing papers in the map yet (data through 7 Oct 2026). Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning. First posted on arXiv 24 Jul 2023.
Builds on
No reference list yet.
Built on by
Not cited yet.
Similar, not cited
Close in wording, no citation either way
- 2023Formal Proofs as Structured Explanations: Proposing Several Tasks on Explainable Natural Language Inference
- 2023Testing the General Deductive Reasoning Capacity of Large Language Models Using OOD Examples
- 2022Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis
- 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoning
- 2026TreeThink: A Modular Tree Search Library for Mathematical Reasoning with LLMs
- 2026Self-Supervised Theorem Discovery in a Formal Axiomatic System
- 2024Aristotle: Mastering Logical Reasoning with A Logic-Complete Decompose-Search-Resolve Framework
- 2026Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs