autoproof-0.0.0.0: Propositional logic library
Copyright(c) Artem Mavrin 2021
LicenseBSD3
Maintainerartemvmavrin@gmail.com
Stabilityexperimental
PortabilityPOSIX
Safe HaskellSafe
LanguageHaskell2010

AutoProof.Internal.Classical.Proof

Description

Classical proofs in propositional logic.

Synopsis

Provability checking

isProvable :: Ord a => Judgement a -> Bool Source #

Determine whether a judgement is classically valid.

Examples

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

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

isTautology :: Ord a => Formula a -> Bool Source #

Determine whether a formula is a classically tautology.

Examples

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