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

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

(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

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.

Determine whether a judgement is intuitionistically valid.

Examples

>>> isProvable $ [Var "a", Var "b"] |- And (Var "a") (Var "b")
True

>>> isProvable $ [] |- Or (Var "a") (Not (Var "a"))
False

Determine whether a formula is an intuitionistic tautology.

Examples

>>> isTautology $ Imp (And (Var 'a') (Var 'b')) (Var 'a')
True

>>> isTautology $ Or (Var 'a') (Not (Var 'a'))
False

>>> isTautology $ Not (Not (Or (Var 'a') (Not (Var 'a'))))
True

Find the cut nearest the root of a proof, if any. This functions assumes the proof is valid.

Check if a proof has a cut.

Check whether a proof is a correct proof of a given judgement

Check whether a proof is valid.

Return an invalid inference node (on the Left), if there is one. Otherwise, return Right ().