Powered by AppSignal & Oban Pro
Notesclub
Sign in with GitHub
created by hec & contributors
terms privacy

Bibliography

90_bibliography.livemd

avatar
Johannes Schuster
avatar
avatar
Share to X
Share to Bluesky
More notebooks

Bibliography

Type Theory and Higher-Order Logic

  • [And02] Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, second edition. Applied Logic Series 27. Kluwer Academic Publishers, 2002.
  • [BBK04] Christoph Benzmüller, Chad E. Brown, and Michael Kohlhase. Higher-order semantics and extensionality. The Journal of Symbolic Logic, 69(4):1027–1088, 2004.
  • [Ben02] Christoph Benzmüller. Comparing approaches to resolution based higher-order theorem proving. Synthese, 133(1–2):203–335, 2002.
  • [Ben99a] Christoph Benzmüller. Equality and Extensionality in Automated Higher Order Theorem Proving. PhD thesis, Universität des Saarlandes, Saarbrücken, 1999.
  • [Ben99b] Christoph Benzmüller. Extensional higher-order paramodulation and RUE-resolution. In Automated Deduction (CADE-16), LNCS 1632, pages 399–413. Springer, 1999.
  • [BK98] Christoph Benzmüller and Michael Kohlhase. Extensional higher-order resolution. In Automated Deduction (CADE-15), LNCS 1421, pages 56–71. Springer, 1998.
  • [BM14] Christoph Benzmüller and Dale Miller. Automation of higher-order logic. In Computational Logic, Handbook of the History of Logic 9, pages 215–254. Elsevier, 2014.
  • [Chu40] Alonzo Church. A formulation of the simple theory of types. The Journal of Symbolic Logic, 5(2):56–68, 1940.
  • [dB72] Nicolaas G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae, 75(5):381–392, 1972.
  • [Hen50] Leon Henkin. Completeness in the theory of types. The Journal of Symbolic Logic, 15(2):81–91, 1950.

Tableaux

  • [ABB00] Peter B. Andrews, Matthew Bishop, and Chad E. Brown. System description: TPS: A theorem proving system for type theory. In Automated Deduction (CADE-17), LNCS 1831, pages 164–169. Springer, 2000.
  • [And81] Peter B. Andrews. Theorem proving via general matings. Journal of the ACM, 28(2):193–214, 1981.
  • [And89] Peter B. Andrews. On connections and higher-order logic. Journal of Automated Reasoning, 5(3):257–291, 1989.
  • [BA98] Matthew Bishop and Peter B. Andrews. Selectively instantiating definitions. In Automated Deduction (CADE-15), LNCS 1421, pages 365–380. Springer, 1998.
  • [BB05] Christoph Benzmüller and Chad E. Brown. A structured set of higher-order problems. In Theorem Proving in Higher Order Logics (TPHOLs 2005), LNCS 3603, pages 66–81. Springer, 2005.
  • [BB11] Julian Backes and Chad E. Brown. Analytic tableaux for higher-order logic with choice. Journal of Automated Reasoning, 47(4):451–479, 2011.
  • [Fit96] Melvin Fitting. First-Order Logic and Automated Theorem Proving, second edition. Graduate Texts in Computer Science. Springer, 1996.
  • [Gie01] Martin Giese. Incremental closure of free variable tableaux. In Automated Reasoning (IJCAR 2001), LNCS 2083, pages 545–560. Springer, 2001.
  • [Hah01] Reiner Hähnle. Tableaux and related methods. In Handbook of Automated Reasoning, volume 1, chapter 3, pages 100–178. Elsevier and MIT Press, 2001.
  • [HS94] Reiner Hähnle and Peter H. Schmitt. The liberalized $\delta$-rule in free variable semantic tableaux. Journal of Automated Reasoning, 13(2):211–221, 1994.
  • [Koh95] Michael Kohlhase. Higher-order tableaux. In Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX 1995), LNCS 918, pages 294–309. Springer, 1995.
  • [Kon98] Karsten Konrad. HOT: A concurrent automated theorem prover based on higher-order tableaux. In Theorem Proving in Higher Order Logics (TPHOLs 1998), LNCS 1479, pages 245–261. Springer, 1998.
  • [Mil87] Dale A. Miller. A compact representation of proofs. Studia Logica, 46(4):347–370, 1987.
  • [Smu68] Raymond M. Smullyan. First-Order Logic. Ergebnisse der Mathematik und ihrer Grenzgebiete 43. Springer, 1968.

Unification

  • [Dow01] Gilles Dowek. Higher-order unification and matching. In Handbook of Automated Reasoning, volume 2, chapter 16, pages 1009–1062. Elsevier and MIT Press, 2001.
  • [Gol81] Warren D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13(2):225–230, 1981.
  • [Hue75] Gérard P. Huet. A unification algorithm for typed $\lambda$-calculus. Theoretical Computer Science, 1(1):27–57, 1975.
  • [Mil91] Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497–536, 1991.
  • [NM26] Johannes Niederhauser and Aart Middeldorp. Unification of deterministic higher-order patterns. In Automated Reasoning (IJCAR 2026), Lecture Notes in Computer Science. Springer, 2026. To appear; preprint arXiv:2601.14211.
  • [Sti09] Colin Stirling. Decidability of higher-order matching. Logical Methods in Computer Science, 5(3), 2009.

Term Orders, Rewriting and Superposition

  • [BBT+21] Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann. Superposition with lambdas. Journal of Automated Reasoning, 65(7):893–940, 2021.
  • [BG94] Leo Bachmair and Harald Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217–247, 1994.
  • [BJR15] Frédéric Blanqui, Jean-Pierre Jouannaud, and Albert Rubio. The computability path ordering. Logical Methods in Computer Science, 11(4:3), 2015.
  • [BN98] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
  • [Der82] Nachum Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279–301, 1982.
  • [NBTV21] Visa Nummelin, Alexander Bentkamp, Sophie Tourret, and Petar Vukmirović. Superposition with first-class Booleans and inprocessing clausification. In Automated Deduction (CADE-28), LNCS 12699, pages 378–395. Springer, 2021.
  • [NM25a] Johannes Niederhauser and Aart Middeldorp. The computability path order for $\beta\eta$-normal higher-order rewriting. In Automated Deduction (CADE-30), LNCS 15943, pages 207–225. Springer, 2025.
  • [NM25b] Johannes Niederhauser and Aart Middeldorp. NCPO goes $\beta\eta$-long normal form. In Proceedings of the 20th International Workshop on Termination (WST 2025), Leipzig, Germany, 2025. Informal proceedings.
  • [VBB+21] Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret. Making higher-order superposition work. In Automated Deduction (CADE-28), LNCS 12699, pages 415–432. Springer, 2021.

Agent Architectures, Parallel Deduction and Model Finding

  • [BN10] Jasmin Christian Blanchette and Tobias Nipkow. Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In Interactive Theorem Proving (ITP 2010), LNCS 6172, pages 131–146. Springer, 2010.
  • [Bon00] Maria Paola Bonacina. A taxonomy of parallel strategies for deduction. Annals of Mathematics and Artificial Intelligence, 29(1):223–257, 2000.
  • [BS98] Christoph Benzmüller and Volker Sorge. A blackboard architecture for guiding interactive proofs. In Artificial Intelligence: Methodology, Systems, and Applications (AIMSA 1998), LNCS 1480, pages 102–114. Springer, 1998.
  • [BSJK05] Christoph Benzmüller, Volker Sorge, Mateja Jamnik, and Manfred Kerber. Can a higher-order and a first-order theorem prover cooperate? In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2004), LNCS 3452, pages 415–431. Springer, 2005.
  • [BSJK08] Christoph Benzmüller, Volker Sorge, Mateja Jamnik, and Manfred Kerber. Combined reasoning by automated cooperation. Journal of Applied Logic, 6(3):318–342, 2008.
  • [CRD+22] Julie Cailler, Johann Rosain, David Delahaye, Simon Robillard, and Hinde Lilia Bouziane. Goéland: A concurrent tableau-based theorem prover (system description). In Automated Reasoning (IJCAR 2022), LNCS 13385, pages 359–368. Springer, 2022.
  • [Sor01] Volker Sorge. $\Omega$-ANTS: A Blackboard Architecture for the Integration of Reasoning Techniques into Proof Planning. PhD thesis, Universität des Saarlandes, Saarbrücken, 2001.
  • [SWB16] Alexander Steen, Max Wisniewski, and Christoph Benzmüller. Agent-based HOL reasoning. In Mathematical Software (ICMS 2016), LNCS 9725, pages 75–81. Springer, 2016.
  • [WB16] Max Wisniewski and Christoph Benzmüller. Is it reasonable to employ agents in automated theorem proving? In Agents and Artificial Intelligence (ICAART 2016), volume 1, pages 281–286. SCITEPRESS, 2016.
  • [WSB15] Max Wisniewski, Alexander Steen, and Christoph Benzmüller. LeoPARD: A generic platform for the implementation of higher-order reasoners. In Intelligent Computer Mathematics (CICM 2015), LNCS 9150, pages 325–330. Springer, 2015.

Systems and Implementation

  • [Arm03] Joe Armstrong. Making Reliable Distributed Systems in the Presence of Software Errors. PhD thesis, Royal Institute of Technology (KTH), Stockholm, 2003.
  • [BK22] Chad E. Brown and Cezary Kaliszyk. Lash 1.0 (system description). In Automated Reasoning (IJCAR 2022), LNCS 13385, pages 350–358. Springer, 2022.
  • [BPTF08] Christoph Benzmüller, Lawrence C. Paulson, Frank Theiss, and Arnaud Fietzke. LEO-II: A cooperative automatic theorem prover for classical higher-order logic (system description). In Automated Reasoning (IJCAR 2008), LNCS 5195, pages 162–170. Springer, 2008.
  • [Bro12] Chad E. Brown. Satallax: An automatic higher-order prover. In Automated Reasoning (IJCAR 2012), LNCS 7364, pages 111–117. Springer, 2012.
  • [Bry86] Randal E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, 1986.
  • [BSPT15] Christoph Benzmüller, Nik Sultana, Lawrence C. Paulson, and Frank Theiss. The higher-order prover Leo-II. Journal of Automated Reasoning, 55(4):389–404, 2015.
  • [BSW17] Christoph Benzmüller, Alexander Steen, and Max Wisniewski. Leo-III version 1.1 (system description). In LPAR-21 Workshops (IWIL), Kalpa Publications in Computing 1, pages 11–26, 2017.
  • [FC06] Jean-Christophe Filliâtre and Sylvain Conchon. Type-safe modular hash-consing. In Proceedings of the 2006 Workshop on ML, pages 12–19. ACM, 2006.
  • [HW03] Gregor Hohpe and Bobby Woolf. Enterprise Integration Patterns: Designing, Building, and Deploying Messaging Solutions. Addison-Wesley, 2003.
  • [Joh85] Thomas Johnsson. Lambda lifting: Transforming programs to recursive equations. In Functional Programming Languages and Computer Architecture (FPCA 1985), LNCS 201, pages 190–203. Springer, 1985.
  • [Knu84] Donald E. Knuth. Literate programming. The Computer Journal, 27(2):97–111, 1984.
  • [KSR16] Cezary Kaliszyk, Geoff Sutcliffe, and Florian Rabe. TH1: The TPTP typed higher-order form with rank-1 polymorphism. In Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016), CEUR Workshop Proceedings 1635, pages 41–55, 2016.
  • [Liv25] The Livebook Team. Livebook: Automate code and data workflows with interactive Elixir notebooks. https://livebook.dev, 2025.
  • [SB10] Geoff Sutcliffe and Christoph Benzmüller. Automated reasoning in higher-order logic using the TPTP THF infrastructure. Journal of Formalized Reasoning, 3(1):1–27, 2010.
  • [SB21] Alexander Steen and Christoph Benzmüller. Extensional higher-order paramodulation in Leo-III. Journal of Automated Reasoning, 65(6):775–807, 2021.
  • [SO25] Stack Overflow. 2025 Developer Survey: Technology. https://survey.stackoverflow.co/2025/technology, 2025.
  • [Sut08] Geoff Sutcliffe. The SZS ontologies for automated reasoning software. In LPAR Workshops (KEAPPA/IWIL), CEUR Workshop Proceedings 418, pages 38–49, 2008.
  • [Sut17] Geoff Sutcliffe. The TPTP problem library and associated infrastructure: From CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning, 59(4):483–502, 2017.
  • [Sut26] Geoff Sutcliffe. The 13th IJCAR automated theorem proving system competition: CASC-J13. https://tptp.org/CASC/J13, 2026.

Previous: Chapter 9: Conclusion  $\cdot$  Contents  $\cdot$  Next: Appendix A: Examples

Other notebooks:

Back