1st Order Temporal Logic 
Author Message
 1st Order Temporal Logic

I am looking for automated (or automatable) proof procedures for temp{*filter*}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



Wed, 19 May 1993 05:02:26 GMT  
 1st Order Temporal Logic
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



Tue, 01 Jun 1993 06:28:46 GMT  
 
 [ 2 post ] 

 Relevant Pages 

1. 1st order logic question about Kleene star operator

2. Post-doctoral Fellowship in Temporal Logic Programming (Hamilton, New Zealand)

3. Temporal logic programming

4. Post-doctoral Fellowship in Temporal Logic Programming (New Zealand)

5. Post-doctoral Fellowship in Temporal Logic Programming (Hamilton, New Zealand)

6. Temporal logic programming

7. Propositional Temporal Logic

8. Temporal logic (re)sources: A summary (900+ lines!)

9. Theorem Provers for Temporal Logic

10. temporal logic

11. Definitive temporal logic source

12. Temporal Logic Programming

 

 
Powered by phpBB® Forum Software