AutoProof.Internal.Intuitionistic.Proof.Provability

Description

Provability checking in intuitionistic propositional logic.

Synopsis

Documentation

Determine whether a judgement is intuitionistically valid.

Expand

>>> 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.

Expand

>>> 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