Axiomatising first-order temporal logic: Until and since over linear time
The author presents a complete axiomatisation for first-order temporal logic with the connectives \(U\) (Until) and \(S\) (Since) over all linear time flows. Adding two more axioms, he obtains also a complete axiomatisation over the rational numbers flow of time. The result extends the corresponding one of Burgess for propositional logic, as well as Scott's result for first-order temporal logic with the connectives \(F\) and \(P\), but the proof is by no means a straightforward generalization of them. In fact, he avoids ``datings for reducing \(U\), \(S\) to \(F\) and \(P\), and unnatural rules. For the construction of the model of a consistent set of formulas, he uses subtle and nice techniques in order to cope with completeness of quantified formulas (``omega completeness). The model is constructed a the limit of finite pieces in countably many steps over a subset of the rationals.
- A complete axiomatic characterization of first-order temporal logic of linear time
- A complete deductive-system for since-until branching-time logic
- An axiomatization for until and since over the reals without the IRR rule
- An Axiomatization of the Temporal Logic with Until and Since over the Real Numbers
- Arithmetical axiomatization of first-order temporal logic
- scientific article; zbMATH DE number 747023 (Why is no real title available?)
- scientific article; zbMATH DE number 52331 (Why is no real title available?)
- scientific article; zbMATH DE number 3559512 (Why is no real title available?)
- scientific article; zbMATH DE number 1028824 (Why is no real title available?)
- scientific article; zbMATH DE number 1028834 (Why is no real title available?)
- scientific article; zbMATH DE number 757647 (Why is no real title available?)
- Model theory for tense logics
- On some U,S-tense logics
- A complete axiomatic characterization of first-order temporal logic of linear time
- Incompleteness of first-order temporal logic with until
- An axiomatization for until and since over the reals without the IRR rule
- Decidable fragments of first-order temporal logics
- A decision procedure and complete axiomatization for projection temporal logic
- A survey on temporal logics for specifying and verifying real-time systems
- The temporal logic of linear time frames with inductions axiom
- scientific article; zbMATH DE number 1678387 (Why is no real title available?)
- On the Priorean temporal logic with \([d]\) over the real line
- First-Order Linear-Time Epistemic Logic with Group Knowledge: An Axiomatisation of the Monodic Fragment
- scientific article; zbMATH DE number 1536551 (Why is no real title available?)
- An Axiomatization of the Temporal Logic with Until and Since over the Real Numbers
- scientific article; zbMATH DE number 2086407 (Why is no real title available?)
- scientific article; zbMATH DE number 757647 (Why is no real title available?)
- scientific article; zbMATH DE number 5790393 (Why is no real title available?)
- On the axiomatizability of some first-order spatio-temporal theories
- Peano arithmetic as axiomatization of the time frame in logics of programs and in dynamic logics
- Nesting until and since in linear temporal logic
- Quantified epistemic logics for reasoning about knowledge in multi-agent systems
This page was built for publication: Axiomatising first-order temporal logic: Until and since over linear time
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2563451)
