Prover for G4ip (LJT)
Readme
Formulae:
F ::= false
| A
| F & F
| F v F
| F -> F
| F <-> F
| (F)
Sequents: => F or
[F,]* F => F
Inference Rules:
html,
dvi or
ps.
Start: starts the proof search,
Clear: clears the text fields,
Next: searches for the next proof,
Stop: stops the proof search.
Provable Examples:
- => (p v (q v r)) <-> ((p v q) v r)
- => (p & (q & r)) <-> ((p & q) & r)
- => (p & (q v r)) <-> ((p & q) v (p & r))
- => (p v (q & r)) <-> ((p v q) & (p v r))
- => (p -> p) -> (p -> p)
- => (a -> (b -> c)) -> ((a -> b) -> (a -> c))
- => a -> ((a -> b) -> a)
- => b -> ((a -> b) -> b)
- => (a & b) -> (b & a)
- => (a -> (a -> b)) -> (a -> b)
- => ((((p -> q) -> p) -> p) -> q) -> q
- => (a v (a -> b)) -> (((a -> b) -> a)-> a)
- => (a -> (b -> false)) -> (b -> (a -> false))
- => ((a v (a -> false))-> false)-> false
- a & b, c & d => b & c
- (a v (a-> false)) -> false => false
Non-Provable Examples:
- => ((a -> b) -> a) -> a
- => a v (a -> false)
- => (a & b v (((( a-> flase) -> false) -> q) v (b -> q)) -> q) -> q
Some advanced examples
Source Code:
Formulae,
Contexts,
Sequents,
ProofDisplay,
Prover,
Parser,
Applet
Lambda Prolog Version: The programm
G4ip.mod can be executed using
Terzo
Another implementation of G4ip by Joshua Hodas and Dale Miller written in
Lolli can be found
here.
Christian Urban
Last modified: Sun May 10 18:18:13 GMT 1998