The use of embeddings to provide a clean separation of term and annotation for higher order rippling. (English) Zbl 1216.68232
Summary: Rippling is a proof search guidance technique with particular application to proof by mathematical induction. It is based on a concept of annotating the differences between two terms. In its original formulation this annotation was only appropriate to first-order formulae. We use a notion of embedding to adapt these annotations appropriately for higher-order syntax. This representation simplifies the theory of annotated terms, no longer requiring special substitution and unification theorems. A key feature of the representation is that it provides a clean separation of the term and the annotation. We illustrate this with selected examples using our implementation of these ideas in \(\lambda\)Clam.
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
References:
| [1] | Basin, D., Walsh, T.: A calculus for and termination of rippling. J. Autom. Reason. 16(1–2), 147–180 (1996) · Zbl 0847.68105 · doi:10.1007/BF00244462 |
| [2] | Boudet, A., Comon, H.: About the theory of tree embedding. In: Gaudek, M.-C., Jouannaud, J.-P. (eds.) TAPSOFT ’93: Theory and Practice of Software Development. Lecture Notes in Computer Science, vol. 668, pp. 376–390. Springer, Berlin (1993) |
| [3] | Bundy, A.: A science of reasoning. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic: Essays in Honor of Alan Robinson, pp. 178–198. MIT, Cambridge (1991) |
| [4] | Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-Level Guidance for Mathematical Reasoning. Cambridge Tracts in Theoretical Computer Science, vol. 56. Cambridge University Press, Cambridge (2005) · Zbl 1095.68108 |
| [5] | Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: a heuristic for guiding inductive proofs. Artif. Intell. 62, 185–253 (1993, Also available from Edinburgh as DAI Research Paper No. 567) · Zbl 0789.68121 · doi:10.1016/0004-3702(93)90079-Q |
| [6] | Dennis, L.A.: Program slicing and middle-out reasoning for error location and repair. In: Disproving: Non-Theorems, Non-Validity and Non-Provability (2006) |
| [7] | Dennis, L.A., Brotherston, J.: {\(\lambda\)}clam v4: User/Developer’s Manual. Mathematical Reasoning Group, Division of Informatics, University of Edinburgh, Edinburgh (2002) |
| [8] | Dennis, L.A., Smaill, A.: Ordinal arithmetic: a case study for rippling in a higher order domain. In: Boulton, R.J., Jackson, P.B. (eds.) Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001. Lecture Notes in Computer Science, vol. 2152, pp. 185–200. Springer, Berlin (2001) · Zbl 1005.68540 |
| [9] | Dixon, L., Fleuriot, J.D.: Higher order rippling in IsaPlanner. In: Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 3223, pp. 83–98 (2004) · Zbl 1099.68723 |
| [10] | Felty, A.: A logic programming approach to implementing higher-order term rewriting. In: Eriksson, L.-H., et al. (eds.) Second International Workshop on Extensions to Logic Programming. Lecture Notes in Computer Science, vol. 596, pp. 135–61. Springer, Berlin (1992) |
| [11] | Gallagher, J.K.: The use of proof plans in tactic synthesis. Ph.D. thesis, University of Edinburgh (1993) |
| [12] | Gardent, C., Kohlhase, M.: Higher-order coloured unification and natural language semantics. In: Joshi, A., Palmer, M. (eds.) Proceedings of the Thirty-Fourth Annual Meeting of the Association for Computational Linguistics, pp. 1–9. Morgan Kaufmann, San Francisco (1996) |
| [13] | Hutter, D.: Guiding inductive proofs. In: Stickel, M.E. (ed.) 10th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 449, pp. 147–161. Springer, Berlin (1990) |
| [14] | Hutter, D.: Pattern-direct guidance of equational proofs. Ph.D. thesis, University of Karlsruhe (1991) |
| [15] | Hutter, D.: Using rippling for equational reasoning. In: Hölldobler, S. (ed.) Proceedings 20th German Annual Conference on Artificial Intelligence KI-96. Lecture Notes in Artificial Intelligence, vol. 1137. Springer, Berlin (1996) |
| [16] | Hutter, D., Kohlhase, M.: Managing structural information by higher-order colored unification. J. Autom. Reason. 25(2), 123–164 (2000) · Zbl 0959.03007 · doi:10.1023/A:1006282725324 |
| [17] | Ireland, A., Bundy, A.: Productive use of failure in inductive proof. J. Autom. Reason. 16(1–2), 79–111 (1996, Also available from Edinburgh as DAI Research Paper No. 716) · Zbl 0847.68103 · doi:10.1007/BF00244460 |
| [18] | Jouannaud, J.-P., Okada, M.: Satisfiability of systems of ordinal notations with the subterm property is decidable. In: Proceedings of the Eighteenth EATCS Colloquium on Automata, Languages and Programming. Madrid, Spain (1991) · Zbl 0789.68125 |
| [19] | Klop, J.W.: Term rewriting systems. In: Abramsky, S., Gabbay, D., Maibaum, T.S. (eds.) Handbook of Logic in Computer Science, vol. 2, pp. 1–116. Clarendon, Oxford (1992) |
| [20] | Lacey, D., Richardson, J., Smaill, A.: Logic program synthesis in a higher-order setting. In: Lloyd, J., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Palamidessi, C., Pereira, L.M., Sagiv, Y., Stuckey, P.J. (eds.) Computational Logic–CL2000. Lecture Notes in Computer Science, vol. 1861. Springer, Berlin (2000) · Zbl 0983.68502 |
| [21] | Liang, C.: {\(\lambda\)}Prolog implementation of ripple-rewriting. In: Proceedings of the 1992 Workshop on the {\(\lambda\)}Prolog Programming Language. University of Pennsylvania, Philadelphia (1992) |
| [22] | Luo, Z., Pollack, R.: LEGO Proof Development System: User’s Manual. Report ECS-LFCS-92-211, Department of Computer Science, University of Edinburgh, Edinburgh (1992) |
| [23] | Miller, D.: Abstract syntax for variable binders: an overview. In: Lloyd, J., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Palamidessi, C., Pereira, L.M., Sagiv, Y., Stuckey, P.J. (eds.) Computation Logic (CL’2000). Lecture Notes in Computer Science, vol. 1861. Springer, Berlin (2000) |
| [24] | Negrete, S., Smaill, A.: Guiding proof search in logical frameworks with rippling. Technical Report, Dept. of Artificial Intelligence, University of Edinburgh, Edinburgh (1995) |
| [25] | Paulson, L.: Isabelle: A Generic Theorem Prover. Lecture Notes in Computer Science, vol. 823. Springer, Berlin (1994) · Zbl 0825.68059 |
| [26] | Richardson, J., Smaill, A., Green, I.: System description: proof planning in higher-order logic with Lambda-Clam. In: Kirchner, C., Kirchner, H. (eds.) Conference on Automated Deduction (CADE’98). Lecture Notes in Computer Science, vol. 1421, pp. 129–133. Springer, Berlin (1998) |
| [27] | Smaill, A., Green, I.: Automating the Synthesis of Functional Programs. Research paper 777, Dept. of Artificial Intelligence, University of Edinburgh, Edinburgh (1995) |
| [28] | Smaill, A., Green, I.: Higher-order annotated terms for proof search. In: von Wright, J., Grundy, J., Harrison, J. (eds.) Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs’96. Lecture Notes in Computer Science, vol. 1275, pp. 399–414. Springer, Berlin (1996, Also available as DAI Research Paper 799) |
| [29] | Walsh, T., Nunes, A., Bundy, A.: The use of proof plans to sum series. In: Kapur, D. (ed.) CADE11. Lecture Notes in Computer Science, vol. 607, pp. 325–339. Springer, Berlin (1992) · Zbl 0925.03072 |
| [30] | Yoshida, T., Bundy, A., Green, I., Walsh, T., Basin, D.: Coloured rippling: an extension of a theorem proving heuristic. In: Cohn, A.G. (ed.) Proceedings of ECAI-94, pp. 85–89. Wiley, New York (1994) |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
