A couple of weeks back, I posted a request for literature on proof procedures
for temp{*filter*}logic with quantifiers. Much thanks to everybody who responded.
A summary of results follows.
The state delta verification system developed at Aerospace Corp, is a
proof-checker/program verifier based on temp{*filter*}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.
There was something called The Interactive Proof Editor written at
Edinburgh that did first order TL but it required help from the user.
Some that I extracted from a related request by somebody else last year:
[Sza 87a] A. Szalas, A complete axiomatic characterization of first-order
temp{*filter*}logic of linear time, Theoret. Comput. Sci. 54, pp.199-214,
1987
[Sza 87b] A. Szalas, Arithmetical axiomatization of first-order
temp{*filter*}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 Temp{*filter*}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