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.