Incompleteness of first-order temporal logic with until (Q1123184): Difference between revisions

From MaRDI portal
Added link to MaRDI item.
Set OpenAlex properties.
 
(4 intermediate revisions by 3 users not shown)
Property / author
 
Property / author: Andrzej Szałas / rank
Normal rank
 
Property / reviewed by
 
Property / reviewed by: Q593640 / rank
Normal rank
 
Property / author
 
Property / author: Andrzej Szałas / rank
 
Normal rank
Property / reviewed by
 
Property / reviewed by: Cristian Masalagiu / rank
 
Normal rank
Property / MaRDI profile type
 
Property / MaRDI profile type: MaRDI publication profile / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3220545 / rank
 
Normal rank
Property / cites work
 
Property / cites work: A generalized nexttime operator in temporal logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Concerning the semantic consequence relation in first-order temporal logic / rank
 
Normal rank
Property / full work available at URL
 
Property / full work available at URL: https://doi.org/10.1016/0304-3975(88)90045-x / rank
 
Normal rank
Property / OpenAlex ID
 
Property / OpenAlex ID: W2092497338 / rank
 
Normal rank

Latest revision as of 11:11, 30 July 2024

scientific article
Language Label Description Also known as
English
Incompleteness of first-order temporal logic with until
scientific article

    Statements

    Incompleteness of first-order temporal logic with until (English)
    0 references
    0 references
    0 references
    1988
    0 references
    The version of first-order temporal logic (with equality) chosen in this paper is essentially that introduced by \textit{Z. Manna} and \textit{A. Pnueli} [Verification of concurrent programs: the temporal framework, in: The correctness problem in computer science (\textit{R. S. Boyer} and \textit{J S. Moore} (eds.)), 215-273 (1981; Zbl 0476.68009)]; it uses the temporal modalities ``always'', ``sometimes'', ``next time'', ``until'' and ``at next''. It is shown that this logic is weakly incomplete (the set of tautologies over an arbitrary signature is not r.e.) and strongly incomplete (the set of tautologies is r.e. for no signature). Although the first claim is a consequence of the second, they are separately presented. The proof of the first theorem is analogous to the proof of incompleteness of second-order prediate logic. It is based on Trakhtenbrot's theorem and the fact that finite structures are characterizable in temporal logic (this result is interesting by its own). For the second theorem, the technique consists in reducing the complement of the halting problem for Turing machines to the problem whether a temporal formula (only with \(``='')\) is a tautology.
    0 references
    incompleteness
    0 references
    first-order temporal logic
    0 references
    temporal modalities
    0 references
    halting problem
    0 references

    Identifiers