Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis
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