Implementing Clausal Resolution

Aim

The aim of this project is to implement a fully automatic temporal resolution theorem-prover based on [1].

Background

Resolution was proposed as a proof procedure by Robinson in 1965 [5] for propositional and first-order logics. Resolution was claimed to be ``machine-oriented" as it was particularly suitable for proofs to be performed by computer having only one rule of inference that may have to be applied many times. To check the validity of a logical formula P, it is negated and ~P is translated into a normal form. The resolution inference rule is applied repeatedly and new inferences added to the set. If a contradiction ( false) is derived then ~P is unsatisfiable and the original formula P must therefore be valid. The process of determining the unsatisfiability of the negation of a formula is known as refutation. The resolution proof procedure is refutation complete for classical logic as, when applied to an unsatisfiable formula, the procedure is guaranteed to produce false. Efficient theorem provers for propositional and first-order classical logics based on resolution have been developed eg OTTER [3].

Temporal logics are extensions of classical logic, with operators that deal with time. They have been used in a wide variety of areas within Computer Science and Artificial Intelligence for example robotics [6], databases [7], hardware verification [2] and agent based systems [4]. In particular, temporal logics have been used successfully in the specification of safety, liveness and fairness properties of a range of dynamic systems. Such a logical representation of a system then permits the analysis of the systems properties via logical proof.

As part of our ongoing research we have developed a proof method for temporal logics based upon clausal resolution [1]. This involves the transformation of temporal formulae into a normal form, followed by the application of a classical style resolution rule to formulae that occur at the same moment of time. Finally a novel temporal resolution rule is applied that resolves contradictory formula that hold over a time period. The temporal resolution method has been defined, proved correct and has been extended to more complex logics. Whilst we have extensively considered the theoretical aspects of the system, to continue developing this research we need a robust implementation with which to experiment. In particular we would use the developed system to prove properties of complex distributed systems which can be specified using temporal logics, to feed into the development of strategies designed to guide proof search and to use as a starting point for implementing resolution for extensions of the logic.

References

1

M. Fisher, C. Dixon, and M. Peim.
Clausal Temporal Resolution.
ACM Transactions on Computational Logic, 2(1), January 2001.

2

G. J. Holzmann.
The Model Checker Spin.
IEEE Trans. on Software Engineering, 23(5):279--295, May 1997. Special Issue on Formal Methods in Software Practice.

3

W. W. McCune.
OTTER 2.0 Users Guide.
Argonne National Laboratory, 9700 South Cass Avenue, Argonne, Illinois 60439-4801, March 1990.ANL-90/9.

4

A. S. Rao and M. P. Georgeff.
Decision procedures for BDI logics.
Journal of Logic and Computation, 8(3):293--342, 1998.

5

J. A. Robinson.
A Machine--Oriented Logic Based on the Resolution Principle.
ACM Journal, 12(1):23--41, January 1965.

6

M. P. Shanahan.
Solving the Frame Problem.
MIT Press, 1997.

7

A.~Tansel, editor.
Temporal Databases: theory, design, and implementation.
Benjamin/Cummings, 1993.