Modal and Temporal Logics with Fixpoints
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
Modal mu-calculus and sequential composition.
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
Clausal Resolution for Linear-Time Temporal Mu-calculus
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.
Least fixed points in the modal, 2-variable and guarded domains.
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.
Linear and branching time FOTLs:
decidable fragments and their applications.
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.
First Order Temporal logic embedded in a higher-order framework.
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.
Towards First-Order Temporal Resolution
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
Experiments with first-order temporal logic theorem proving
within LambdaClam proof planning system
A report on experiments on proving first-order temporal logic formulas
under arithmetical translation with LambdaClam
will be given.