Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures.

*(English)*Zbl 0805.68103Summary: Recently the first author and D. Plaisted [ibid. 9, No. 1, 25-42 (1992; Zbl 0784.68077)] proposed a theorem-proving method, the hyperlinking proof procedure, to eliminate duplication of instances of clauses during the process of inference. A theorem prover, CLIN, which implements the procedure was also constructed. In this implementation, redundant work on literal unification checking, partial unification checking, and duplicate instance checking is performed repetitively, resulting in a large overhead when many rounds of hyperlinking are needed for an input problem. We propose a technique that maintains information across rounds in shared network structures, so that the redundant work in each hyperlinking round can be avoided. Empirical performance comparison has been done between CLIN and CLIN-net, which is the theorem prover with shared network structures, and some results are shown. Problems related to memory overhead and literal ordering are discussed.

##### MSC:

68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |

03B35 | Mechanization of proofs and logical operations |

PDF
BibTeX
XML
Cite

\textit{S.-J. Lee} and \textit{C.-H. Wu}, J. Autom. Reasoning 12, No. 3, 359--388 (1994; Zbl 0805.68103)

Full Text:
DOI

##### References:

[1] | Bledsoe, W.W.: Non-resolution theorem proving,Artificial Intelligence 9 (1977), 1-35. · Zbl 0358.68131 |

[2] | Butler, R. and Overbeek, R.: A tutorial on the construction of high-performance resolution/paramodulation systems, Technical Report ANL-90/30, Argonne National Laboratory, Argonne, Ill., 1990. |

[3] | Chang, C. and Lee, R.:Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973. · Zbl 0263.68046 |

[4] | Charniak, E., Reisbeck C. and McDermott, D.:Artificial Intelligence Programming, Lawrence Earlbaum Assoc., Hillside, N.J., 1980. |

[5] | Christian, J.: Fast knuth-Bendix completion: A summary, inProc. 3rd International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 355, New York, 1990, pp. 551-555. |

[6] | Davis, M. and Putnam, H.: A computing procedure for quantification theory,J. Assoc. Comput. Machinery 7 (1960), 201-215. · Zbl 0212.34203 |

[7] | Forgy, C. L.: Rete: A fast algorithm for the many pattern/many object pattern match problem,Artificial Intelligence 19 (1982), 17-37. |

[8] | Freuder, E. C.: Synthesizing contraint expressions,Comm. Assoc. Comput. Machinery 21 (1978), 958-966. · Zbl 0386.68065 |

[9] | Fujita, H. and Hasegawa, R.: A model generation theorem prover in KL1 using a ramified-stack algorithm, inProc. 8th International Conference on Logic Programming, 1991, pp. 535-548. |

[10] | Giarratano, J. and Riley, G.:Expert Systems: Principles and Programming, PWS-KENT Publishing Company, Boston, 1989. |

[11] | Greenbaum, S.:Input Transformations and Resolution Implementation Techniques for Theorem Proving in First-Order Logic, Ph.D. thesis, University of Illinois at Urbana-Champaign, 1986. |

[12] | Lee, S.-J. and Plaisted, D.: New applications of a fast propositional calculus decision procedure, inProc. 8th Biennial Conference of Canadian Society for Computational Studies of Intelligence, Ottawa, Canada, 1990, pp. 204-211. |

[13] | Lee, S.-J. and Plaisted, D.: Eliminating duplication with the hyperlinking strategy,J. Automated Reasoning 9(1) (1992), 25-42. · Zbl 0784.68077 |

[14] | Lee, S.-J. and Plaisted, D.: Problem solving by searching for models with a theorem prover,Artificial Intelligence (to appear). · Zbl 0941.68740 |

[15] | Loveland, D.:Automated Theorem Proving: A Logical Basis, North-Holland, New York, 1978. · Zbl 0364.68082 |

[16] | Lusk, E. and Overbeek, R.: Non-Horn problems,J. Automated Reasoning 1 (1985), 103-114. · Zbl 0614.68069 |

[17] | McCharen, J., Overbeek, R. and Wos, L.: Complexity and related enhancements for automated theoremproving programs,Computers and Mathematics with Applications 2 (1976), 1-16. · Zbl 0336.68037 |

[18] | McCune, W.: Experiments with discrimination-Tree indexing and path indexing for term retrieval,J. Automatic Reasoning 9 (1992), 147-169. · Zbl 0781.68101 |

[19] | Pelletier, F. J.: Seventy-five problems for testing automatic theorem provers,J. Automated Reasoning 2 (1986), 191-216. · Zbl 0642.68147 |

[20] | Pereira, F.:C-Prolog User’s Manual, SRI International, Menlo Park, California, 1984. |

[21] | Plaisted, D.: A simplified problem reduction format,Artificial Intelligence 18 (1982), 227-261. · Zbl 0497.68058 |

[22] | Plaisted, D. and Greenbaum, S.: A structure-preserving clause form translation.J. of Symbolic Computation 2 (1986), 293-304. · Zbl 0636.68119 |

[23] | Robinson, J.: Theorem proving on the computer,J. Assoc. Comput. Machinery 10 (1963), 163-174. · Zbl 0109.35603 |

[24] | Scales, D. J.: Efficient matching algorithm for the SOAR/OPS5 production system, Technical Report STAN-CS-86-1124, Departments of Computer Sciences, Stanford University, 1986. |

[25] | Sterling, L. and Shapiro, E.:The Art of Prolog, MIT Press, Cambridge, Massachusetts, 1986. · Zbl 0605.68002 |

[26] | Stickel, M. E.: The path-indexing method for indexing terms, Technical Note 473, Artificial Intelligence Center, SRI International, Menlo Park, California, 1989. |

[27] | Stickel, M. E.: A Prolog technology theorem prover: Implementation by an extended Prolog compiler,J. Automated Reasoning 4 (1988), 353-380. · Zbl 0662.68104 |

[28] | Sutcliffe, G.: The TPTP problem library, release v1.0.0, Technical Report, Department of Computer Sciences, James Cook University, 1993. · Zbl 0910.68197 |

[29] | Ullman, J. D.:Database and Knowledge-Base Systems, Vol. 1: Classical Database Systems, Computer Science Press, 1988. |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.