Abstract:
An approach to applying clausal resolution, a proof method for classical logics suited to mechanisation, to temporal logics has been developed by Fisher. The method invol...Show MoreMetadata
Abstract:
An approach to applying clausal resolution, a proof method for classical logics suited to mechanisation, to temporal logics has been developed by Fisher. The method involves translation to a normal form, classical style resolution within states and temporal resolution between states. The method consists of only one temporal resolution rule and is therefore particularly suitable as the basis of an automated temporal resolution theorem prover. As the application of this temporal resolution rule is the most costly part of the method, involving search amongst graphs, it is on this area we focus. A breadth-first search approach to the application of this rule is presented and shown to be correct. Analysis of its operation is carried out and test results for its comparison to a previously developed depth-first style algorithm given.
Published in: Proceedings Third International Workshop on Temporal Representation and Reasoning (TIME '96)
Date of Conference: 19-20 May 1996
Date Added to IEEE Xplore: 06 August 2002
Print ISBN:0-8186-7528-4