MA@SAIL.STANFORD.EDU (Martin Abadi) (10/01/86)
PhD Oral Examination Wednesday, October 8, 2:15 PM Margaret Jacks Hall 146 Temporal Theorem Proving Martin Abadi Computer Science Department In the last few years, temporal logic has been applied in the specification, verification, and synthesis of concurrent programs, as well as in the synthesis of robot plans and in the verification of hardware devices. Nevertheless, proof techniques for temporal logic have been quite limited up to now. This talk presents a novel proof system R for temporal logic. Proofs are generally short and natural. The system is based on nonclausal resolution, an attractive classical logic method, and involves a special treatment of quantifiers and modal operators. Unfortunately, no effective proof system for temporal logic is complete. We examine soundness and completeness issues for R and other systems. For example, a simple extension of our resolution system is as powerful as Peano Arithmetic. (Fortunately, refreshments will follow the talk.) Like classical resolution, temporal resolution suggests an approach to logic programming. We explore temporal logic as a programming language and a temporal resolution theorem prover as an interpreter for programs in this language. Other modal logics have found a variety of uses in artificial intelligence and in the analysis of distributed systems. We discuss resolution systems analogous to R for the modal logics K, T, K4, S4, S5, D, D4, and G.