--- res: bibo_abstract: - 'This paper presents a complete axiomatization of fully decidable propositional real-time linear temporal logics with past: the Event Clock Logic (ECL) and the Metric Interval Temporal Logic with past (MITL). The completeness proof consists of an effective proof building procedure for ECL. From this result we obtain a complete axiomatization of MITL by providing axioms translating MITL formulae into ECL formulae, the two logics being equally expressive. Our proof is structured to yield a similar axiomatization and procedure for interesting fragments of these logics, such as the linear temporal logic of the real numbers (LTR).@eng' bibo_authorlist: - foaf_Person: foaf_givenName: Jean foaf_name: Raskin, Jean foaf_surname: Raskin - foaf_Person: foaf_givenName: Pierre foaf_name: Schobbens, Pierre foaf_surname: Schobbens - foaf_Person: foaf_givenName: Thomas A foaf_name: Henzinger, Thomas A foaf_surname: Henzinger foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87 orcid: 0000−0002−2985−7724 bibo_doi: 10.1007/BFb0055625 bibo_volume: 1466 dct_date: 1998^xs_gYear dct_isPartOf: - http://id.crossref.org/issn/9783540648963 dct_language: eng dct_publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik@ dct_title: Axioms for real-time logics@ ...