[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.
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⑈
More information about the Haskell-Cafe
mailing list