g4ip-prover-2.0.0.0: Theorem prover for intuitionistic propositional logic using G4ip

G4ipProver.Prover

Description

The actual theorem prover

Synopsis

# Documentation

Construct a proof if it exists for the given proposition.

Decide if the given proposition has a proof

Add a proposition to the context.

Invertible decisions.

left :: [Prop] -> Prop -> Maybe (ProofTree Context) Source #

Non-invertible decisions

data ProofTree a Source #

Type parameter represents context type.

Constructors

 InitRule a Prop init rule: Γ, P ⊢ P TopR a ⊤R rule: ∅ ⊢ T BottomL a Prop ⊥L rule: Γ, ⊥ ⊢ A SplitAnd a Prop Prop (ProofTree a) (ProofTree a) ∧R rule ImpRight a Prop Prop (ProofTree a) →R rule AndLeft a Prop Prop Prop (ProofTree a) ∧L rule ElimOr a Prop Prop Prop (ProofTree a) (ProofTree a) TImpLeft a Prop Prop (ProofTree a) ⊤L rule FImpLeft a Prop Prop (ProofTree a) ⊥→L rule AndImpLeft a Prop Prop Prop Prop (ProofTree a) ∧→L rule OrImpLeft a Prop Prop Prop Prop (ProofTree a) ∨→L rule OrRight1 a Prop Prop (ProofTree a) ∨R1 rule OrRight2 a Prop Prop (ProofTree a) ∨R2 rule LeftBoth a Prop (ProofTree a) PImpLeft a Prop Prop Prop (ProofTree a) (ProofTree a) P→L rule ImpImpLeft a Prop Prop Prop Prop (ProofTree a) (ProofTree a) →→L rule
Instances
 Show a => Show (ProofTree a) Source # Instance detailsDefined in G4ipProver.Prover MethodsshowsPrec :: Int -> ProofTree a -> ShowS #show :: ProofTree a -> String #showList :: [ProofTree a] -> ShowS #

type Context = ([Prop], [Prop]) Source #

Context is a tuple of (invertible propositions, non-invertible propositions).