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.