Working with Automated Reasoning Tools
BlockLecture at Saarland University
September 1 to September 5, 2008
Lecturers
PD Dr. Christoph Benzmueller and Prof. Dr. Geoff Sutcliffe (Miami, USA)
Credit Points
3CP
Preparation and Lecture Registration Meeting:
16:00, Wednesday, June 18, Office of Christoph Benzmüller, Room 212,
Building E1 1, Saarland University
Lectures:
9:0010:30, 11:0012:30, 14:0015:30, 16:0017:30, MondayFriday, September 15,
Hörsaal 003, Building E1 3, Saarland University
Aim:
Students will learn to work with different automated reasoning systems
for firstorder and higherorder logic.
The theory part of the lecture will introduce these systems and sketch their
background.
The focus of the lecture will be on practical work with the systems, and for
this the TPTP (www.tptp.org)
infrastructure will be introduced and exploited.
Preparation Phase
The students will be asked to prepare for the course by:
 Studying the logics to be used
 Studying literature on automated reasoning
Syllabus of Lecture
 Monday, September 1

 Morning: What is ATP?.
Logical consequence.
1st order logic.
Logical consequence by SPTs.
Clause normal form.
The Herbrand world.
The Resolution inference rule.
The CNF saturation procedure.
The ANL loop.
Paramodulation and superposition.
Encoding and solving problems.
 Afternoon: The TPTP FOF and CNF languages, the SZS ontology.
TPTP problems, TSTP derivations, TSTP models.
SystemOnTPTP interface tools.
 Tuesday, September 2

 Morning: Lab using firstorder logic TPTP and tools; practical
exercises.
 Afternoon: Higherorder logic prerequisite knowledge.
Higherorder logic, inference, calculi.
 Wednesday, September 3

 Morning: The TPTP THF language.
Encoding and solving problems.
LEO II and other higherorder tols.
 Afternoon: Lab using higherorder logic TPTP and tools; practical
exercises.
 Thursday, September 4

 Morning: Overview and review.
Topics as requested.
 Afternoon: Student presentations of proposed project work.
Open lab for experimentation and playing.
Teamwork on some more advanced exercises.
 Friday, September 5

 Morning and afternoon: Open lab for student project work.
Course Materials
Assessment
 Project (25%). Students will work in groups of up to three, to encode
a domain of their choice (subject to instructor approval), and use
automated reasoning to establish results in the domain.
Some domains we've thought of are:
 Rules of a chosen sport
 Newtonian physics (in an idealized environment)
 The soundness and completeness of resolution based ATP
 Exam (75%). The exam will take place on Friday, 12th September.
Relevant Literature
 H. Barendregt, Lambda calculi with types. In Handbook of Logic in
Computer Science, vol.2, Abramsky, Gabbay, and Maibaum, eds., Oxford
University Press, pp. 118309, 1992.
(In Library)
 Programmierung, by Gert Smolka. An introduction to programming using
Standard ML (in German): http://www.ps.unisb.de/progbuch
Links to Systems and Tools