On Effective Deductive Procedure for a Restricted First-order Linear Temporal Logic
by
Regimantas Pliuskevicius
Institute of Mathematics and Informatics, Akademijos 4, Vilnius 2600, LITHUANIA

An effective deductive procedure is presented for the so-called D-sequents of a restricted first order linear temporal logic with temporal operators ``next'' and ``always''. The procedure is based on the contraction-free (see, e.g., [1]) new type infinitary calculus for D-sequents. The proposed procedure consists of the preparatory part and the main part. In the preparatory part a given D-sequent is automatically reduced to some canonical form, the so-called ``saturated" sequent. The main part consists of two separate sections. In the first section the inductive hypothesis is automatically generated. In the second section an automatic validation of the given D-sequent (using generated inductive hypothesis) is performed. The attractive properties of the proposed procedure are ``temporal linearity" makes it possible to restricted oneself to linear-like derivations of the temporal part of the given D-sequent. `` Space-preserving" allows to generate the sequents having the same length as the initial D-sequent. It should be stressed that both the generation of inductive hypothesis and validation of the given sequent are carried out by the uniform saturation procedures (adopted and revised for D-sequents from [3, 4, 5]) replacing the application of omega-type rule for ``always" operator. The general shape of D-sequents [6] was proposed by V. Orevkov and it is a specialization of a normal form from [2]. The soundness and completeness of the proposed procedure are proved.

References

[]

Dyckhoff, R.: Contraction-free sequent calculi for intuitionistic logic, JSL, 51 (1992) 795-807.

[]

Fisher, M.: A normal form for first order temporal formulae. LNCS 607 (1992) 370-384.

[]

Pliuskevicius, R.: On saturated calculi for a linear temporal logic. LNCS 711 (1993) 640-649.

[]

Pliuskevicius, R.: The saturated tableaux for linear miniscoped Horn-like temporal logic. Journal of Automated Reasoning 13 (1994) 51-67.

[]

Pliuskevicius, R.: Replacement of induction by similarity saturation in a first order linear temporal logic Journal of Applied Non-Classical Logics 8(1-2) (1998) 141-169.

[]

Pliuskevicius, R.: Quantified contradiction-free infinitary calculus for a restricted first-order linear temporal logic (in Russian). Lithuanian Mathematical Journal (submitted).

Date received: March 15, 1999

Copyright © 1999 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Conferences Inc. Document # cacs-21.