The Mosaic Method for Temporal Logics

Maarten Marx, Szabolcs Mikulas and Mark Reynolds

Abstract

The aim of this paper is to apply the so called mosaic method for proving decidability, Hilbert-style (strong) completeness and tableau (weak) completeness.

The mosaic method was invented by István Németi to prove decidability of the equational theories of certain classes of algebras of relations, cf. [Nem86], [Nem95]. The idea is to show that the existence of a model is equivalent to the existence of a finite set of partial models, called mosaics. This gives us a decision procedure, and, intuitively, a systematic procedure to check the theoremhood of a certain formula.

Recently the mosaic method has been applied to prove decidability, Hilbert-style axiomatizability and complexity results for various modal logics, cf., e.g., [HHMMR], [Mik96], and [vene:moda96].

In this paper, we try to make explicit the connection between the mosaic method and tableau systems. Using the original idea of a mosaic decidability proof we will define a complete tableau systems for linear temporal logic. This seems to be a new result, since we will not assume anything about the linear order. We will also prove completeness and decidability. These results are well known, but we think using mosaics the proofs become much simpler. In the last section we will show how to modify the method to obtain similar results for special linear flows of time, e.g., discrete, dense, with or without endpoints, substructures of whole numbers.

Full Paper

Postscript version March 2000

Status

Accepted to appear in proceedings of TABLEAUX'2000.

Online theorem-prover

This theorem-prover uses the temporal mosaic idea to decide the satisfiability or otherwise of formulas in the temporal language with F and P over the class of all linear flows of time.

Bibtex

@inproceedings{MMR:tempmos,
author="M. Marx and S. Mikulas and M. Reynolds",
title="The Mosaic Method for Temporal Logics",
editor="R. Dyckoff",
booktitle="TABLEAUX'2000",
publisher="?",
year="to appear 2000",
}

References

@phdthesis{Nem86,
author="I. N\'emeti",
title="Free Algebras and Decidability in Algebraic Logic",
school="Hungarian Academy of Sciences, Budapest",
note="In Hungarian",
year=1986
}

@inproceedings{Nem95,
author="I. N\'emeti",
title="Decidable versions of first order logic and cylindric-relativized set algebras",
editor="L. Csirmaz and D. Gabbay and M. de Rijke",
booktitle="Logic Colloquium '92",
publisher="CSLI Publications",
year="1995",
pages="171--241"
}

@incollection{HHMMR,
author="R. Hirsch and I. Hodkinson and M. Marx and S. Mikul\'as and M. Reynolds",
title="Mosaics and step-by-step. {Remarks on ``A modal logic of relations}''",
booktitle="Logic at Work. Essays Dedicated to the Memory of {Helena} {Rasiowa}",
editor=" E. Orlowska",
series = "Studies in Fuzziness and Soft Computing",
volume="24",
publisher="Springer-Verlag",
place="Berlin/Heidelberg",
isbn="3-7908-1164-5",
year="1999",
pages = {158--167}
}

@article{Mik96,
author="S. Mikul\'as",
title="Taming First-order Logic",
journal="Journal of the IGPL",
volume=6,
number=2,
pages="305-316",
year="1998"
}

@incollection{vene:moda96,
author = "Y. Venema and M. Marx",
title = "A Modal Logic of Relations",
booktitle="Logic at Work: Essays Dedicated to the Memory of Helena Rasiowa",
editor=" E. Orlowska",
publisher="Springer-Verlag",
place="Berlin/Heidelberg",
isbn="3-7908-1164-5",
year="1999"
}