Calculational deductive systems, developed by Dijkstra and Scholten and extended by Gries and Schneider, are based on only four inference rules -- Substitution, Leibniz, Equanimity, and Transitivity. The paper, A Calculational Deductive System for Linear Temporal Logic (CDS4LTL), is a survey of the linear temporal logic (LTL) literature and presents all the LTL theorems from the survey, plus many new ones, in a calculational deductive system. This paper improves on the CDS4LTL system by decreasing the number of axioms while at the same time using two newly-discovered axioms as its basis. It presents additional theorems not in CDS4LTL and also extends the presentation of duality. All the theorems have been proved with calculation logic without using the temporal deduction metatheorem.
stanwarford / ras4ltl Goto Github PK
View Code? Open in Web Editor NEWA paper by Wiegley, Staley, and Warford on linear temporal logic.