Refuting conjectures in first-order theories

Abstract

Given some first-order theory, a formula (also called a conjecture) may or may not be a theorem of some theory. A theorem prover attempting to prove that the given formula is a theorem may terminate, proving that the formula is (or isn't) a theorem or run forever (in practice the theorem prover will usually halt when some resource is exhausted). In the latter case we are left with an unanswered question about the status of the formula. There are basically two ways to proceed. First, accept the limitations of the theorem prover and the inconclusiveness of the result or second, attempt to use some other technique to make a judgement about the status of the given formula. So far there seems to be very little research exploring the detection of non-theorems in first-order logic. Most theorem provers concentrate on the detection of theorems and the automatic detection of non-theorems is usually neglected. For resolution based theorem provers a reason for this might be that refutation completeness gives a strong incentive to concentrate on proving theorems as we are certain that the theorem prover will answer affirmatively, in finite time, if the formula is indeed a theorem. In general, such a result does not hold if the formula is not a theorem. One general system that can be used to refute conjectures is based on meta-programming, partial evaluation and regular approximations. The idea is to approximate the behaviour of a proof procedure on a specific theorem proving problem. If the generated approximation is empty we have a proof that the formula we are interested in is not a theorem of the particular theory. As failure is decidable in the approximation, this can be done in finite time. Another general system that is capable of refuting conjectures is FINDER (Finite Domain Enumerator). It takes as input a first-order theory, expressed as a set of clauses, and gives as output the models of that theory with domains of given finite cardinality. We developed a system dedicated to detecting failure in definite logic programs (refuting conjectures in Horn theories). Our system uses a top-down evaluation strategy with tabulation and constraint logic programming technology as its basic mechanisms. As FINDER has no equivalent of a top-down strategy, it behaves poorly on many problems with huge search spaces. FINDER is at least an order of magnitude faster in raw speed than our prototype system, but our results suggests that our basic strategy (using a goal directed strategy with tabulation) is sound and scales up better than the bottom-up strategy used in FINDER. However, it lacks in power compared to FINDER as it is only designed to handle Horn clauses, where FINDER takes as input first-order clauses. The obvious question now is if we can extend our top-down strategy to cover first-order theories and formulas. Unfortunately such an extension is not straightforward as we rely heavily on results from logic programming for success. However, there is a way in which the given results for our system can be extended to the first-order case. The idea is to use meta-programming to "reduce" the first-order problem to a Horn clause problem and furthermore to use program specialisation to reduce the overhead introduced by the meta-program. In the paper we explain the proposed approach in more detail and give some preliminary results and conclusions.