autoproof-0.0.0.0: Propositional logic library

Copyright	(c) Artem Mavrin 2021
License	BSD3
Maintainer	artemvmavrin@gmail.com
Stability	experimental
Portability	POSIX
Safe Haskell	Safe
Language	Haskell2010

AutoProof.Internal.Intuitionistic.Proof.Correctness

Description

Check proof correctness in intuitionistic logic.

Synopsis

correct :: Ord a => Judgement a -> Proof a -> Bool
valid :: Ord a => Proof a -> Bool
debug :: Ord a => Proof a -> Either (Proof a) ()

Documentation

correct :: Ord a => Judgement a -> Proof a -> Bool Source #

Check whether a proof is a correct proof of a given judgement

valid :: Ord a => Proof a -> Bool Source #

Check whether a proof is valid.

debug :: Ord a => Proof a -> Either (Proof a) () Source #

Return an invalid inference node (on the Left), if there is one. Otherwise, return Right ().