Abstract
Interactive provers typically use higher-order logic, while automatic provers typically use first-order logic. To integrate interactive provers with automatic ones, one must translate higher-order formulas to first-order form. The translation should ideally be both sound and practical. We have investigated several methods of translating function applications, types, and λ-abstractions. Omitting some type information improves the success rate but can be unsound, so the interactive prover must verify the proofs. This paper presents experimental data that compares the translations in respect of their success rates for three automatic provers.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Beeson, M.: Mathematical induction in Otter-lambda. J. Autom. Reason. 36(4), 311–344 (2006)
Benzmüller, C., Sorge, V., Jamnik, M., Kerber, M.: Can a higher-order and a first-order theorem prover cooperate? In: Baader, F., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning – 11th International Workshop, LPAR 2004, LNAI, vol. 3452, pp. 415–431. Springer (2005)
Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., Rinard, M.: Using first-order theorem provers in the Jahob data structure verification system. In: Cook, B., Podelski, A. (eds.) Verification, Model Checking, and Abstract Interpretation, LNCS, vol. 4349, pp. 74–88. Springer (2007)
Gordon, M.J.C., Melham, T.F.: Introduction to HOL: a Theorem Proving Environment for Higher Order Logic. Cambridge Univ. Press (1993)
Hughes, R.J.M.: Supercombinators: a new implementation method for applicative languages. In: LISP and Func. Prog. ACM Press (1982)
Hurd, J.: An LCF-style interface between HOL and first-order logic. In: Voronkov, A. (ed.) Automated Deduction – CADE-18 International Conference, LNAI, vol. 2392, pp. 134–138. Springer (2002)
Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Vito, B.D., Muñoz, C. (eds.) Design and Application of Strategies/Tactics in Higher Order Logics, Number NASA/CP-2003-212448 in NASA Technical Reports, pp. 56–68, September (2003)
Kennaway, R., Sleep, R.: Director strings as combinators. ACM Trans. Program. Lang. Syst. 10(4), 602–626 (1988)
Meng, J., Paulson, L.C.: Translating higher-order problems to first-order clauses. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) FLoC’06 Workshop on Empirically Successful Computerized Reasoning, CEUR Workshop Proceedings, vol. 192, pp. 70–80 (2006)
Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. Journal of Applied Logic (2007) (in press)
Meng, J., Quigley, C., Paulson, L.C.: Automation for interactive proof: first prototype. Inf. Comput. 204(10), 1575–1596 (2006)
Miller, D.: Unification under a mixed prefix. J. Symb. Comput. 14(4), 321–358 (1992)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a Proof Assistant for Higher-Order Logic. LNCS Tutorial, vol. 2283. Springer (2002)
Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.K.: PVS: Combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) Computer Aided Verification: 8th International Conference, CAV ’96, LNCS, vol. 1102, pp. 411–414. Springer (1996)
Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Klaus, S., Brandt, J. (eds.) Theorem Proving in Higher Order Logics, LNCS, vol. 4732, pp. 232–245. Springer (2007)
Peyton Jones, S.L.: The Implementation of Functional Programming Languages. Prentice Hall (1987)
Pierce, B.C.: Types and Programming Languages. MIT Press (2002)
Riazanov, A., Voronkov, A.: Vampire 1.1 (system description). In: Goré, R., Leitsch, A., Nipkow, T. (eds.) Automated Reasoning – First International Joint Conference, IJCAR 2001, LNAI, vol. 2083, pp. 376–380. Springer (2001)
Schulz, S.: System description: E 0.81. In: Basin, D., Rusinowitch, M. (eds.) Automated Reasoning – Second International Joint Conference, IJCAR 2004, LNAI, vol. 3097, pp. 223–228. Springer (2004)
Sutcliffe, G., Suttner, C.: The TPTP problem library for automated theorem proving. On the internet at http://www.cs.miami.edu/~tptp/ (2004)
Sutcliffe, G., Zimmer, J., Schulz, S.: TSTP data-exchange formats for automated theorem proving tools. In: Zhang, W., Sorge, V. (eds.) Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, Number 112 in Frontiers in Artificial Intelligence and Applications, pp. 201–215. IOS Press (2004)
Turner, D.A.: Another algorithm for bracket abstraction. J. Symb. Log. 44(2), 267–270, June 1979
Turner, D.A.: A new implementation technique for applicative languages. Softw. Pract. Exp. 9, 31–49 (1979)
Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. II, chapter 27, pp. 1965–2013. Elsevier Science (2001)
Zimmer, J., Meier, A., Sutcliffe, G., Zhang, Y.: Integrated proof transformation services. In: Benzmüller, C., Windsteiger, W. (eds.) Workshop on Computer-Supported Mathematical Theory Development, 2nd International Joint Conference on Automated Reasoning, Electronic Notes in Theoretical Computer Science (2004)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Meng, J., Paulson, L.C. Translating Higher-Order Clauses to First-Order Clauses. J Autom Reasoning 40, 35–60 (2008). https://doi.org/10.1007/s10817-007-9085-y
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-007-9085-y