There are some great sources for logic, including AI logics, logic in language, metaphysics, model theory, foundations. The Guide to Philosophy and the Stanford Encyclopedia of Philosophy are good starting points. A source of mathematical logic that has a lot of stuff on jobs, conferences, journals, specific research programs, etc. is Mathematical Logic around the world.

Wikipedia has good pages on propositional logic and first-order logic, and many related topics. In particular, the external links contain several useful online resources for mathematical logic.

If you feel you need much more support in understanding first order logic, there is courseware available from the Openproof Project at Stanford University called Tarski's World. You will need to buy it (US$40).

There is free software called Deductions that supports development of natural deduction (= Gentzen system) proofs in a tabular format. There are books available online based on this kind of proof system, including A Modern Formal Logic Primer by Paul Teller, and Symbolic Logic: An Accessible Introduction to Serious Mathematical Logic by Tony Roy

Andrei Vorokov of the University of Manchester, UK is teaching a similar course on logic in computer science.

From the following pages you can download the main reference papers for BDDs:

Graph Based Algorithms for Boolean Function Manipulation R. Bryant, 1986.

Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams, R. Bryant, 1992.

We place here two resources on the conversion of wffs to clausal form. Although the algorithm is well-known, they are good summaries. The first one is from Temple University, author unknown. The second is course notes by Prof Stephen Hegner of Umea University in Sweden.

A brief description of Tseitin's transformation of formulas to CNF.

A study of different normal forms based on NNF, looking at succinctness of representation, polytime queries, and polytime operations. (local version)

M. Genesereth has nice slides on Herbrand Models that are useful for testing satisfiability of clausal formulas.

The NY Times has a nice introductory article on infinity: countable and uncountable. It is one in a series giving an introduction to mathematics.

Here are miscellaneous papers/notes/slides on logic programming and nonmonotonic reasoning.

Notes on the CWA

PDF Notes by Carsten Fritz on Fixed Points

Paper on well-founded semantics by the inventors of this semantics

Paper on Stable Models by the inventors of this semantics

Paper on Answer Sets by the inventors of this semantics

Prof G. Brewka's slides on Answer Sets

Prof G. Brewka's slides on Applications of Answer Sets

Friends of ours prepared notes on Default Logic that you can download. Be warned, though. The file is quite big.

A brief introduction to modal logic is available from the Stanford Encyclopedia of Philosophy. There is also the webpage of a course on modal logic.

If you are rusty about how to set out mathematical proofs, a text that may be a helpful refresher is

- Wikipedia has pages on philosophical ontology and computer science ontology, as well as description logics.
- http://dl.kr.org: The definitive description logics website.
- The Protege ontology editor and knowledge base framework developed at Stanford.
- The SWOOP ontology editor. The RACER description logic reasoner.
- The FACT++ description logic reasoner.
- The CEL description logic reasoner.
- Franz Baader's home page containing links to his talks and papers on description logics.
- Ian Horrocks's home page containing links to his talks and publications on descriptions logics.
- Enrico Franconi's slides on propositional description logics.
- Tommie Meyer's slides on the description logic ALC.