This directory, ~ok/COSC410, is for COSC410,
Logic for Artificial Intelligence.
It holds a mix of stuff for the new 13-week COSC410
and the old 20-week COSC462.
Roadmap for 2011:
1. I am going to present a method of proving (or rather,
of disproving) propositional formulas called the Tableau
method. In previous years I have presented other methods.
This method extends to handle modal logics rather nicely.
2. This is a Computer Science paper, not a Philosophy paper.
I want you to go away knowing that you personally COULD
build a program that processed logical formulas. The first
step here is the notion of
- a recursively defined Language
- modelled by a recursively defined Data Structure, atree
so I talk about how we define languages and how we represent
and work on trees inside a computer.
3. There will also be some material on parsing and printing
such languages.
Resources for 2011:
410-LIA-sets-and-functions.pdf
Background on set theory and functions, useful for my assignment.
This was downloaded from www.logicinaction.org
410-LIA-tableaux.pdf
Extensive chapter on tableau methods for propositional calculus,
first-order predicate calculus, and a simple modal logic.
This was downloaded from www.logicinaction.org
410-LIA-natural-deduction.pdf
For interest.
This was downloaded from www.logicinaction.org
Hans van Ditmarsch
410-Aho-Ullman-FOCS-tree-model.pdf
Foundations of Computer Science, by Aho and Ullman,
was a *superb* introduction to, well, what it says.
There was a Pascal edition and then a C edition.
It's the kind of thing that *should* have been at
the core of an undergraduate CS1/CS2 programme and
would have produced really well grounded students.
Sadly, the tides of fashion passed it by, and the
world jumped on the Java bandwagon and the 'let's
mash up a bunch of stuff we don't understand and
throw it on the Web approach.' If you can find a
secondhand copy of the book, it's worth buying and
reading. You probably think you know everything
you should have learned in CS1/CS2, but this book
may well teach you something. The whole book (C
edition) is now available on-line at
http://infolab.stanford.edu/~ullman/focs.html
This chapter tells you how to program trees. The
trees you particularly need are what Aho & Ullman
call "expression trees".
2011-assignment
My part of the last assignment.
Arith.java
arith.c
arith.hs
Arithmetic expressions involving literal integers, unary
minus, sum, difference, product, quotient, and remainder.
Output and evaluation but no input.
http://en.wikipedia.org/wiki/Sequent
is a good short summary about sequents.
http://stanford.library.usyd.edu.au/contents.html
is the Australian mirror of the Stanford Encyclopedia
of Philosophy, which has a lot of interesting stuff
about logic.