shankar@SRC.Honeywell.COM (Subash Shankar) (12/01/90)
I am looking for automated (or automatable) proof procedures for temporal logic with quantifiers. Any pointers would be appreciated. (I'll post a summary of E-mail if there's any interest) --- Subash Shankar Honeywell Systems & Research Center MN65-2100 voice: (612) 782 7558 US Snail: 3660 Technology Dr., Minneapolis, MN 55418 shankar@src.honeywell.com srcsip!shankar
shankar@SRC.Honeywell.COM (Subash Shankar) (12/14/90)
A couple of weeks back, I posted a request for literature on proof procedures
for temporal logic with quantifiers. Much thanks to everybody who responded.
A summary of results follows.
From doner%henri@hub.ucsb.edu Sat Dec 1 00:22:52 1990
The state delta verification system developed at Aerospace Corp, is a
proof-checker/program verifier based on temporal logic. Various papers
describing it have been published, but the system itself has not yet
been cleared for public distribution by the sponsoring government agency.
From Rajeev.Gore@computer-lab.cambridge.ac.uk Mon Dec 3 07:43:13 1990
There was something called The Interactive Proof Editor written at
Edinburgh that did first order TL but it required help from the user.
Name was Brian Ritchie, try email to postmaster@uk.ac.ed.lfcs
Some that I extracted from a related request by somebody else last year:
[Sza 87a] A. Szalas, A complete axiomatic characterization of first-order
temporal logic of linear time, Theoret. Comput. Sci. 54, pp.199-214,
1987
[Sza 87b] A. Szalas, Arithmetical axiomatization of first-order
temporal logic, Information processing letters, Vol 26, No. 3,
pp.111-116, 1987
Others that I have dug up:
Martin Abadi and Zohar Manna
Nonclausal Deduction in First-Order Temporal Logic
JACM, April 1990, pp 279
Lincoln A Wallen
Automated Deduction in Nonclassical Logics
MIT Press, 1990
---
Subash Shankar Honeywell Systems & Research Center MN65-2100
voice: (612) 782 7558 US Snail: 3660 Technology Dr., Minneapolis, MN 55418
shankar@src.honeywell.com srcsip!shankar