AutoProof.Internal.Classical.Proof.Provability

Contents

Description

Provability checking in classical propositional logic.

Synopsis

Provability checking

Determine whether a judgement is classically valid.

Expand

>>> isProvable $ [Not (Not (Var 'a'))] |- Var 'a'
True

>>> isProvable $ [Var 'a'] |- Var 'b'
False

Determine whether a formula is a classically tautology.

Expand

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