# Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis

arXiv: https://arxiv.org/abs/2205.05728 · HTML: https://mlsanity.com/paper/2205.05728/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 0 of its 15 references that are in the map.
- First posted on arXiv 11 May 2022.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Built on by (most cited first, 2 of 2)

- [Full Automation of Goal-driven LLM Dialog Threads with And-Or Recursors and Refiner Oracles](https://mlsanity.com/paper/2306.14077/) (2023)
- [Through the Looking Glass, and what Horn Clause Programs Found There](https://mlsanity.com/paper/2407.20413/) (2024)

## Abstract (arXiv)

With help of a compact Prolog-based theorem prover for Intuitionistic Propositional Logic, we synthesize minimal assumptions under which a given formula formula becomes a theorem. After applying our synthesis algorithm to cover basic abductive reasoning mechanisms, we synthesize conjunctions of literals that mimic rows of truth tables in classical or intermediate logics and we abduce conditional hypotheses that turn the theorems of classical or intermediate logics into theorems in intuitionistic logic. One step further, we generalize our abductive reasoning mechanism to synthesize more expressive sequent premises using a minimal set of canonical formulas, to which arbitrary formulas in the calculus can be reduced while preserving their provability. Organized as a self-contained literate Prolog program, the paper supports interactive exploration of its content and ensures full replicability of our results.