[Haskell-cafe] manipulating predicate formulae

John Meacham john at repetae.net
Thu Dec 4 03:50:29 EST 2008

I have no idea if it is relevant, but I wrote a tiny proof assistant for
a hilbert style first order logic the other day.


set hasUnicode to False at the top if your terminal doesn't support
unicode. fun what one can do in a few  hundred lines of haskell.. :)

heres the cheat sheet:

---- stack operations ----
0 duplicate top of lemma stack
1-9 move the specified formula to the top of the stack
shift A-Z copy the specified formula from the theorem list to the top of
the stack
- delete top of lemma stack
p promote the top of the lemma stack to a theorem
---- rules of inference ----
d (degeneralize) replace a quantifier with an unbound term
g (generalize) universally quantify all unbound terms
m use modus pones to apply the top of the stack to the second item in
the stack
---- utilities ----
h show this help
u undo last operation
! quit


John Meacham - ⑆repetae.net⑆john⑈

More information about the Haskell-Cafe mailing list