| Copyright | (c) Artem Mavrin 2021 |
|---|---|
| License | BSD3 |
| Maintainer | artemvmavrin@gmail.com |
| Stability | experimental |
| Portability | POSIX |
| Safe Haskell | Safe |
| Language | Haskell2010 |
AutoProof.Internal.Intuitionistic.Proof.Search.Implication
Description
Intuitionistic proofs in the implicational fragment of propositional logic.
Documentation
proveImp :: Ord a => Judgement a -> Maybe (Proof a) Source #
( finds an intuitionistic proof
of a judgement \(g \vdash a\) in the implicational fragment of propositional
logic, if such a proof exists.proveImp (g |- a))
The algorithm is adapted from section 2.4 of
- Samuel Mimram (2020) PROGRAM = PROOF.
Examples
>>>proveImp $ [Var 'a', Imp (Var 'a') (Var 'b')] |- Var 'b'Just (ImpElim ([Var 'a',Imp (Var 'a') (Var 'b')] |- Var 'b') (Axiom ([Var 'a',Imp (Var 'a') (Var 'b')] |- Imp (Var 'a') (Var 'b'))) (Axiom ([Var 'a',Imp (Var 'a') (Var 'b')] |- Var 'a')))
>>>proveImp $ [Imp (Var 'a') (Var 'b'), Imp (Var 'b') (Var 'a')] |- Var 'a'Nothing