|
Abstract : |
The aim of this paper is to apply the so called mosaic method for proving decidability, Hilbertstyle (strong) completeness and tableau (weak) completeness. The mosaic method was invented by N'emeti to prove decidability of the equational theories of certain classes of algebras of relations, cf. [N'e86], [N'e95]. 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], [Ma96], [Mi96], and [VM96]. 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, |
