×

zbMATH — the first resource for mathematics

Cut-elimination for quantified conditional logic. (English) Zbl 1417.03282
Summary: A semantic embedding of quantified conditional logic in classical higher-order logic is utilized for reducing cut-elimination in the former logic to existing results for the latter logic. The presented embedding approach is adaptable to a wide range of other logics, for many of which cut-elimination is still open. However, special attention has to be payed to cut-simulation, which may render cut-elimination as a pointless criterion.

MSC:
03F05 Cut-elimination and normal-form theorems
03B15 Higher-order logic; type theory (MSC2010)
03B60 Other nonclassical logic
Software:
GitHub; HOL; LEO-II; Satallax; TPTP
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Andrews, P. (2014). Church’s type theory. In Zalta, E.N. (Ed.) The Stanford Encyclopedia of Philosophy, Spring 2014 edn.: Stanford University.
[2] Andrews, PB, Resolution in type theory, Journal of Symbolic Logic, 36, 414-432, (1971) · Zbl 0231.02038
[3] Andrews, PB, General models and extensionality, Journal of Symbolic Logic, 37, 395-397, (1972) · Zbl 0264.02050
[4] Andrews, PB, General models, descriptions, and choice in type theory, Journal of Symbolic Logic, 37, 385-394, (1972) · Zbl 0264.02049
[5] Backes, J; Brown, CE, Analytic tableaux for higher-order logic with choice, Journal of Automated Reasoning, 47, 451-479, (2011) · Zbl 1258.03019
[6] Benzmüller, C. (1999). Equality and extensionality in automated higher-order theorem proving. Ph.D. thesis, Saarland University.
[7] Benzmüller, C. (1999). Extensional higher-order paramodulation and RUE-resolution. In Ganzinger, H. (Ed.) Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, no. 1632 in LNCS, pp. 399-413. : Springer. doi:10.1007/3-540-48660-7_39 · Zbl 1185.68636
[8] Benzmüller, C. (2009). Automating access control logic in simple type theory with LEO-II. In Gritzalis, D., & López, J. (Eds.) Emerging Challenges for Security, Privacy and Trust, 24th IFIP TC 11 International Information Security Conference, SEC 2009, Pafos, Cyprus, May 18-20, 2009. Proceedings, IFIP, vol. 297, pp. 387-398. doi:10.1007/978-3-642-01244-0_34: Springer. · Zbl 1211.68371
[9] Benzmüller, C, Combining and automating classical and non-classical logics in classical higher-order logic, Annals of Mathematics and Artificial Intelligence (Special issue Computational logics in Multi-agent Systems (CLIMA XI)), 62, 103-128, (2011) · Zbl 1252.03025
[10] Benzmüller, C. (2013). Automating quantified conditional logics in HOL. In Rossi, F. (Ed.) 23rd International Joint Conference on Artificial Intelligence (IJCAI-13), pp. 746-753, Beijing, China. · Zbl 0930.03080
[11] Benzmüller, C. (2013). Cut-free calculi for challenge logics in a lazy way. In Clint van Alten Petr Cintula, C.N. (Ed.) Proceedings of the International Workshop on Algebraic Logic in Computer Science. · Zbl 0231.02038
[12] Benzmüller, C. (2013). A top-down approach to combining logics. In Proc. of the 5th International Conference on Agents and Artificial Intelligence (ICAART), pp. 346-351. SciTePress Digital Library, Barcelona, Spain. doi:10.5220/0004324803460351.
[13] Benzmüller, C. (2015). Higher-order automated theorem provers. In Delahaye, D., & Woltzenlogel Paleo, B. (Eds.) All about Proofs, Proofs for All, Mathematical Logic and Foundations, pp. 171-214, College Publications. · JFM 57.0054.02
[14] Benzmüller, C; Brown, C; Kohlhase, M, Higher-order semantics and extensionality, Journal of Symbolic Logic, 69, 1027-1088, (2004) · Zbl 1071.03024
[15] Benzmüller, C., Brown, C., & Kohlhase, M. (2008). Cut elimination with xi-functionality. In Benzmüller, C., Brown, c., Siekmann, J., & Statman, R. (Eds.) Reasoning in Simple Type Theory — Festschrift in Honor of Peter B. Andrews on His 70th Birthday, Studies in Logic, Mathematical Logic and Foundations, pp. 84-100. College Publications. · Zbl 0039.00801
[16] Benzmüller, C; Brown, C; Kohlhase, M, Cut-simulation and impredicativity, Logical Methods in Computer Science, 5, 1-21, (2009) · Zbl 1160.03004
[17] Benzmüller, C; Gabbay, D; Genovese, V; Rispoli, D, Embedding and automating conditional logics in classical higher-order logic, Annals of Mathematics and Artificial Intelligence, 66, 257-271, (2012) · Zbl 1272.03064
[18] Benzmüller, C., & Genovese, V. Quantified conditional logics are fragments of HOL. In The International Conference on Non-classical Modal and Predicate Logics (NCMPL). Guangzhou (Canton), China (2011). The conference had no published proceedings; the paper is available as. arXiv:1204.5920v1. · Zbl 1365.68164
[19] Benzmüller, C., & Paulson, L. (2008). Exploring properties of normal multimodal logics in simple type theory with LEO-II. In Benzmüller, C., Brown, C., Siekmann, J., & Statman, R. (Eds.) Reasoning in Simple Type Theory — Festschrift in Honor of Peter B. Andrews on His 70th Birthday, Studies in Logic, Mathematical Logic and Foundations, pp. 386-406. College Publications. · Zbl 1227.03017
[20] Benzmüller, C., & Miller, D. (2014). Automation of Higher-Order Logic. Chapter. In Gabbay, D.M., Siekmann, J.H., & Woods, J. (Eds.) Handbook of the History of Logic, Volume 9 — Computational Logic, North Holland, Elsevier, pp. 215-254.
[21] Benzmüller, C; Paulson, L, Multimodal and intuitionistic logics in simple type theory, The Logic Journal of the IGPL, 18, 881-892, (2010) · Zbl 1222.03023
[22] Benzmüller, C; Paulson, L, Quantified multimodal logics in simple type theory, Logica Universalis (Special Issue on Multimodal Logics), 7, 7-20, (2013) · Zbl 1334.03014
[23] Benzmüller, C; Paulson, LC; Sultana, N; Theiß, F, The higher-order prover LEO-II, Journal of Automated Reasoning, 55, 389-404, (2015) · Zbl 1356.68176
[24] Benzmüller, C., & Sultana, N. (2013). LEO-II Version 1.5. In Blanchette , J.C., & Urban, J. (Eds.) PxTP 2013, EPiC Series, vol. 14, pp. 2-10. EasyChair. · Zbl 1365.68404
[25] Benzmüller, C., & Woltzenlogel Paleo, B. (2014). Automating Gödel’s ontological proof of God’s existence with higher-order automated theorem provers. In Schaub, T., Friedrich, G., & O’Sullivan, B. (Eds.) ECAI 2014, Frontiers in Artificial Intelligence and Applications, vol. 263, pp. 93-98. IOS Press. doi:10.3233/978-1-61499-419-0-93. · JFM 66.1192.06
[26] Brown, C.E. (2004). Set comprehension in church’s type theory. Ph.D. thesis, Department of Mathematical Sciences Carnegie Mellon University. See also Chad E. Brown (2007), Automated Reasoning in Higher-Order Logic, College Publications. · Zbl 0317.02029
[27] Brown, C.E. (2005). Reasoning in extensional type theory with equality. In Nieuwenhuis, R. (Ed.) Proc. of CADE-20, LNCS, vol. 3632, pp. 23-37. Springer. · Zbl 1135.68551
[28] Brown, C.E. (2012). Satallax: An automatic higher-order prover. In Gramlich, B., Miller, D., & Sattler, U. (Eds.) Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, LNCS, vol. 7364, pp. 111-117. Springer. doi:10.1007/978-3-642-31365-3_11. · Zbl 1358.68250
[29] Brown, C.E., & Smolka, G. (2010). Analytic tableaux for simple type theory and its first-order fragment. Logical Methods in Computer Science, \(6\)(2). · Zbl 1198.03022
[30] Chellas, B, Basic conditional logic, Journal of Philosophical Logic, 4, 133-153, (1975) · Zbl 0317.02029
[31] Chellas, B. (1980). Modal logic: an introduction. Cambridge: Cambridge University Press. · Zbl 0431.03009
[32] Church, A, A set of postulates for the foundation of logic, Annals of Mathematics, 33, 346-366, (1932) · JFM 59.0052.01
[33] Church, A, An unsolvable problem of elementary number theory, American Journal of Mathematics, 58, 354-363, (1936) · Zbl 0014.09802
[34] Church, A, A formulation of the simple theory of types, Journal of Symbolic Logic, 5, 56-68, (1940) · JFM 66.1192.06
[35] Chwistek, L. (1948). The limits of science: Outline of logic and of the methodology of the exact sciences. London: Routledge and Kegan Paul.
[36] Delgrande, J, A first-order conditional logic for prototypical properties, Artificial Intelligence, 33, 105-130, (1987) · Zbl 0654.68106
[37] Delgrande, J, On first-order conditional logics, Artificial Intelligence, 105, 105-137, (1998) · Zbl 0909.68174
[38] Fitting, M, Interpolation for first order S5, Journal of Symbolic Logic, 67, 621-634, (2002) · Zbl 1009.03013
[39] Frege, G. Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle (1879). Translated in [43]. · Zbl 1116.03008
[40] Friedman, N; Halpern, J; Koller, D, First-order conditional logic for default reasoning revisited, ACM Transactions on Computational Logic, 1, 175-207, (2000) · Zbl 1365.68404
[41] Girard, J.Y. (1971). Une extension de l’interpretation de Gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types. In Fenstad, J.E. (Ed.) 2nd scandinavian logic symposium, pp. 63-92, North-Holland, Amsterdam. · Zbl 1160.03004
[42] Gödel, K, Über formal unentscheidbare Sätze der principia Mathematica und verwandter systeme I, Monatshefte der Mathematischen Physik, 38, 173-198, (1931) · JFM 57.0054.02
[43] van Heijenoort, J. (1967). From Frege to Gödel: A source Book in Mathematics, 1879-1931, 3rd printing, 1997 edn. Source books in the history of the sciences series. Harvard University Press, Cambridge, MA. · Zbl 1071.03024
[44] Henkin, L, Completeness in the theory of types, Journal of Symbolic Logic, 15, 81-91, (1950) · Zbl 0039.00801
[45] Huet, G.P. (1972). Constrained resolution: a complete method for higher order logic. Ph.D. thesis, Case Western Reserve University. · Zbl 1009.03013
[46] Huet, G.P. (1973). A mechanization of type theory. In Proceedings of the 3rd International Joint Conference on Artificial Intelligence, pp. 139-146. · Zbl 0199.00801
[47] Kohlhase, M. (1994). A mechanization of sorted higher-order logic based on the resolution principle. Ph.D. thesis, Saarland University.
[48] McDowell, R; Miller, D, Reasoning with higher-order abstract syntax in a logical framework, ACM Transactions on Computational Logic, 3, 80-136, (2002) · Zbl 1365.68164
[49] Mints, G, Cut-elimination for simple type theory with an axiom of choice, Journal of Symbolic Logic, 64, 479-485, (1999) · Zbl 0930.03080
[50] Muskens, R, Intensional models for the theory of types, Journal of Symbolic Logic, 72, 98-118, (2007) · Zbl 1116.03008
[51] Nute, D. (1980). Topics in conditional logic. Dordrecht: Reidel. · Zbl 0453.03016
[52] Olivetti, N., Pozzato, G., & Schwind, C. (2007). A sequent calculus and a theorem prover for standard conditional logics. ACM Transactions on Computational Logic, \(8\)(4). · Zbl 1367.68253
[53] Paleo, B.W. (2014). An embedding of neighbourhood-based modal logics in hol. Unpublished draft; available at https://github.com/Paradoxika/ModalLogic.
[54] Pattinson, D., & Schröder, L. (2011). Generic modal cut elimination applied to conditional logics. Logical Methods in Computer Science, \(7\)(1). doi:10.2168/LMCS-7(1:4)2011. · Zbl 0075.23404
[55] Prawitz, D, Hauptsatz for higher order logic, Journal of Symbolic Logic, 33, 452-457, (1968) · Zbl 0164.31002
[56] Ramsey, F.P. (1926). The foundations of mathematics. In Proceedings of the London Mathematical Society, 2, vol. 25, pp. 338-384. · JFM 52.0046.01
[57] Rasga, J, Sufficient conditions for cut elimination with complexity analysis, Annals of Pure and Applied Logic, 149, 81-99, (2007) · Zbl 1145.03033
[58] Russell, B, Mathematical logic as based on the theory of types, American Journal of Mathematics, 30, 222-262, (1908) · JFM 39.0085.03
[59] Schütte, K, Semantical and syntactical properties of simple type theory, Journal of Symbolic Logic, 25, 305-326, (1960) · Zbl 0109.00511
[60] Smullyan, RM, A unifying principle for quantification theory, Proc Nat Acad Sciences, 49, 828-832, (1963) · Zbl 0118.24901
[61] Stalnaker, R. (1968). A theory of conditionals. In Studies in Logical Theory , pp. 98-112. Blackwell.
[62] Sutcliffe, G, The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0, Journal of Automated Reasoning, 43, 337-362, (2009) · Zbl 1185.68636
[63] Sutcliffe, G; Benzmüller, C, Automated reasoning in higher-order logic using the TPTP THF infrastructure, Journal of Formalized Reasoning, 73, 1-27, (2010) · Zbl 1211.68371
[64] Tait, WW, A nonconstructive proof of gentzen’s hauptsatz for second order predicate logic, Bulletin of the American Mathematical Society, 72, 980-983, (1966) · Zbl 0199.00801
[65] Takahashi, M, A proof of cut-elimination theorem in simple type theory, Journal of the Mathematical Society of Japan, 19, 399-410, (1967) · Zbl 0206.27503
[66] Takeuti, G, On a generalized logic calculus. Japanese, Journal of Mathematics 23, 39-96 (1953). Errata: ibid, 24, 149-156, (1954) · Zbl 0053.20301
[67] Takeuti, G, An example on the fundamental conjecture of GLC, Journal of the Mathematical Society of Japan, 12, 238-242, (1960) · Zbl 0075.23404
[68] Takeuti, G. (1975). Proof Theory, Studies in Logic and the Foundations of Mathematics, vol. 81. Elsevier. · Zbl 0355.02023
[69] Wisniewski, M., & Steen, A. (2015). Embedding of First-Order Nominal Logic into Higher-Order Logic. In Beziau, J. Y. et al. Handbook of the 5th world congress and school on universal logic (UNILOG’15), Istanbul, Turkey (pp. 337-339). · Zbl 1356.68176
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.