Bibliography

1

J. Brotherston, A. Degtyarev, M. Fisher and A.Lisitsa, Searching for Invariants using Temporal Resolution, Proceedings of LPAR 2002, (to appear)

2

B. Beckert and J. Posegga.
lean $T^{\!\!\textstyle A}\!\!P$: Lean, Tableau-based Deduction.
Journal of Automated Reasoning, Vol. 15, No. 3, pages 339-358, 1995.

3

A. Bundy.
The use of explicit plans to guide inductive proofs.
In Proc. of 9th International Conference on Automated Deduction Springer-Verlag, 1988.

4

A. Degtyarev and M. Fisher.
Towards first-order temporal resolution.
In Proccedings of KI-2001, volume 2174 of LNAI, 2001.

5

M. Fisher, C. Dixon, and M. Peim.
Clausal temporal resolution.
ACM Transactions on Computation Logic, 2(1), January 2001.

6

M. Fisher.
A resolution method for temporal logic.
In Proc. Twelfth International Joint Conference on Artificial Intelligence (IJCAI). Morgan Kaufman, 1991.

7

I. Hodkinson, F. Wolter, and M. Zakharyaschev.
Fragments of first-order temporal logics.
Annals of Pure and Applied logic, 106:85-134, 2000.

8

A. Lisitsa, $\lambda$ LeanTap: lean deduction in $\lambda$Prolog, University of Liverpool Department of Computer Science Technical Report ULCS-03-17, 2003

9

$\lambda$ Prolog home page, http://www.cse.psu.edu/ dale/lProlog/

10

J. Richardson, A. Smaill, and I. Green.
System description: proof planning in higher-order logic with lambdaclam.
In Proc. of CADE'15, volume 1421 of LNAI, 1998.

11

Teyjus web page, http://teyjus.cs.umn.edu/