-- |
-- Module      : AutoProof.Internal.Classical.Proof.Provablity
-- Copyright   : (c) Artem Mavrin, 2021
-- License     : BSD3
-- Maintainer  : artemvmavrin@gmail.com
-- Stability   : experimental
-- Portability : POSIX
--
-- Provability checking in classical propositional logic.
module AutoProof.Internal.Classical.Proof.Provability
  ( -- * Provability checking
    isProvable,
    isTautology,
  )
where

import AutoProof.Internal.Classical.Proof.Glivenko (isProvableGlivenko)
import AutoProof.Internal.Formula (Formula)
import AutoProof.Internal.Judgement (Judgement, (|-))

-- | Determine whether a judgement is classically valid.
--
-- ==== __Examples__
--
-- >>> isProvable $ [Not (Not (Var 'a'))] |- Var 'a'
-- True
--
-- >>> isProvable $ [Var 'a'] |- Var 'b'
-- False
isProvable :: Ord a => Judgement a -> Bool
isProvable :: Judgement a -> Bool
isProvable = Judgement a -> Bool
forall a. Ord a => Judgement a -> Bool
isProvableGlivenko

-- | Determine whether a formula is a classically tautology.
--
-- ==== __Examples__
--
-- >>> isTautology $ Or (Var 'a') (Not (Var 'a'))
-- True
-- >>> isTautology $ Var 'a'
-- False
isTautology :: Ord a => Formula a -> Bool
isTautology :: Formula a -> Bool
isTautology = Judgement a -> Bool
forall a. Ord a => Judgement a -> Bool
isProvable (Judgement a -> Bool)
-> (Formula a -> Judgement a) -> Formula a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([] [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|-)