Class Text

• Huth and Ryan, Logic in Computer Science, Modelling and Reasoning about Systems, second edition, Cambridge University Press, ISBN 0-521-54310-X.

Supplemental Texts

• Fitting, First-Order Logic and Automated Theorem Proving, second edition, Springer, ISBN 0-387-94593-8.
• Enderton, A Mathematical Introduction to Logic, Academic Press, ISBN 0-12-238450-4.
• Nerode and Shore, ???

Lecture Notes

Lecture notes for the first several classes are at pdf/outline.pdf. The source is in the directory lectures.

Code fragments are in the directory Code.

Class Mailing list:

The web page for users of your mailing list is:

https://mailhost.cecs.pdx.edu/mailman/listinfo/cs510logic

There is also an email-based interface for users (not administrators)
of your list; you can get info about using it by sending a message
with just the word `help' as subject or in the body, to:

cs510logic-request@cecs.pdx.edu

Other Courses

• http://www.cl.cam.ac.uk/teaching/1011/LogicProof/
• http://www.cs.cornell.edu/courses/cs4860/2009sp/
• http://santos.cis.ksu.edu/771/ (see also http://santos.cis.ksu.edu/771-Distribution/index.html)

Discussion

Huth and Ryan introduce logic with a focus on algorithms. It will be the primary resource for the class. It covers propositional logic, predicate logic, and the modal logics foundational to model checking. It also discusses SAT solving and related techniques in some detail.

Fitting and Nerode and Shore both use Smullyan's technique of tableau proof for elementary provers for propositional and predicate logic. The proof theory and the model theory are very closely related with this technique, making proofs of completeness straightforward.

Topical links:

Links that come up in lecture notes and such. Added more or less in chronological order:

• http://en.wikipedia.org/wiki/Minimal_logic
• Finn Lawler: Classical Logic and the Curry-Howard Correspondence, http://www.scss.tcd.ie/publications/tech-reports/reports.08/TCD-CS-2008-55.pdf.
• Finn Lawler presentation on Classical logic and Curry-Howard http://www.scss.tcd.ie/~flawler/talks/classical-slides.pdf