🚀 go-pugleaf

In <IMG.92Nov17114848@hope.aisb.ed.ac.uk> img@aisb.ed.ac.uk (Ian Green) writes:


>If you're looking for an interactive system, you might try FOL or
>its derivative, GETFOL.  Contact Fausto Giunchiglia, at fausto@irst.it or
>fausto@dist.unige.it for more info.  Weyhrauch80 describes FOL.

>	-ian

>@article(Weyhrauch80,
>        Author = {Weyhrauch, Richard W.},
>         Title = {Prolegomena to a Theory of Mechanized Formal Reasoning},
>          Year = {1980},
>       Journal = AI,
>        Volume = {13},
>         Pages = {133--170})

As I recall there are several programs that do FOL proofs in a natural
deduction system for the Mac and for IBM-clones.  The ones I'm
thinking of aren't theorem provers, but are more like proof checkers.
I know that Tarski's World (by Barwise and Etchemendy) is available both
for the macintosh and for windows.  If that's the sort of thing you're looking
for then there are several others also (tho I can't at the moment recall the
titles).  Someone was demo'ing an IBMish program at the last APA conference
I attended.

If that's the sort of thing you're looking for then you might ask on
philos-l.  I seem to recall that a list of such programs circulated there not
too long ago.

jim hardy