Abstract
Wos has identified the problem of recomputing redundant information in the general setting of automated reasoning. We consider this problem in the setting of logic programming where we are given a formula and a goal and asked to find the instances of the goal that follow from the formula. We can use a proof procedure to find the result. The procedure exhibits redundancy when it finds two results such that one either duplicates or is more specific than the other. We introduce the foothold format, a refinement of linear resolution that admits fewer duplicate proofs than Loveland's popular MESON format. The duplicates arise when reasoning by cases. It leads to proof procedures that compute fewer duplicate substitutions. In some of our examples all duplication is eliminated. The foothold refinement depends on a simple condition that can be checked quickly, and can detect redundancy before the proof is completely generated. This is important from a practical point of view, since the earlier redundancy is detected, the more unnecessary work can be avoided. For some examples the speedup is exponential. We show that the elimination of redundancy also applies to SLI resolution, a procedure for processing disjunctive logic programs.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
C.-L. Chang and R.C.-T. Lee,Symbolic Logic and Mechanical Theorem Proving (Academic Press, New York and London, 1973).
C.C. Green, Theorem-proving by resolution as a basis for question-answering systems, in:Machine Intelligence 4, eds. B. Meltzer and D. Michie (Eisevier, New York), pp. 183–205.
D. Loveland,Automated Theorem Proving: A Logical Basis (North-Holland, Amsterdam, 1978).
J. Minker and A. Rajasekar, A fixpoint semantics for disjunctive logic programs, J. Logic Progr. 9 (1990) 45–74.
F.J. Pelletier, Seventy-five problems for testing automated theorem provers, J. Automated Reasoning 2 (1986) 191–216.
D. Plaisted, A sequent-style model elimination strategy and a positive refinement, J. Automated Reasoning 6 (1990) 389–402.
R. Socher-Ambrosius, How to avoid the derivation of redundant clauses in reasoning systems, J. Automated Reasoning 9 (1992) 77–97.
B. Spencer, Avoiding duplicate proofs, in:Proc. North American Conf. on Logic Programming, eds. S.K. Debray and M. Hermenegildo (MIT Press, 1990) pp. 569–584.
B. Spencer, Linear resolution with ordered clauses, in:Proc. Workshop on Disjunctive Logic Programming Int. Symp. Logic Programming (San Diego, Cal., 1991).
M.E. Stickel, A prolog technology theorem prover, J. Automated Reasoning 4 (1989) 353–380.
L. Wos,Automated Reasoning: 33 Basic Research Problems (Prentice-Hall, Englewood Cliffs, NJ, 1988).
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Spencer, B. Avoiding duplicate proofs with the foothold refinement. Ann Math Artif Intell 12, 117–140 (1994). https://doi.org/10.1007/BF01530763
Issue Date:
DOI: https://doi.org/10.1007/BF01530763