Linked bibliography for the SEP article "Church’s Type Theory" by Christoph Benzmüller and Peter Andrews

This is an automatically generated and experimental page

If everything goes well, this page should display the bibliography of the aforementioned article as it appears in the Stanford Encyclopedia of Philosophy, but with links added to PhilPapers records and Google Scholar for your convenience. Some bibliographies are not going to be represented correctly or fully up to date. In general, bibliographies of recent works are going to be much better linked than bibliographies of primary literature and older works. Entries with PhilPapers records have links on their titles. A green link indicates that the item is available online at least partially.

This experiment has been authorized by the editors of the Stanford Encyclopedia of Philosophy. The original article and bibliography can be found here.

Andrews, Peter B., 1963, “A Reduction of the Axioms for the Theory of Prepositional Types”, Fundamenta Mathematicae, 52(3): 345–350. doi:10.4064/fm-52-3-345-350 (Scholar)
–––, 1971, “Resolution in Type Theory”, The Journal of Symbolic Logic, 36(3): 414–432. Reprinted in Siekmann & Wrightson 1983 and in Benzmüller et al. 2008. doi:10.2307/2269949 doi:10.1007/978-3-642-81955-1 (Scholar)
–––, 1972a, “General Models and Extensionality”, The Journal of Symbolic Logic, 37(2): 395–397. Reprinted in Benzmüller et al. 2008. doi:10.2307/2272982 (Scholar)
–––, 1972b, “General Models, Descriptions, and Choice in Type Theory”, The Journal of Symbolic Logic, 37(2): 385–394. Reprinted in Benzmüller et al. 2008. doi:10.2307/2272981 (Scholar)
–––, 1974, “Provability in Elementary Type Theory”, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 20(25–27): 411–418. doi:10.1002/malq.19740202506 (Scholar)
–––, 1981, “Theorem Proving via General Mappings”, Journal of the ACM, 28(2): 193–214. doi:10.1145/322248.322249 (Scholar)
–––, 2001, “Classical Type Theory”, in Robinson and Voronkov 2001, Volume 2, Chapter 15, pp. 965–1007. doi:10.1016/b978-044450813-3/50017-5 (Scholar)
–––, 2002, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, (Applied Logic Series 27), second edition, Dordrecht: Springer Netherlands. doi:10.1007/978-94-015-9934-4 (Scholar)
Andrews, Peter B., Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, and Hongwei Xi, 1996, “TPS: A Theorem-Proving System for Classical Type Theory”, Journal of Automated Reasoning, 16(3): 321–353. Reprinted in Benzmüller et al. 2008. doi:10.1007/BF00252180 (Scholar)
Andrews, Peter B. and Chad E. Brown, 2006, “TPS: A Hybrid Automatic-Interactive System for Developing Proofs”, Journal of Applied Logic, 4(4): 367–395. doi:10.1016/j.jal.2005.10.002 (Scholar)
Baader, Franz and Wayne Snyder, 2001, “Unification Theory”, in Robinson and Voronkov 2001, Volume 1, Chapter 8, Amsterdam: Elsevier Science, pp. 445–533. doi:10.1016/b978-044450813-3/50010-2 (Scholar)
Backes, Julian and Chad Edward Brown, 2011, “Analytic Tableaux for Higher-Order Logic with Choice”, Journal of Automated Reasoning, 47(4): 451–479. doi:10.1007/s10817-011-9233-2 (Scholar)
Barbosa, Haniel, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, and Clark Barret, 2019, “Extending SMT Solvers to Higher-Order Logic”, in Automated Deduction – CADE 27, Pascal Fontaine (ed.), (Lecture Notes in Computer Science 11716), Cham: Springer Nature Switzerland AG. doi:10.1007/978-3-030-29436-6_3 (Scholar)
Barendregt, H. P., 1984, The Lambda Calculus: Its Syntax and Semantics, (Studies in Logic and the Foundations of Mathematics, 103), revised edition, Amsterdam: North-Holland. (Scholar)
Barendregt, Henk, Wil Dekkers, and Richard Statman, 2013, Lambda Calculus with Types, Cambridge: Cambridge University Press. doi:10.1017/cbo9781139032636 (Scholar)
Bayer, Jonas, Christoph Benzmüller, Kevin Buzzard, Marco David, Leslie Lamport, Yuri Matiyasevich, Lawrence Paulson, Dierk Schleicher, Benedikt Stock, and Efim Zelmanov, 2024, “Mathematical Proof Between Generations”, Notices of the AMS, 71(1):80-92. doi:10.1090/noti2860 (Scholar)
Bentkamp, Alexander, Jasmin Blanchette, Simon Cruanes, and Uwe Waldmann, 2018, “Superposition for Lambda-Free Higher-Order Logic”, in Galmiche et al. 2018: 28–46. doi:10.1007/978-3-319-94205-6_3">10.1007/978-3-319-94205-6_3 (Scholar)
Bentkamp, Alexander, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, and Uwe Waldmann, 2023a, “Complete and Efficient Higher-Order Reasoning via Lambda-Superposition”. ACM SIGLOG News 10(4):25–40. doi:10.1145/3636362.3636367">10.1145/3636362.3636367 (Scholar)
Bentkamp, Alexander, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Petar Vukmirovic, and Uwe Waldmann, 2023b, “Mechanical Mathematicians” Communications of the ACM, 66(4):80–90. doi:10.1145/3636362.3636367 (Scholar)
Bentkamp, Alexander, Jasmin Blanchette, Sophie Tourret, and Petar Vukmirovic, 2023c, “Superposition for Higher-Order Logic”, Journal of Automated Reasoning, 67(1):10. doi:10.1007/s10817-022-09649-9 (Scholar)
Bentkamp, Alexander, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, and Uwe Waldmann, 2021, “Superposition with Lambdas”,Journal of Automated Reasoning, 65, 893–940. doi:10.1007/s10817-021-09595-y (Scholar)
Benzmüller, Christoph, 1997, A Calculus and a System Architecture for Extensional Higher-Order Resolution, Technical report 97–198, Department of Mathematical Sciences, Carnegie Mellon University. doi:10.1184/r1/6476477.v1 (Scholar)
–––, 1999a, Equality and Extensionality in Automated Higher-Order Theorem Proving, Ph.D. dissertation, Computer Science Department, Universität des Saarlandes. (Scholar)
–––, 1999b, “Extensional Higher-Order Paramodulation and RUE-Resolution”, in Ganzinger 1999: 399–413. doi:10.1007/3-540-48660-7_39">10.1007/3-540-48660-7_39 (Scholar)
–––, 2019, “Universal (Meta-)Logical Reasoning: Recent Successes”, Science of Computer Programming, 172: 48–62. doi:10.1016/j.scico.2018.10.008 (Scholar)
Benzmüller, Christoph and Michael Kohlhase, 1997, “Model Existence for Higher Order Logic”. SEKI Report SR-97-09. (Scholar)
–––, 1998a, “Extensional Higher-Order Resolution”, Kirchner and Kirchner 1998: 56–71. doi:10.1007/bfb0054248 (Scholar)
–––, 1998b, “System Description: Leo—A Higher-Order Theorem Prover”, in Kirchner and Kirchner 1998: 139–143. doi:10.1007/bfb0054256 (Scholar)
Benzmüller, Christoph, Chad E. Brown, and Michael Kohlhase, 2004, “Higher-Order Semantics and Extensionality”, The Journal of Symbolic Logic, 69(4): 1027–1088. doi:10.2178/jsl/1102022211 (Scholar)
–––, 2009, “Cut-Simulation and Impredicativity”, Logical Methods in Computer Science, 5(1): 6. doi:10.2168/lmcs-5(1:6)2009 (Scholar)
Benzmüller, Christoph, Chad E. Brown, Jörg Siekmann, and Richard Statman (eds.), 2008, Reasoning in Simple Type Theory: Festschrift in Honour of Peter B. Andrews on His 70th Birthday, (Studies in Logic 17), London: College Publications. (Scholar)
Benzmüller, Christoph, David Fuenmayor, Alexander Steen, and Geoff Sutcliffe, 2023, “Who Finds the Short Proof?”, Logic Journal of the IGPL. doi:10.1093/jigpal/jzac082 (Scholar)
Benzmüller, Christoph and Dale Miller, 2014, “Automation of Higher Order Logic”, in Computational Logic, (Handbook of the History of Logic, 9), Dov M. Gabbay, Jörg H. Siekmann, and John Woods (eds.), Amsterdam: Elsevier, 215–254. (Scholar)
Benzmüller, Christoph, Xavier Parent, and Leendert van der Torre, 2020, “Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support, Artificial Intelligence, 287:103348. doi:10.1016/j.artint.2020.103348 (Scholar)
Benzmüller, Christoph, Nik Sultana, Lawrence C. Paulson, and Frank Theiß, 2015, “The Higher-Order Prover Leo-II”, Journal of Automated Reasoning, 55(4): 389–404. doi:10.1007/s10817-015-9348-y (Scholar)
Benzmüller, Christoph and Dana S. Scott, 2019, “Automating Free Logic in HOL, with an Experimental Application in Category Theory”, Journal of Automated Reasoning, 64:53–72 (2020). doi:10.1007/s10817-018-09507-7 (Scholar)
Benzmüller, Christoph and Bruno Woltzenlogel Paleo, 2014, “Automating Gödel’s Ontological Proof of God’s Existence with Higher-Order Automated Theorem Provers”, in Proceedings of the Twenty-First European Conference on Artificial Intelligence (ECAI 2014), T. Schaub, G. Friedrich, and B. O’Sullivan (eds.), (Frontiers in Artificial Intelligence 263), Amsterdam: IOS Press, 93–98. doi:10.3233/978-1-61499-419-0-93 (Scholar)
Bertot, Yves and Pierre Castéran, 2004, Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions, (Texts in Theoretical Computer Science An EATCS Series), Berlin, Heidelberg: Springer Berlin Heidelberg. doi:10.1007/978-3-662-07964-5 (Scholar)
Bhayat, Ahmed and Giles Reger, 2020, “A Combinator-Based Superposition Calculus for Higher-Order Logic”, in Automated Reasoning. IJCAR 2020, Nicolas Peltier and Sofronie-Stokkermans (eds.), (Lecture Notes in Computer Science 12166), Cham: Springer Nature Switzerland AG. doi:10.1007/978-3-030-51074-9_16 (Scholar)
Bibel, Wolfgang, 1981, “On Matrices with Connections”, Journal of the ACM, 28(4): 633–645. doi:10.1145/322276.322277 (Scholar)
Bishop, Matthew, 1999, “A Breadth-First Strategy for Mating Search”, in Ganzinger 1999: 359–373. doi:10.1007/3-540-48660-7_32 (Scholar)
Blanchette, Jasmin Christian and Tobias Nipkow, 2010, “Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder”, in Interactive Theorem Proving, Matt Kaufmann and Lawrence C. Paulson (eds.), (Lecture Notes in Computer Science 6172), Berlin, Heidelberg: Springer Berlin Heidelberg, 131–146. doi:10.1007/978-3-642-14052-5_11 (Scholar)
Blanchette, Jasmin Christian, Sascha Böhme, and Lawrence C. Paulson, 2013, “Extending Sledgehammer with SMT Solvers”, Journal of Automated Reasoning, 51(1): 109–128. doi:10.1007/s10817-013-9278-5 (Scholar)
Boolos, George, 1987, “A Curious Inference”, Journal of Philosophical Logic, 16(1): 1–12. doi:10.1007/bf00250612 (Scholar)
Brown, Chad E., 2004, “Set Comprehension in Church’s Type Theory”, PhD Thesis, Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh, PA. (Scholar)
–––, 2007, Automated Reasoning in Higher-Order Logic: Set Comprehension and Extensionality in Church`s Type Theory, (Studies in Logic Logic and Cognitive Systems 10), London: King’s College Publications. (Scholar)
–––, 2012, “Satallax: An Automatic Higher-Order Prover”, in Automated Reasoning (IJCAR 2012), Bernhard Gramlich, Dale Miller, and Uli Sattler (eds.) (Lecture Notes in Computer Science 7364), Berlin, Heidelberg: Springer Berlin Heidelberg, 111–117. doi:10.1007/978-3-642-31365-3_11 (Scholar)
Brown, Chad and Gert Smolka, 2010, “Analytic Tableaux for Simple Type Theory and Its First-Order Fragment”, Logical Methods in Computer Science, 6(2): 3. doi:10.2168/lmcs-6(2:3)2010 (Scholar)
Büchi, J. Richard, 1953, “Investigation of the Equivalence of the Axiom of Choice and Zorn’s Lemma from the Viewpoint of the Hierarchy of Types”, The Journal of Symbolic Logic, 18(2): 125–135. doi:10.2307/2268945 (Scholar)
Church, Alonzo, 1932, “A Set of Postulates for the Foundation of Logic”, The Annals of Mathematics, 33(2): 346–366. doi:10.2307/1968337 (Scholar)
–––, 1940, “A Formulation of the Simple Theory of Types”, The Journal of Symbolic Logic, 5(2): 56–68. Reprinted in Benzmüller et al. 2008. doi:10.2307/2266170 (Scholar)
–––, 1941, The Calculi of Lambda Conversion, (Annals of Mathematics Studies 6), Princeton, NJ: Princeton University Press. (Scholar)
–––, 1956, Introduction to Mathematical Logic, Princeton, NJ: Princeton University Press. (Scholar)
Czajka, Łukasz and Cezary Kaliszyk, 2018, “Hammer for Coq: Automation for Dependent Type Theory”, Journal of Automated Reasoning, 61(1–4): 423–453. doi:10.1007/s10817-018-9458-4 (Scholar)
Díaz, Javier, 2023, “Metatheory of Q0”, Archive of Formal Proofs. https://www.isa-afp.org/entries/Q0_Metatheory.html (Scholar)
Dowek, Gilles, 2001, “Higher-Order Unification and Matching”, in Robinson and Voronkov 2001, Volume 2, Chapter 16, Amsterdam: Elsevier Science, pp. 1009–1062. doi:10.1016/b978-044450813-3/50018-7 (Scholar)
Dowek, Gilles and Benjamin Werner, 2003, “Proof Normalization Modulo”, The Journal of Symbolic Logic, 68(4): 1289–1316. doi:10.2178/jsl/1067620188 (Scholar)
Farmer, William M., 2008, “The Seven Virtues of Simple Type Theory”, Journal of Applied Logic, 6(3): 267–286. doi:10.1016/j.jal.2007.11.001 (Scholar)
Farmer, William M., 2023, “Simple Type Theory - A Practical Logic for Expressing and Reasoning About Mathematical Ideas”, Cham: Birkhäuser. doi:10.1007/978-3-031-21112-6 (Scholar)
Farmer, William M., Joshua D. Guttman, and F. Javier Thayer, 1993, “IMPS: An Interactive Mathematical Proof System”, Journal of Automated Reasoning, 11(2): 213–248. doi:10.1007/bf00881906 (Scholar)
Gallin, Daniel, 1975, Intensional and Higher-Order Modal Logic, Amsterdam: North-Holland. (Scholar)
Galmiche, Didier, Stephan Schulz, and Roberto Sebastiani (eds.), 2018, Automated Reasoning (IJCAR 2018), (Lecture Notes in Computer Science 10900), Cham: Springer International Publishing. doi:10.1007/978-3-319-94205-6 (Scholar)
Ganzinger, Harald (ed.), 1999, Automated Deduction—CADE-16, (Lecture Notes in Computer Science, 1632), Berlin, Heidelberg: Springer Berlin Heidelberg. doi:10.1007/3-540-48660-7 (Scholar)
Gödel, Kurt, 1931, “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I”, Monatshefte für Mathematik und Physik, 38(1): 173–198. Translated in Gödel 1986: 144–195, and in van Heijenoort 1967: 596–616. (Scholar)
–––, 1986, Collected Works, Volume I, Oxford: Oxford University Press. (Scholar)
Goldfarb, Warren D., 1981, “The Undecidability of the Second-Order Unification Problem”, Theoretical Computer Science, 13(2): 225–230. doi:10.1016/0304-3975(81)90040-2 (Scholar)
Gordon, Michael J. C., 1986, “Why Higher-Order Logic is a Good Formalism for Specifying and Verifying Hardware”, in George J. Milne, and P. A. Subrahmanyam (eds.), Formal Aspects of VLSI Design: Proceedings of the 1985 Edinburgh Workshop on VLSI, Amsterdam: North-Holland, pp. 153–177. (Scholar)
–––, 1988, “HOL: A Proof Generating System for Higher-Order Logic”, in VLSI Specification, Verification and Synthesis, Graham Birtwistle and P. A. Subrahmanyam (eds.), (The Kluwer International Series in Engineering and Computer Science 35), Boston, MA: Springer US, 73–128. doi:10.1007/978-1-4613-2007-4_3 (Scholar)
Gordon, M. J., and T. F. Melham, 1993, Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic, Cambridge: Cambridge University Press. (Scholar)
Gould, William Eben, 1966, A Matching Procedure for \(\omega\)-order Logic, Ph.D. dissertation, Mathematics Department, Princeton University. [Gould 1966 available online] (Scholar)
Hales, Thomas, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong Hoang, Cezary Kaliszyk, et al., 2017, “A Formal Proof of the Kepler Conjecture”, Forum of Mathematics, Pi, 5: e2. doi:10.1017/fmp.2017.1 (Scholar)
Harrison, John, 1996, “HOL Light: A Tutorial Introduction”, in Formal Methods in Computer-Aided Design, Mandayam Srivas and Albert Camilleri (eds.), (Lecture Notes in Computer Science 1166), Berlin, Heidelberg: Springer Berlin Heidelberg, 265–269. doi:10.1007/bfb0031814 (Scholar)
Halkjær, Asta, Anders Schlichtkrull, Jørgen Villadsen, 2023, “A sequent calculus for first-order logic formalized in Isabelle/HOL”, Journal of Logic and Computation, 33(4):818-836. doi: 10.1093/logcom/exad013 (Scholar)
Henkin, Leon, 1950, “Completeness in the Theory of Types”, The Journal of Symbolic Logic, 15(2): 81–91. Reprinted in Hintikka 1969 and in Benzmüller et al. 2008. doi:10.2307/2266967 (Scholar)
–––, 1963, “A Theory of Prepositional Types”, Fundamenta Mathematicae, 52(3): 323–344. doi:10.4064/fm-52-3-323-344 (Scholar)
–––, 1975, “Identity as a Logical Primitive”, Philosophia, 5(1–2): 31–45. doi:10.1007/bf02380832 (Scholar)
Hilbert, David, 1928, “Die Grundlagen der Mathematik”, Abhandlungen aus dem mathematischen Seminar der Hamburgischen Universität, 6: 65–85; translated in van Heijenoort 1967: 464–479. (Scholar)
Hintikka, Jaakko (ed.), 1969, The Philosophy of Mathematics, Oxford: Oxford University Press. (Scholar)
Huet, Gerald P., 1973a, “A Mechanization of Type Theory”, in Proceedings of the Third International Joint Conference on Artificial Intelligence (Stanford University), D. E. Walker and L. Norton (eds.), Los Altos, CA: William Kaufman, 139–146. [Huet 1973a available online] (Scholar)
–––, 1973b, “The Undecidability of Unification in Third Order Logic”, Information and Control, 22(3): 257–267. doi:10.1016/s0019-9958(73)90301-x (Scholar)
–––, 1975, “A Unification Algorithm for Typed λ-Calculus”, Theoretical Computer Science, 1(1): 27–57. doi:10.1016/0304-3975(75)90011-0 (Scholar)
Jensen, D.C. and T. Pietrzykowski, 1976, “Mechanizing ω-Order Type Theory through Unification”, Theoretical Computer Science, 3(2): 123–171. doi:10.1016/0304-3975(76)90021-9 (Scholar)
Kaliszyk, Cezary and Josef Urban, 2015, “HOL(y)Hammer: Online ATP Service for HOL Light”, Mathematics in Computer Science, 9(1): 5–22. doi:10.1007/s11786-014-0182-0 (Scholar)
Kirchner, Claude and Hélène Kirchner (eds.), 1998, Automated Deduction—CADE-15, (Lecture Notes in Computer Science, 1421), Berlin, Heidelberg: Springer Berlin Heidelberg. doi:10.1007/bfb0054239 (Scholar)
Klein, Gerwin, June Andronick, Matthew Fernandez, Ihor Kuz, Toby Murray, and Gernot Heiser, 2018, “Formally Verified Software in the Real World”, Communications of the ACM, 61(10): 68–77. doi:10.1145/3230627 (Scholar)
Kohlhase, Michael, 1993, “A Unifying Principle for Extensional Higher-Order Logic”, Technical Report 93–153, Department of Mathematics, Carnegie Mellon University. (Scholar)
–––, 1995, “Higher-Order Tableaux”, in Theorem Proving with Analytic Tableaux and Related Methods, Peter Baumgartner, Reiner Hähnle, and Joachim Possega (eds.), (Lecture Notes in Computer Science 918), Berlin, Heidelberg: Springer Berlin Heidelberg, 294–309. doi:10.1007/3-540-59338-1_43 (Scholar)
–––, 1998, “Higher-Order Automated Theorem Proving”, in Automated Deduction—A Basis for Applications, Volume 1, Wolfgang Bibel and Peter H. Schmitt (eds.), Dordrecht: Kluwer, 431–462. (Scholar)
Konrad, Karsten, 1998, “Hot: A Concurrent Automated Theorem Prover Based on Higher-Order Tableaux”, in Theorem Proving in Higher Order Logics, Jim Grundy and Malcolm Newey (eds.), (Lecture Notes in Computer Science 1479), Berlin, Heidelberg: Springer Berlin Heidelberg, 245–261. doi:10.1007/bfb0055140 (Scholar)
Kumar, Ramana, Rob Arthan, Magnus O. Myreen, and Scott Owens, 2016, “Self-Formalisation of Higher-Order Logic”, Journal of Automated Reasoning, 56:221–259. doi:10.1007/s10817-015-9357-x (Scholar)
Maslov, S. Yu, 1967, “An Inverse Method for Establishing Deducibility of Nonprenex Formulas of Predicate Calculus”, Soviet Mathematics Doklady, 8(1): 16–19. (Scholar)
Miller, Dale A., 1983, Proofs in Higher-Order Logic, Ph.D. dissertation, Mathematics Department, Carnegie Mellon University. (Scholar)
–––, 1987, “A Compact Representation of Proofs”, Studia Logica, 46(4): 347–370. doi:10.1007/bf00370646 (Scholar)
–––, 1991, “A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification”, Journal of Logic and Computation, 1(4): 497–536. doi:10.1093/logcom/1.4.497 (Scholar)
Mints, G., 1999, “Cut-Elimination for Simple Type Theory with an Axiom of Choice”, The Journal of Symbolic Logic, 64(2): 479–485. doi:10.2307/2586480 (Scholar)
Montague, Richard, 1974, Formal Philosophy. Selected Papers Of Richard Montague, edited and with an introduction by Richmond H. Thomason, New Haven: Yale University Press. (Scholar)
Muskens, Reinhard, 2006, “Higher Order Modal Logic”, in Handbook of Modal Logic, Patrick Blackburn, Johan Van Benthem, and Frank Wolter (eds.), Amsterdam: Elsevier, 621–653. (Scholar)
–––, 2007, “Intensional Models for the Theory of Types”, The Journal of Symbolic Logic, 72(1): 98–118. doi:10.2178/jsl/1174668386 (Scholar)
Nipkow, Tobias, Markus Wenzel, and Lawrence C. Paulson (eds.), 2002, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, (Lecture Notes in Computer Science 2283), Berlin, Heidelberg: Springer Berlin Heidelberg. doi:10.1007/3-540-45949-9 (Scholar)
Owre, S., S. Rajan, J. M. Rushby, N. Shankar, and M. Srivas, 1996, “PVS: Combining Specification, Proof Checking, and Model Checking”, in Computer Aided Verification, Rajeev Alur and Thomas A. Henzinger (eds.), (Lecture Notes in Computer Science 1102), Berlin, Heidelberg: Springer Berlin Heidelberg, 411–414. doi:10.1007/3-540-61474-5_91 (Scholar)
Paulson, Lawrence C, 1988, “Isabelle: The next Seven Hundred Theorem Provers”, in 9th International Conference on Automated Deduction, Ewing Lusk and Ross Overbeek (eds.), (Lecture Notes in Computer Science 310), Berlin/Heidelberg: Springer-Verlag, 772–773. doi:10.1007/bfb0012891 (Scholar)
–––, 1990, “A Formulation of the Simple Theory of Types (for Isabelle)”, in COLOG-88, Per Martin-Löf and Grigori Mints (eds.), (Lecture Notes in Computer Science 417), Berlin, Heidelberg: Springer Berlin Heidelberg, 246–274. doi:10.1007/3-540-52335-9_58 (Scholar)
Prawitz, Dag, 1968, “Hauptsatz for Higher Order Logic”, The Journal of Symbolic Logic, 33(3): 452–457. doi:10.2307/2270331 (Scholar)
Quine, W. V., 1956, “Unification of Universes in Set Theory”, The Journal of Symbolic Logic, 21(3): 267–279. doi:10.2307/2269102 (Scholar)
Richardson, Julian, Alan Smaill, and Ian Green, 1998, “System Description: Proof Planning in Higher-Order Logic with ΛClam”, in Kirchner and Kirchner 1998: 129–133. doi:10.1007/bfb0054254 (Scholar)
Robinson, Alan and Andrei Voronkov (eds.), 2001, Handbook of Automated Reasoning, Volumes 1 and 2, Amsterdam: Elsevier Science. (Scholar)
Russell, Bertrand, 1903, The Principles of Mathematics, Cambridge: Cambridge University Press. (Scholar)
–––, 1908, “Mathematical Logic as Based on the Theory of Types”, American Journal of Mathematics, 30(3): 222–262. Reprinted in van Heijenoort 1967: 150–182. doi:10.2307/2369948 (Scholar)
Schlichtkrull, Anders, 2023, “Soundness of the Q0 proof system for higher-order logic”, Archive of Formal Proofs. https://www.isa-afp.org/entries/Q0_Soundness.html (Scholar)
Schlichtkrull, Anders, Jasmin Blanchette, Dmitriy Traytel, and Uwe Waldmann, 2020, “Formalizing Bachmair and Ganzinger's Ordered Resolution Prover.” Journal of Automated Reasoning, 64(7): 1169-1195. doi:10.1007/s10817-020-09561-0 (Scholar)
Schönfinkel, M., 1924, “Über die Bausteine der mathematischen Logik”, Mathematische Annalen, 92(3–4): 305–316. Translated in van Heijenoort 1967: 355–366. doi:10.1007/bf01448013 (Scholar)
Schütte, Kurt, 1960, “Syntactical and Semantical Properties of Simple Type Theory”, The Journal of Symbolic Logic, 25(4): 305–326. doi:10.2307/2963525 (Scholar)
Shankar, Natarajan, 2001, “Using Decision Procedures with a Higher-Order Logic”, in Theorem Proving in Higher Order Logics, Richard J. Boulton and Paul B. Jackson (eds.), (Lecture Notes in Computer Science 2152), Berlin, Heidelberg: Springer Berlin Heidelberg, 5–26. doi:10.1007/3-540-44755-5_3 (Scholar)
Siekmann, Jörg H. and Graham Wrightson (eds.), 1983, Automation of Reasoning, (Classical Papers on Computational Logic 1967–1970: Vol. 2), Berlin, Heidelberg: Springer Berlin Heidelberg. doi:10.1007/978-3-642-81955-1 (Scholar)
Siekmann, Jörg, Christoph Benzmüller, and Serge Autexier, 2006, “Computer Supported Mathematics with ΩMEGA”, Journal of Applied Logic, 4(4): 533–559. doi:10.1016/j.jal.2005.10.008 (Scholar)
Smullyan, Raymond M., 1963, “A Unifying Principal in Quantification Theory”, Proceedings of the National Academy of Sciences, 49(6): 828–832. doi:10.1073/pnas.49.6.828 (Scholar)
–––, 1995, First-Order Logic, New York: Dover, second corrected edition. (Scholar)
Steen, Alexander, 2018, Extensional Paramodulation for Higher-Order Logic and its Effective Implementation Leo-III, Ph.D. dissertation, Series: Dissertations in Artificial Intelligence (DISKI), Volume 345, Berlin: AKA-Verlag (IOS Press). (Scholar)
Steen, Alexander and Christoph Benzmüller, 2018, “The Higher-Order Prover Leo-III”, in Galmiche et al. 2018: 108–116. doi:10.1007/978-3-319-94205-6_8 (Scholar)
Steen, Alexander and Christoph Benzmüller, 2021, “Extensional Higher-Order Paramodulation in Leo-III”, Journal of Automated Reasoning, 65: 775–807. doi:10.1007/s10817-021-09588-x (Scholar)
Steen, Alexander, Geoff Sutcliffe, Tobias Scholl, Christoph Benzmüller, 2023, “Solving Modal Logic Problems by Translation to Higher-Order Logic”, in Logic and Argumentation. CLAR 2023, Andreas Herzig, Jieting Luo, Pere Pardo (eds.), (Lecture Notes in Computer Science 14156), Cham: Springer Nature Switzerland AG. doi:10.1007/978-3-031-40875-5_3 (Scholar)
Stenlund, Sören, 1972, Combinators, λ-Terms and Proof Theory, (Synthese Library 42), Dordrecht: Springer Netherlands. doi:10.1007/978-94-010-2913-1 (Scholar)
Sutcliffe, Geoff, 2016, “The CADE ATP System Competition—CASC”, AI Magazine, 37(2): 99–101. doi:10.1609/aimag.v37i2.2620 (Scholar)
–––, 2017, “The TPTP Problem Library and Associated Infrastructure: From CNF to TH0, TPTP v6.4.0”, Journal of Automated Reasoning, 59(4): 483–502. doi:10.1007/s10817-017-9407-7 (Scholar)
–––, 2023, “The logic languages of the TPTP world”, Logic Journal of the IGPL, 31(6): 1153–1169. doi:10.1093/jigpal/jzac068 (Scholar)
Sutcliffe, Geoff and Christoph Benzmüller, 2010, “Automated Reasoning in Higher-Order Logic Using the TPTP THF Infrastructure”, Journal of Formalized Reasoning, 3(1): 1–27. doi:10.6092/issn.1972-5787/1710 (Scholar)
Takahashi, Moto-o, 1967, “A Proof of Cut-Elimination Theorem in Simple Type-Theory”, Journal of the Mathematical Society of Japan, 19(4): 399–410. doi:10.2969/jmsj/01940399 (Scholar)
–––, 1970, “A System of Simple Type Theory of Gentzen Style with Inference on Extensionality, and the Cut Elimination in It”, Commentarii Mathematici Universitatis Sancti Pauli, 18(2):129–147. (Scholar)
Takeuti, Gaisi, 1987, Proof Theory, second edition, Amsterdam: North-Holland. (Scholar)
Tarski, Alfred [Tajtelbaum, Alfred], 1923, “Sur Le Terme Primitif de La Logistique”, Fundamenta Mathematicae, 4: 196–200. Translated in Tarski 1956, 1–23. doi:10.4064/fm-4-1-196-200 (Scholar)
–––, 1956, Logic, Semantics, Metamathematics: Papers from 1923 to 1938, Oxford: Oxford University Press. (Scholar)
van Heijenoort, Jean, 1967, From Frege to Gödel. A Source Book in Mathematical Logic 1879–1931, Cambridge, MA: Harvard University Press. (Scholar)
Vukmirović, Petar, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret, 2022, “Making Higher-Order Superposition Work”, Journal of Automated Reasoning, 66:541–564. doi10.1007/s10817-021-09613-z (Scholar)
Vukmirović, Petar, Jasmin Blanchette, and Stephan Schulz, 2023, “Extending a High-Performance Prover to Higher-Order Logic”, in Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2023, Sankaranarayanan, S., Sharygina, N. (eds.), (Lecture Notes in Computer Science 13994), Cham: Springer Nature Switzerland AG. doi:10.1007/978-3-031-30820-8_10 (Scholar)
Whitehead, Alfred N. and Bertrand Russell, 1927a, Principia Mathematica, Volume 1, Cambridge: Cambridge University Press, second edition. (Scholar)
–––, 1927b, “Incomplete Symbols”, in Whitehead & Russell 1927a: 66–84; reprinted in van Heijenoort 1967: 216–223. (Scholar)
Yasuhara, Mitsuru, 1975, “The Axiom of Choice in Church’s Type Theory” (abstract), Notices of the American Mathematical Society, 22(January): A34. [Yashuhara 1975 available online] (Scholar)

Generated Tue Dec 3 04:43:16 2024

Applied ethics	Epistemology	History of Western Philosophy	Meta-ethics	Metaphysics	Normative ethics
Philosophy of biology	Philosophy of language	Philosophy of mind	Philosophy of religion	Science Logic and Mathematics	More ...