🚀 go-pugleaf

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