Logic Programming as a Bases for Lean Deduction: Achieving Maximal Efficiency from Minimal Means.
Bernhard Beckert, Joachim Posegga · WLP · 1994
Researchers in Automated Reasoning often complain that there are sparse applications of the techniques they develop. One reason might be that implementation-oriented research favors huge and highly complex systems and that this does not suit the needs of many applications.1 It is hard to see how to apply these systems – besides using them as a black box. Adaptability, however, is an important criterion for applying techniques; this discrepancy can be overcome by using lean theorem provers. The idea of lean deduction is to achieve maximal efficiency from minimal means. Every possible effort is made to eliminate overhead; based on experience in implementing (complex) deduction systems, only the most important and efficient techniques and methods are implemented. Logic programming languages provide an ideal tool for implementing lean deduction, as they offer a level of abstraction that is close to the needs for building first-order deduction systems. The Prolog program shown in Figure 1, called leanTAP (Beckert & Posegga, 1994b), is an instance of such a lean deduction system: it implements a complete and sound theorem prover for first-order logic in Skolemized negation normal form. The underlying calculus is based on free-variable semantic tableaux (Fitting, 1990) (we shall explain the program in Section 2). Our approach surely does not lead to deduction systems that are superior to highly sophisticated theorem provers like Otter (McCune, 1990) or Setheo (Letz et al., 1992); these are better on solving difficult problems. However, many applications do not require deduction which is as complex as the state of the art in automated theorem proving. Furthermore, there are often strong constraints on the time allowed for deduction. In such areas our approach can be extremely useful: it offers high inference rates on simple to moderately complex problems and a high degree of adaptability. Another important argument for lean deduction is safety: It is easily possible to verify the couple of lines of standard Prolog implementing leanTAP (Beckert & Posegga, 1994a; Posegga & Schmitt, 1995); verifying thousands of lines of C code, however, is hard—if not impossible—in practice.