-- |
-- Module      : AutoProof.Internal.Intuitionistic.Proof.Search.General
-- Copyright   : (c) Artem Mavrin, 2021
-- License     : BSD3
-- Maintainer  : artemvmavrin@gmail.com
-- Stability   : experimental
-- Portability : POSIX
--
-- A general-purpose proof search algorithm.
module AutoProof.Internal.Intuitionistic.Proof.Search.General
  ( -- * Proof search for judgements and formulas
    prove,
    proveTautology,
  )
where

import AutoProof.Internal.Formula (Formula)
import AutoProof.Internal.Intuitionistic.Proof.Search.Implication (proveImp)
import AutoProof.Internal.Intuitionistic.Proof.Search.Statman (proveStatman)
import AutoProof.Internal.Judgement (Judgement, (|-))
import AutoProof.Internal.Proof.Types (Proof)
import Control.Applicative (Alternative ((<|>)))

-- | Find an intuitionistic proof of a judgement, if a proof exists.
prove :: Ord a => Judgement a -> Maybe (Proof a)
prove :: Judgement a -> Maybe (Proof a)
prove j :: Judgement a
j =
  -- Try proving the judgement as an implicational judgement first (this can
  -- fail if not every formula ocurring in j is implicational).
  Judgement a -> Maybe (Proof a)
forall a. Ord a => Judgement a -> Maybe (Proof a)
proveImp Judgement a
j
    -- Fall back to Statman's algorithm for non-implicational judgements.
    Maybe (Proof a) -> Maybe (Proof a) -> Maybe (Proof a)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Judgement a -> Maybe (Proof a)
forall a. Ord a => Judgement a -> Maybe (Proof a)
proveStatman Judgement a
j

-- | Find an intuitionistic proof of a formula, if a proof exists.
proveTautology :: Ord a => Formula a -> Maybe (Proof a)
proveTautology :: Formula a -> Maybe (Proof a)
proveTautology = Judgement a -> Maybe (Proof a)
forall a. Ord a => Judgement a -> Maybe (Proof a)
prove (Judgement a -> Maybe (Proof a))
-> (Formula a -> Judgement a) -> Formula a -> Maybe (Proof a)
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
|-)