WORKSHOP ABSTRACTS



Colin Stirling
Modal and Temporal Logics with Fixpoints

Abstract
.
I will review results about propositional modal and temporal logics with fixed points and their relationships with other formalisms such as automata on infinite words and infinite trees, games and monadic 2nd-order logic. An issue is whether these results can at all be generalised to interesting fragments of first-order modal and temporal logics. Therefore, I will also review results about the guarded fragment of first-order logic with fixed points.

Martin Lange
Modal mu-calculus and sequential composition.

Abstract
.
In 1999 Markus Mueller-Olm introduced FLC which enriches modal mu-calculus with a sequential composition operator. Following his ideas we define LFLC, its linear time version and present a few results on its expressiveness beyond regular languages. Furthermore, we will consider decidability issues (i.e. satisfiability and model checking) of these logics.

Alexander Bolotov
Clausal Resolution for Linear-Time Temporal Mu-calculus

Abstract
.
In this joint work with Michael Fisher and Clare Dixon a resolution based approach to temporal fixpoint logics has been investigated. Having established the translation from Buchi automata to clausal normal form (SNF) developed for linear-time temporal resolution method, we have, therefore, shown the applicability of the clausal resolution technique to the linear-time temporal mu-calculus, which is equiexpressive with Buchi automata. However, taking into account computational cost of such indirect methods, we have recently been looking at more efficient techniques: direct translation to SNF, definition of the clausal normal form for mu-calculus, and through the translation mu-calculus -> quantified temporal logic -> monadic first order temporal logic with the subsequent application of the clausal resolution technique to the latter logic. These characterisations will be described, together with the translation of primitive (not nested) fixpoints to SNF. We will also discuss main difficulties in defining such direct translation to SNF that arise due to the nesting of minimal and maximal fixpoints even in the case of the alternation free fixpoint logic.

Martin Otto
Least fixed points in the modal, 2-variable and guarded domains.

Abstract
.
2-variable logics and guarded logics have been explored as extensions of modal logics both because of their promising applications and in in order to explore and understand the "good behaviour" of modal logics. I shall dicsuss results and open issues about least fixed points in these three domains, with an emphasis on the comparative study of basic model theoretic questions.


Michael Zakharyashev
Linear and branching time FOTLs: decidable fragments and their applications.

Abstract
.
The aim of the talk is to present a survey of decidable (and undecidable) fragments of first-order temporal logics based on various linear and branching flows of time and show possible applications to knowledge representation and reasoning.

Alan Smaill
First Order Temporal logic embedded in a higher-order framework.

Abstract
.
In joint work with Claudio Castellini, we have been developing an approach to FO temporal logic involving the use of higher-order logic programming characterisations, both of the logical calculi concerned, and of search heursistics for theorem proving in FOTL. These characterisations will be described, together with a discussion of the analogies and disanalogies between theorem proving in inductive domains.

Anatolyi Degtyarev
Towards First-Order Temporal Resolution

Abstract
.
In this talk we extend clausal temporal resolution to the monodic fragment of first-order temporal logic, which has recently been introduced by Hodkinson, Wolter and Zakharyaschev. While a finite Hilbert-like axiomatization of complete monodic first order temporal logic was developed by Wolter and Zakharyaschev, we propose a resolution-based proof system which reduces the satisfiability problem for ground eventuality monodic first-order temporal formulae to the satisfiability problem for formulae of classical first-order logic.

Alexei Lisitza
Experiments with first-order temporal logic theorem proving within LambdaClam proof planning system

Abstract
.
A report on experiments on proving first-order temporal logic formulas under arithmetical translation with LambdaClam will be given.
 
 
 
FFOTL Main Page Outline Registration Participants FFOTL Programme Abstracts Local Info