Find an intuitionistic proof of a judgement, if a proof exists.

Find an intuitionistic proof of a formula, if a proof exists.

Find an intuitionistic proof of a judgement, if one exists, using Statman's algorithm.

• Richard Statman (1979) "Intuitionistic propositional logic is polynomial-space complete." Theoretical Computer Science, Volume 9, Issue 1, pp. 67–72. DOI.

The judgement to be proved is converted to an implicational judgement as described in toImp and proved (if possible) using proveImp. The resulting proof is then converted into a proof of the original judgement.

(proveImp (g |- a)) finds an intuitionistic proof of a judgement \(g \vdash a\) in the implicational fragment of propositional logic, if such a proof exists.

The algorithm is adapted from section 2.4 of

• Samuel Mimram (2020) PROGRAM = PROOF.

Examples

>>> proveImp $ [Var 'a', Imp (Var 'a') (Var 'b')] |- Var 'b'
Just (ImpElim ([Var 'a',Imp (Var 'a') (Var 'b')] |- Var 'b') (Axiom ([Var 'a',Imp (Var 'a') (Var 'b')] |- Imp (Var 'a') (Var 'b'))) (Axiom ([Var 'a',Imp (Var 'a') (Var 'b')] |- Var 'a')))

>>> proveImp $ [Imp (Var 'a') (Var 'b'), Imp (Var 'b') (Var 'a')] |- Var 'a'
Nothing