TY - BOOK
T1 - Search strategies for resolution in temporal logics
AU - Dixon, C.
PY - 1996
Y1 - 1996
N2 - In this paper we give and evaluate the algorithms for a fully automated temporal resolution theorem prover. An approach to applying resolution, a proof method for classical logics suited to mechanisation, to temporal logics has been developed by Fisher. As the application of the temporal resolution rule is the most costly part of the method, involving search amongst graphs, we propose different algorithms on which to base an implementation. The paper concludes with a comparison of their performance.
AB - In this paper we give and evaluate the algorithms for a fully automated temporal resolution theorem prover. An approach to applying resolution, a proof method for classical logics suited to mechanisation, to temporal logics has been developed by Fisher. As the application of the temporal resolution rule is the most costly part of the method, involving search amongst graphs, we propose different algorithms on which to base an implementation. The paper concludes with a comparison of their performance.
KW - Temporal resolution
KW - Temporal logic
KW - Linear temporal logic
KW - Disjunctive normal form
KW - Start node
UR - http://www.scopus.com/inward/record.url?eid=2-s2.0-84957714518&partnerID=MN8TOARS
U2 - 10.1007/3-540-61511-3_121
DO - 10.1007/3-540-61511-3_121
M3 - Book
T3 - Lecture notes in computer science
BT - Search strategies for resolution in temporal logics
ER -