Loop-Type Sequent Calculi for Temporal Logic
- PDF / 388,749 Bytes
- 22 Pages / 439.37 x 666.142 pts Page_size
- 48 Downloads / 206 Views
Loop-Type Sequent Calculi for Temporal Logic R. Alonderis1 · R. Pliuškeviˇcius1 · A. Pliuškeviˇciene˙ 1 · H. Giedra1 Received: 4 April 2019 / Accepted: 16 January 2020 © Springer Nature B.V. 2020
Abstract Various types of calculi (Hilbert, Gentzen sequent, resolution calculi, tableaux) for propositional linear temporal logic (PLTL) have been invented. In this paper, a sound and complete loop-type sequent calculus GL T for PLTL with the temporal operators “next” and “henceforth always” (PLTLn,a ) is considered at first. We prove that all rules of GL T are invertible and that the structural rules of weakening and contraction, as well as the rule of cut, are admissible in GL T. We describe a decision procedure for PLTLn,a based on the introduced calculus GL T. Afterwards, we introduce a sound and complete sequent calculus GL TU for PLTL with the temporal operators “next” and “until”. Keywords Temporal logics · Sequent calculi · Derivation loops
1 Introduction Propositional linear temporal logic (PLTL) is used in computer science for specification and verification of programs [8,11]. Cut-free sequent calculi provide clear and convenient means for validity checking of sequents (formulas) by performing backward proof-search. To check if an arbitrary sequent S is derivable in such a calculus, the derivation rules of the calculus are applied backward to S and the resulting sequents. In the cases where the premises of the derivation rules are simpler than the conclusions, the process is finite and each time the same, routine: determine the outermost symbol of a formula and apply the corresponding derivation rule. (If the calculus contains rules the premises of which are not simpler than the corresponding conclusions, then some additional means is required to ensure termination of backward proof-search.) The rule of cut destroys such a procedure since this rule is not
B
R. Alonderis [email protected] R. Pliuškeviˇcius [email protected] A. Pliuškeviˇcien˙e [email protected] H. Giedra [email protected]
1
Vilnius University Institute of Data Science and Digital Technologies, Akademijos 4, 2600 Vilnius, Lithuania
123
R. Alonderis et al.
deterministic from the backward perspective. It contains the formula (called the cut formula) in the premises that is not specified in the conclusion. Therefore we do not know how many times this rule should be applied and what cut formula should be chosen each time so that to derive the considered sequent or to prove that it is not derivable. Comparing with other traditional modal logics, construction of sound and complete cutfree sequent calculi for PLTL is rather problematic. We would like to mention here the following cut-free sequent calculi for PLTL considered in the literature: 1. Infinitary sequent calculi containing the ω-type induction rule [25] n
→ , φ → , φ . . . → , . . . φ . . . (→ ω ), → , φ where ‘’ and ‘’ stand for the temporal operators “next” and “henceforth always”, respectively. Finitization o
Data Loading...
