Translating Higher-Order Clauses to First-Order Clauses - Journal of Automated Reasoning
- ️Paulson, Lawrence C.
- ️Sat Sep 15 2007
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)