Abstract
While many higher-order interactive theorem provers include a choice operator, higher-order automated theorem provers so far have not. In order to support automated reasoning in the presence of a choice operator, we present a cut-free ground tableau calculus for Church’s simple type theory with choice. The tableau calculus is designed with automated search in mind. In particular, the rules only operate on the top level structure of formulas. Additionally, we restrict the instantiation terms for quantifiers to a universe that depends on the current branch. At base types the universe of instantiations is finite. Both of these restrictions are intended to minimize the number of rules a corresponding search procedure is obligated to consider. We prove completeness of the tableau calculus relative to Henkin models.
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
Altenkirch, T., Uustalu, T.: Normalization by evaluation for λ →2. In: Kameyama, Y., Stuckey, P.J. (eds.) Functional and Logic Programming, 7th International Symposium, FLOPS 2004, Proceedings. LNCS, vol. 2998, pp. 260–275. Springer (2004)
Andrews, P.B.: Resolution in type theory. J. Symb. Log. 36, 414–432 (1971)
Andrews, P.B.: General models and extensionality. J. Symb. Log. 37, 395–397 (1972)
Andrews, P.B., Brown, C.E.: TPS: a hybrid automatic-interactive system for developing proofs. J. Appl. Logic 4(4), 367–395 (2006)
Backes, J.: Tableaux for higher-order logic with if-then-else, description and choice. Master’s thesis, Universität des Saarlandes (2010)
Backes, J., Brown, C.E.: Analytic tableaux for higher-order logic with choice. In: Giesl, J., Hähnle, R. (eds.) Automated Reasoning: 5th International Joint Conference, IJCAR 2010, Proceedings. LNCS/LNAI, vol. 6173, pp. 76–90. Springer (2010)
Beeson, M.: Unification in lambda-calculi with if-then-else. In: Kirchner, C., Kirchner, H. (eds.) Proceedings of the 15th International Conference on Automated Deduction. LNAI, vol. 1421, pp. 103–118. Springer, Lindau, Germany (1998)
Benzmueller, C., Brown, C.E., Kohlhase, M.: Cut-simulation and impredicativity. LMCS 5(1:6), 1–21 (2009)
Benzmüller, C., Brown, C.E., Kohlhase, M.: Higher-order semantics and extensionality. J. Symb. Log. 69, 1027–1088 (2004)
Benzmüller, C., Theiss, F., Paulson, L., Fietzke, A.: LEO-II — a cooperative automatic theorem prover for higher-order logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Fourth International Joint Conference on Automated Reasoning, IJCAR’08. LNAI, vol. 5195. Springer (2008)
Brown, C.E.: Automated Reasoning in Higher-Order Logic: Set Comprehension and Extensionality in Church’s Type Theory. College Publications (2007)
Brown, C.E., Smolka, G.: Extended first-order logic. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Proceedings. LNCS, vol. 5674, pp. 164–179. Springer (2009)
Brown, C.E., Smolka, G.: Terminating tableaux for the basic fragment of simple type theory. In: Giese, M., Waaler, A. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods: 18th International Conference, TABLEAUX 2009, Proceedings. LNCS/LNAI, vol. 5607, pp. 138–151. Springer (2009)
Brown, C.E., Smolka, G.: Analytic tableaux for simple type theory and its first-order fragment. LMCS 6(2), 1–33 (2010)
Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5, 56–68 (1940)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) Theory and Applications of Satisfiability Testing, LNCS, vol. 2919, pp. 333–336. Springer, Berlin/Heidelberg (2004)
Gordon, M., Melham, T.: Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic. Cambridge University Press (1993)
Harrison, J.: HOL light: a tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD’96), LNCS, vol. 1166, pp. 265–269. Springer (1996)
Henkin, L.: Completeness in the theory of types. J. Symb. Log. 15, 81–91 (1950)
Hintikka, K.J.J.: Form and content in quantification theory. Two papers on symbolic logic. Acta Philos. Fenn. 8, 7–55 (1955)
Huet, G.P.: Constrained resolution: a complete method for higher order logic. PhD thesis, Case Western Reserve University (1972)
King, D.J., Arthan, R.D.: Development of practical verification tools. ICL Systems J. 11(1) (1996)
Miller, D.A.: A compact representation of proofs. Stud. Log. 46(4), 347–370 (1987)
Mints, G.: Cut-elimination for simple type theory with an axiom of choice. J. Symb. Log. 64(2), 479–485 (1999)
Mitchell, J.C., Hoang, M., Howard, B.T.: Labeling techniques and typed fixed-point operators. In: Higher Order Operational Techniques in Semantics, pp. 137–174. Cambridge University Press, New York (1998)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — a proof assistant for higher-order logic. LNCS, vol. 2283. Springer (2002)
Prawitz, D.: Hauptsatz for higher order logic. J. Symb. Log. 33, 452–457 (1968)
Slind, K., Norrish, M.: A brief overview of HOL4. In: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics. LNCS, vol. 5170, pp. 28–32. Springer, Berlin, Heidelberg (2008)
Smullyan, R.M.: A unifying principle in quantification theory. Proc. Natl. Acad. Sci. U.S.A. 49, 828–832 (1963)
Smullyan, R.M.: First-Order Logic. Springer (1968)
Sutcliffe, G.: The 5th IJCAR automated theorem proving system competition - CASC-J5. AI Commun. 24(1), 75–89 (2011)
Sutcliffe, G., Benzmüller, C., Brown, C.E., Theiss, F.: Progress in the development of automated theorem proving for higher-order logic. In: Schmidt, R.A. (ed.) Automated Deduction - CADE-22. 22nd International Conference on Automated Deduction, Proceedings. LNCS, vol. 5663, pp. 116–130. Springer (2009)
Takahashi, M.: Simple type theory of gentzen style with the inference of extensionality. Proc. Jpn. Acad. 44(2), 43–45 (1968)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Backes, J., Brown, C.E. Analytic Tableaux for Higher-Order Logic with Choice. J Autom Reasoning 47, 451–479 (2011). https://doi.org/10.1007/s10817-011-9233-2
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-011-9233-2