Reasoning in Monodic First-Order Temporal Logic

Ullrich Hustadt (University of Liverpool)

NICTA LC SEMINAR

DATE: 2009-11-26
TIME: 16:00:00 - 17:00:00
LOCATION: NICTA - 7 London Circuit
CONTACT: JavaScript must be enabled to display this email address.

ABSTRACT:
Temporal logics have long been considered as appropriate formal languages for specifying important computational properties of hardware and software systems. However, while various propositional temporal logics have been used very successfully in this context, the same has not been true to the same extent for first-order temporal logic. One reason is that first-order temporal logic is not even semi-decidable, which limits its usefulness for the purpose of automatic verification. A prominent fragment of first-order temporal logic which has the completeness property is the monodic fragment. Besides completeness, the monodic fragment enjoys a number of other beneficial properties, e.g. the existence of non-trivial decidable subclasses, automated deduction, etc. Moreover, reasoning in other formalisms, like temporal logics of knowledge, can be reduced to reasoning in the monodic fragment.

In this talk I will give an overview of the monodic fragment of first-order temporal logic and of resolution-based calculi for reasoning in this logic. The main focus of the talk will be the problems associated with turning such calculi into practical theorem provers and how these can be solved.
BIO:
Ullrich Hustadt received his MSc/MPhil in Computer Science from the University of Dortmund in 1991 and his PhD in Computer Science from Saarland University in 1999. From 1991 to 1998 he was a Research Fellow in the Programming Logics Research Group at the Max-Plank-Institut fur Informatik in Saarbrucken, Germany. He joined the Department of Computer Science, University of Liverpool, in January 2001 and is currently a Reader in the Logic and Computation Research Group. His interests include theoretical and practical approaches to the decision problem in classical and non-classical logics, in particular, resolution decision procedures, and their realisation, evaluation and application.