| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
G4ipProver.Prover
Description
The actual theorem prover
Synopsis
- prove :: Prop -> Maybe (ProofTree Context)
- decide :: Prop -> Bool
- add :: Prop -> Context -> Context
- right :: Context -> Prop -> Maybe (ProofTree Context)
- left :: [Prop] -> Prop -> Maybe (ProofTree Context)
- elim :: (Prop, [Prop]) -> Prop -> Maybe (ProofTree Context)
- data ProofTree a
- = InitRule a Prop
- | TopR a
- | BottomL a Prop
- | SplitAnd a Prop Prop (ProofTree a) (ProofTree a)
- | ImpRight a Prop Prop (ProofTree a)
- | AndLeft a Prop Prop Prop (ProofTree a)
- | ElimOr a Prop Prop Prop (ProofTree a) (ProofTree a)
- | TImpLeft a Prop Prop (ProofTree a)
- | FImpLeft a Prop Prop (ProofTree a)
- | AndImpLeft a Prop Prop Prop Prop (ProofTree a)
- | OrImpLeft a Prop Prop Prop Prop (ProofTree a)
- | OrRight1 a Prop Prop (ProofTree a)
- | OrRight2 a Prop Prop (ProofTree a)
- | LeftBoth a Prop (ProofTree a)
- | PImpLeft a Prop Prop Prop (ProofTree a) (ProofTree a)
- | ImpImpLeft a Prop Prop Prop Prop (ProofTree a) (ProofTree a)
- type Context = ([Prop], [Prop])
Documentation
prove :: Prop -> Maybe (ProofTree Context) Source #
Construct a proof if it exists for the given proposition.
Type parameter represents context type.
Constructors
| InitRule a Prop |
|
| TopR a |
|
| BottomL a Prop |
|
| SplitAnd a Prop Prop (ProofTree a) (ProofTree a) |
|
| ImpRight a Prop Prop (ProofTree a) |
|
| AndLeft a Prop Prop Prop (ProofTree a) |
|
| ElimOr a Prop Prop Prop (ProofTree a) (ProofTree a) | |
| TImpLeft a Prop Prop (ProofTree a) |
|
| FImpLeft a Prop Prop (ProofTree a) |
|
| AndImpLeft a Prop Prop Prop Prop (ProofTree a) |
|
| OrImpLeft a Prop Prop Prop Prop (ProofTree a) |
|
| OrRight1 a Prop Prop (ProofTree a) |
|
| OrRight2 a Prop Prop (ProofTree a) |
|
| LeftBoth a Prop (ProofTree a) | |
| PImpLeft a Prop Prop Prop (ProofTree a) (ProofTree a) |
|
| ImpImpLeft a Prop Prop Prop Prop (ProofTree a) (ProofTree a) |
|