Re: Logic and proof tutorial resources

On Tue, Dec 11, 2001 at 05:24:23PM -0800, Piotr Kaminski wrote:
> > >[1] http://www.wikipedia.com/wiki/Larrys_Text
> > I really would not recommend this, to be honest.
> 
> What can you recommend?  I'm currently working my way through Sowa's
> Knowledge Representation book (2000).  It's not exactly easy going, but it
> seems to be relevant.  What's your opinion?
> 
>         -- P.
> 
> --
>   Piotr Kaminski <piotr@ideanest.com>  http://www.ideanest.com/
>   "It's the heart afraid of breaking that never learns to dance."

Hi, I have taught logic at various levels for some years. Here are a
couple of suggestions. 

I don't know of many (or any) good logic tutorials on the net. I don't
like the wikipedia thingy very much, although I don't think there is any
problem with the emphasis on nl argument --  it seems to me that it would
be more likely for your New Fancy Theorem Prover to be used in some
nl-processing related task rather than to test the independence of
large cardinals conjectures. 

There are some very good entries in the Stanford Encyclopedia of
Philosophy (http://plato.stanford.edu), beginning with the classical
logic article by Stewart Shapiro. These are useful to get an idea of the
variety of things covered, though likely not suited to initial study or
self-study (as always, your mileage etc.).

There are couple of really good books which I have liked much and I think
would be good for a 'select' beginner:

A Logic Primer, by  C. Allen and M. Hand. MIT Press. 
(An added benefits is that it sells for $15 or so)

Natural Logic, by N. Tennant. I fear this is out of print. Used to be
published by the U. of Edinburgh Press.

The "Primer" is as concise as can be, and Allen and Hand claim it to be
'for use with an instructor', but I think for someone wanting to learn
the basic formal presentation of a natural deduction system, and to find
a ton of exercises for practice, the information is there. Covers only
classical FOL, via natural deduction Lemmon-style (in fact, it basically
uses Lemmon's system and notation except for a couple of minor changes). 

There is also a well-designed web-site where one can practice with the
proof system, http://logic.tamu.edu. 

Tennant's book actually covers a lot of stuff for its size, including
classical semantics and basic (and not so basic) meta-logic,
intuitionistic logic, Kripke semantics for same etc. It presents natural
deduction Prawitz-style, which I find more interesting and more
illuminating as to various other more advanced topics (like normal form
theorems etc.). The book is more advanced than the "Primer," obviously. 

I have occasionally tried to convince Tennant to revise and reprint, but
I'm not sure he has any plans.

I don't know of a lot of intro books that use Hilbert-style, as opposed
to natural deduction, presentations. A great book of course is Harold
Enderton's (recently republished), used in many semi-advanced courses.
I'm not sure how it would be to start with that, but maybe with a good
math background it wouldn't be too bad. 

I haven't read Waldinger-Manna unfortunately (for me, I suppose), but
what I have read about theorem provers and automated deduction is
generally very strongly focused on engineering (as one would expect), not
logical issues. I don't think one would get a good appreciation for the
basic notions and their main consequences by reading that. (And the basic
notions are both simpler and more general anyway.) I have bought a couple
of Prolog books (authors will go unnamed) where the reader really has to
do some work just to figure out that the comma is equivalent to logical
conjunction or some such.

Best,


-- 
- - - - * * * * * - - - - * * * * * - - - - * * * * * - - - -
Pierluigi Miraglia                  Cycorp, Inc.
Ontological Engineer                3721 Executive Center Dr.
(512) 514-2988                      Austin, TX 78731

Received on Wednesday, 12 December 2001 12:24:33 UTC