G4ipProver.Prover

The actual theorem prover

Documentation

prove :: Prop -> Maybe (ProofTree Context)

Construct a proof if it exists for the given proposition.

decide :: Prop -> Bool

Decide if the given proposition has a proof

add :: Prop -> Context -> Context

Add a proposition to the context.

right :: Context -> Prop -> Maybe (ProofTree Context)

Invertible decisions.

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

Non-invertible decisions

elim :: (Prop, [Prop]) -> Prop -> Maybe (ProofTree Context)

data ProofTree a

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)

Defined in G4ipProver.Prover

Methods

showsPrec :: Int -> ProofTree a -> ShowS

show :: ProofTree a -> String

showList :: [ProofTree a] -> ShowS

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

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