0
$\begingroup$

In what paper(s), textbook(s), and/or classnote(s) can I find a detailed proof of the completeness of a certain proof system for PLTL (Propositional Linear Temporal Logic)?

$\endgroup$
7
  • $\begingroup$ Logics aren't complete but proof systems are. Which one did you have in mind? $\endgroup$
    – Kai
    Commented Mar 9, 2023 at 5:04
  • $\begingroup$ @Kai The proof system. Where can I find a detailed proof that a certain proof system of PLTL is complete? $\endgroup$
    – Evan Aad
    Commented Mar 9, 2023 at 8:15
  • $\begingroup$ Sorry, I meant which proof system did you have in mind? Got a reference? $\endgroup$
    – Kai
    Commented Mar 9, 2023 at 23:04
  • $\begingroup$ @Kai I'm especially interested in Fred Kroeger's system as delineated in chapter 5 The Formal System $\Sigma_{\textrm{TA}}$ of his textbook Temporal Logic of Programs (Springer 1987). He presents a detailed proof of its completeness in chapter 6 (Theorem 6.10 on p. 36), but I think the proof is incorrect, so I'm looking for other proofs. (More accurately, it is the proof of Theorem 6.9 on the Satisfiability of $\Sigma_{\text{TA}}$ which I deem incorrect, but the completeness proof makes use of it.) $\endgroup$
    – Evan Aad
    Commented Mar 10, 2023 at 15:03
  • $\begingroup$ What's your issue with the proof of Kröger's Theorem 6.9? (Mind you, Kröger's $\mathcal{L)_{\mathrm{TA}}$ is not exactly LTL but I believe they are equally expressive.) $\endgroup$
    – Kai
    Commented Mar 11, 2023 at 1:06

1 Answer 1

1
$\begingroup$

The proof system "DUX" in On the temporal analysis of fairness. D Gabbay, A Pnueli, S Shelah, J Stavi. POPL 1980 is perhaps closest to what you're after. Being a conference paper, the completeness proof is rather terse but with a bit of luck you can fill in the details.

$\endgroup$
1
  • $\begingroup$ I'm interested in a detailed proof, not a terse one. But this is better than nothing. Thanks. $\endgroup$
    – Evan Aad
    Commented Mar 11, 2023 at 8:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.