[FOM] Logic packages

[Steven Obua]

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
>
>           Thomas
>
>
> 
>  
>
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.

Best,

Steven Obua

-- 
Steven Obua
Technische Universität München
Institut für Informatik
Boltzmannstr. 3
D-85748 Garching

Tel: ++49 (0)89 / 289-17328
EMail: obua at in.tum.de
Raum: 01.11.059