Advertisement
Published in:
13-02-2020
Loop-Type Sequent Calculi for Temporal Logic
Published in: Journal of Automated Reasoning | Issue 8/2020
Log inActivate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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 \(\mathbf{G} _\text {L}{} \mathbf{T} \) for PLTL with the temporal operators “next” and “henceforth always” (\({\mathbf{PLTL}}^{n,a}\)) is considered at first. We prove that all rules of \(\mathbf{G} _\text {L}{} \mathbf{T} \) are invertible and that the structural rules of weakening and contraction, as well as the rule of cut, are admissible in \(\mathbf{G} _\text {L}{} \mathbf{T} \). We describe a decision procedure for \({\mathbf{PLTL}}^{n,a}\) based on the introduced calculus \(\mathbf{G} _\text {L}{} \mathbf{T} \). Afterwards, we introduce a sound and complete sequent calculus \(\mathbf{G} _\text {L}{} \mathbf{T} ^\mathcal {U}\) for PLTL with the temporal operators “next” and “until”.