Temporal-Logic Theorem Proving

摘要

This dissertation presents a novel proof system for temporal logic. The system is based on the classical nonclausal resolution method, and involves a special treatment of quantifiers and temporal operators. Unfortunately, no effective proof method for temporal logic can be complete. The authors investigate soundness and completeness issues for the resolution system and for other related systems. In particular, they establish that a simple extension of the resolution system is as powerful as Peano Arithmetic. The most immediate application of the resolution system is in the verification of sequential and concurrent programs. The authors discuss the role of temporal reasoning in proofs of program correctness and give examples of resolution proofs that originate in the verification of specific programs. The authors explore the use of temporal logic as a programming language. They suggest that a specialized temporal resolution system could interpret programs in this language. They also provide analogous resolution systems for other useful modal logics, such as certain modal logics of knowledge and belief.