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