Connection-driven inductive theorem proving

被引：0
作者：
Kreitz C. [1 ]
Pientka B. [2 ]
机构：
[1] Department of Computer Science, Cornell-University, Ithaca
[2] Department of Computer Science, Carnegie Mellon University, Pittsburgh
来源：
Studia Logica | 2001年 / 69卷 / 2期
关键词：
Induction; Matrix Methods; Program Synthesis; Rippling; Theorem Proving;
D O I：
10.1023/A:1013874024997
中图分类号：
学科分类号：
摘要：
We present a method for integrating rippling-based rewriting into matrixbased theorem proving as a means for automating inductive specification proofs. The selection of connections in an inductive matrix proof is guided by symmetries between induction hypothesis and induction conclusion. Unification is extended by decision procedures and a rippling/reverse-rippling heuristic. Conditional substitutions are generated whenever a uniform substitution is impossible. We illustrate the integrated method by discussing several inductive proofs for the integer square root problem as well as the algorithms extracted from these proofs. © 2001 Kluwer Academic Publishers.
引用
收藏
页码：293 / 326
页数：33
相关论文
共 36 条
  • [1] Allen S., Constable R., Eaton R., Kreitz C., Lorigo L., The Nuprl Open Logical Environment, Lecture Notes in Artificial Intelligence, 1831, pp. 170-176, (2000)
  • [2] Altenkirch T., Gaspes V., Nordstrom B., Von Sydow B., A User's Guide to ALF', (1994)
  • [3] Andrews P., Theorem-Proving via General Matings, Journal of the Association for Computing Machinery, 28, 2, pp. 193-214, (1981)
  • [4] Armando A., Smaill A., Green I., Automatic synthesis of recursive programs: The proof-planning paradigm, Automated Software Engineering, 6, 4, pp. 329-356, (1999)
  • [5] Autexier S., Hutter D., Mantel H., Schairer A., Inka 5.0 - A logical voyager, Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, 1632, pp. 207-211, (1999)
  • [6] Basin D., Walsh T., A Calculus for and Termination of Rippling, Journal of Automated Reasoning, 16, 2, pp. 147-180, (1996)
  • [7] Bates J.L., Constable R.L., Proofs as Programs, ACM Transactions on Programming Languages and Systems, 7, 1, pp. 113-136, (1985)
  • [8] Bibel W., On Matrices with Connections, Journal of the Association for Computing Machinery, 28, pp. 633-645, (1981)
  • [9] Bibel W., A deductive solution for plan generation, New Generation Computing, 4, pp. 115-132, (1986)
  • [10] Bibel W., Automated Theorem Proving, (1987)
1234