A compact Prolog-based Theorem Prover for Intuitionistic Propositional Logic

Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis

We present a compact theorem prover for intuitionisticpropositional logic to synthesize minimal assumptions under which a given formula formula becomes a theorem.After applying our synthesis algorithm to cover basic abductive reasoningmechanisms, we synthesize conjunctions of literals that mimic rows of truthtables 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 reasoningmechanism 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.