Automated Theorem Proving On-Line Course Materials Resource

This is a collection of teaching materials for courses in theorem proving, including propositional, first-order, and higher order theorem proving, classical and non-classical logics, resolution and non-resolution methods, and mathematical induction. Courses in logic per se are not appropriate, but rather courses that emphasize automatic theorem proving. Mainly course notes, transparencies, handouts, and assignments are sought. The purpose of this page is to have such materials online to facilitate the teaching of theorem proving courses. Send URL's of any additional such on-line materials to plaisted@cs.unc.edu and indicate the nature of the material (course notes, transparencies, handouts, assignments, or course outlines).

Matt Kaufmann and J Strother Moore's Flying Demo of ACL2

Matt Kaufmann and J Strother Moore's Brief ACL2 Tutorial

Christoph Kreitz' Computational Type Theory Course (Partial course notes and slides, Nuprl manuals, draft notes from a 1985 lecture, material from Stuart Allen, 1985 course notes in German, and a 1986 Nuprl book on line)

Christoph Kreitz' Introduction to Automated Reasoning course(A variety of material, some of it in German)

Christoph Kreitz' Automated Logic and Programming Course (in German) (Slides and on-line textbook)

Christoph Kreitz' summary page (Links to a variety of material from a variety of courses, some of it in German)

Manfred Kerber's Mechanised Deduction page (Syllabus, slides, exercises, and Otter proofs)

Larry Paulson's Logic and Proof course (Syllabus, past exam questions, course notes, and slides)

Frank Pfenning's Automated Theorem Proving Course (Course outline and course notes)

Power Point Slides on Resolution

Power Point Slides on Theorem Proving

Jürgen Stuber's copy of exercises in Machine-aided Proof (in German) (propositional and first-order theorem proving mostly by resolution with an emphasis on orderings and term rewriting, from a 1993 course given by another person in Saarbrücken)

Geoff Sutcliffe's Automated Theorem Proving Course (HTML course notes covering propositional and first-order logic, resolution, paramodulation, and tableau methods, with some other related materials)

Some Miscellaneous Slides about Theorem Proving I Found on the Web

Introduction to Artificial Intelligence and Computer Simulation (An AI course including theorem proving; includes slides and homework assignments. Found by a web search.)

PSU local HOL system page (Contains an HOL tutorial. Found by a web search.)

Concrete Semantics With Isabelle/HOL (The book Concrete Semantics introduces semantics of programming languages through the medium of a proof assistant.)