Nonclausal deduction in first-order temporal logic
- 1 April 1990
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 37 (2) , 279-317
- https://doi.org/10.1145/77600.77617
Abstract
This paper presents a proof system for first-order temporal logic. The system extends the nonclausal resolution method for ordinary first-order logic with equality, to handle quantifiers and temporal operators. Soundness and completeness issues are considered. The use of the system for verifying concurrent programs is discussed and variants of the system for other modal logics are also described.Keywords
This publication has 22 references indexed in Scilit:
- Temporal logic programmingJournal of Symbolic Computation, 1989
- The power of temporal proofsTheoretical Computer Science, 1989
- Modal theorem provingPublished by Springer Nature ,1986
- Adequate proof principles for invariance and liveness properties of concurrent programsScience of Computer Programming, 1984
- Dynamic LogicPublished by Springer Nature ,1984
- Specifying Concurrent Program ModulesACM Transactions on Programming Languages and Systems, 1983
- Modular Verification of Computer Communication ProtocolsIEEE Transactions on Communications, 1983
- Proof Methods for Modal and Intuitionistic LogicsPublished by Springer Nature ,1983
- Using branching time temporal logic to synthesize synchronization skeletonsScience of Computer Programming, 1982
- Assigning meanings to programsPublished by American Mathematical Society (AMS) ,1967