[Haskell-cafe] manipulating predicate formulae

[John Meacham]

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.

http://repetae.net/Hilbert.hs         

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

-- 
John Meacham - ⑆repetae.net⑆john⑈