Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis

TL;DR

This paper presents a Prolog-based method for abductive reasoning in intuitionistic propositional logic, synthesizing minimal assumptions and complex premises to transform classical theorems into intuitionistic ones, with a focus on proof synthesis and logical inference.

Contribution

It introduces a novel abductive reasoning mechanism in intuitionistic logic using theorem synthesis, including the generation of minimal assumptions and expressive sequent premises.

Findings

Synthesizes minimal assumptions for formulas to become theorems.

Generates conjunctions of literals mimicking truth table rows.

Abduces conditional hypotheses to convert classical theorems into intuitionistic ones.

Abstract

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.