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

AutoProof.Internal.Intuitionistic.Proof.Search.General

Description

A general-purpose proof search algorithm.

Synopsis

Proof search for judgements and formulas

prove :: Ord a => Judgement a -> Maybe (Proof a) Source #

Find an intuitionistic proof of a judgement, if a proof exists.

proveTautology :: Ord a => Formula a -> Maybe (Proof a) Source #

Find an intuitionistic proof of a formula, if a proof exists.