[FOM] Logic packages
obua at in.tum.de
Wed Jan 2 05:01:16 EST 2008
Thomas Forster wrote:
>Do list members have any favourite computer aids for teaching logic to
>undergraduates? I have been using JAPE, which has many virtues, but it
>does have the disadvantage that it supports Kalish-Montague-style box
>proofs - which is something i am trying to wean my bairns off.
> Any suggestions?
> Happy New Year
One possibility would be the Isabelle proof assistant
(isabelle.in.tum.de). It supports first order ZF, higher-order logic,
and more. One of its main advantages is that it has a very natural logic
language (Isar) which makes both the writing and the reading of proofs
easier. In Munich we use it both for advanced research in mechanical
theorem proving and for teaching logic to undergraduates.
Technische Universität München
Institut für Informatik
Tel: ++49 (0)89 / 289-17328
EMail: obua at in.tum.de
More information about the FOM