Extensional Higher-Order Paramodulation in Leo-III
Tóm tắt
Từ khóa
Tài liệu tham khảo
Abadi, M., Cardelli, L., Curien, P., Lévy, J.: Explicit substitutions. J. Funct. Program. 1(4), 375–416 (1991). https://doi.org/10.1017/S0956796800000186
Andrews, P.B.: General models and extensionality. J. Symb. Log. 37(2), 395–397 (1972). https://doi.org/10.2307/2272982
Andrews, P.B.: General models, descriptions, and choice in type theory. J. Symb. Log. 37(2), 385–394 (1972). https://doi.org/10.2307/2272981
Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory. Springer, Applied Logic Series (2002)
Andrews, P.B., Bishop, M., Brown, C.E.: System description: TPS: A theorem proving system for type theory. In: D.A. McAllester (ed.) Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings, Lecture Notes in Computer Science, vol. 1831, pp. 164–169. Springer (2000). https://doi.org/10.1007/10721959_11
Andrews, P.B., Brown, C.E.: TPS: a hybrid automatic-interactive system for developing proofs. J. Appl. Logic 4(4), 367–395 (2006). https://doi.org/10.1016/j.jal.2005.10.002
Andrews, P.B., Miller, D.A., Cohen, E.L., Pfenning, F.: Automating higher-order logic. Contemp. Math. 29, 169–192 (1984)
Bachmair, L., Ganzinger, H.: On restrictions of ordered paramodulation with simplification. In: M.E. Stickel (ed.) 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, Lecture Notes in Computer Science, vol. 449, pp. 427–441. Springer (1990). https://doi.org/10.1007/3-540-52885-7_105
Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217–247 (1994). https://doi.org/10.1093/logcom/4.3.217
Barbosa, H., Reynolds, A., Ouraoui, D.E., Tinelli, C., Barrett, C.W.: Extending SMT solvers to higher-order logic. In: P. Fontaine (ed.) Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11716, pp. 35–54. Springer (2019). https://doi.org/10.1007/978-3-030-29436-6_3
Barcan, R.C.: A functional calculus of first order based on strict implication. J. Symb. Log. 11(1), 1–16 (1946). https://doi.org/10.2307/2269159
Barendregt, H.P., Dekkers, W., Statman, R.: Lambda Calculus with Types. Perspectives in logic. Cambridge University Press, Cambridge (2013)
Barrett, C., et al.: CVC4. In: G. Gopalakrishnan, S. Qadeer (eds.) Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, LNCS, vol. 6806, pp. 171–177. Springer (2011). https://doi.org/10.1007/978-3-642-22110-1_14
Bentkamp, A., Blanchette, J., Tourret, S., Vukmirovic, P., Waldmann, U.: Superposition with lambdas. In: P. Fontaine (ed.) Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11716, pp. 55–73. Springer (2019). https://doi.org/10.1007/978-3-030-29436-6_4
Bentkamp, A., Blanchette, J.C., Cruanes, S., Waldmann, U.: Superposition for lambda-free higher-order logic. In: D. Galmiche, S. Schulz, R. Sebastiani (eds.) Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Lecture Notes in Computer Science, vol. 10900, pp. 28–46. Springer (2018). https://doi.org/10.1007/978-3-319-94205-6_3
Benzmüller, C.: Equality and extensionality in automated higher order theorem proving. Ph.D. thesis, Saarland University, Saarbrücken, Germany (1999)
Benzmüller, C.: Extensional higher-order paramodulation and RUE-resolution. In: H. Ganzinger (ed.) Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, Lecture Notes in Computer Science, vol. 1632, pp. 399–413. Springer (1999). https://doi.org/10.1007/3-540-48660-7_39
Benzmüller, C.: Combining and automating classical and non-classical logics in classical higher-order logics. Ann. Math. Artif. Intell. 62(1–2), 103–128 (2011). https://doi.org/10.1007/s10472-011-9249-7
Benzmüller, C.: Cut-elimination for quantified conditional logic. J. Philos. Logic 46(3), 333–353 (2017). https://doi.org/10.1007/s10992-016-9403-0
Benzmüller, C.: Universal (meta-)logical reasoning: recent successes. Sci. Comput. Prog. 172, 48–62 (2019). https://doi.org/10.1016/j.scico.2018.10.008
Benzmüller, C., Brown, C.E., Kohlhase, M.: Higher-order semantics and extensionality. J. Symb. Log. 69(4), 1027–1088 (2004). https://doi.org/10.2178/jsl/1102022211
Benzmüller, C., Brown, C.E., Kohlhase, M.: Cut-simulation and impredicativity. Logical Methods Comput. Sci. 5(1), (2009)
Benzmüller, C., Farjami, A., Parent, X.: A dyadic deontic logic in HOL. In: J.M. Broersen, C. Condoravdi, N. Shyam, G. Pigozzi (eds.) Deontic Logic and Normative Systems - 14th International Conference, DEON 2018, Utrecht, The Netherlands, July 3-6, 2018., pp. 33–49. College Publications (2018)
Benzmüller, C., Kohlhase, M.: System description: LEO - A higher-order theorem prover. In: C. Kirchner, H. Kirchner (eds.) Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings, Lecture Notes in Computer Science, vol. 1421, pp. 139–144. Springer (1998). https://doi.org/10.1007/BFb0054256
Benzmüller, C., Miller, D.: Automation of higher-order logic. In: Siekmann, J.H. (ed.) Computational Logic, Handbook of the History of Logic. Elsevier, Amsterdam (2014)
Benzmüller, C., Otten, J., Raths, T.: Implementing and evaluating provers for first-order modal logics. In: L.D. Raedt, et al. (eds.) ECAI 2012 - 20th European Conference on Artificial Intelligence. Including prestigious applications of artificial intelligence (PAIS-2012) system demonstrations track, montpellier, France, August 27-31 , 2012, Frontiers in Artificial Intelligence and applications, vol. 242, pp. 163–168. IOS Press (2012). https://doi.org/10.3233/978-1-61499-098-7-163
Benzmüller, C., Paulson, L.C.: Multimodal and intuitionistic logics in simple type theory. Logic J. IGPL 18(6), 881–892 (2010). https://doi.org/10.1093/jigpal/jzp080
Benzmüller, C., Paulson, L.C.: Quantified multimodal logics in simple type theory. Logica Univ. 7(1), 7–20 (2013). https://doi.org/10.1007/s11787-012-0052-y
Benzmüller, C., Raths, T.: HOL based first-order modal logic provers. In: K.L. McMillan, A. Middeldorp, A. Voronkov (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8312, pp. 127–136. Springer (2013). https://doi.org/10.1007/978-3-642-45221-5_9
Benzmüller, C., Scott, D.S.: Automating free logic in Isabelle/HOL. In: G. Greuel, T. Koch, P. Paule, A.J. Sommese (eds.) Mathematical software - ICMS 2016 - 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings, Lecture Notes in Computer Science, vol. 9725, pp. 43–50. Springer (2016). https://doi.org/10.1007/978-3-319-42432-3_6
Benzmüller, C., Steen, A., Wisniewski, M.: Leo-III Version 1.1 (System description). In: T. Eiter, D. Sands, G. Sutcliffe, A. Voronkov (eds.) IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, Maun, Botswana, May 7-12, 2017, Kalpa publications in computing, vol. 1. EasyChair (2017). https://doi.org/10.29007/grmx
Benzmüller, C., Sultana, N., Paulson, L.C., Theiss, F.: The higher-order prover LEO-II. J. Autom. Reason. 55(4), 389–404 (2015). https://doi.org/10.1007/s10817-015-9348-y
Benzmüller, C., Weber, L., Woltzenlogel Paleo, B.: Computer-assisted analysis of the Anderson-Hájek ontological controversy. Logica Univ. 11(1), 139–151 (2017). https://doi.org/10.1007/s11787-017-0160-9
Benzmüller, C., Woltzenlogel Paleo, B.: The inconsistency in Gödel’s ontological argument: A success story for AI in metaphysics. In: S. Kambhampati (ed.) Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016, pp. 936–942. IJCAI/AAAI Press (2016)
Benzmüller, C., Woltzenlogel Paleo, B.: Experiments in computational metaphysics: Gödel’s proof of God’s existence Savijnanam scientific exploration for a spiritual paradigm. J. Bhaktivedanta Inst. 9, 43–57 (2017)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development - Coq’Art The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Berlin (2004)
Bhayat, A., Reger, G.: Set of support for higher-order reasoning. In: B. Konev, J. Urban, P. Rümmer (eds.) Proceedings of the 6th Workshop on practical aspects of automated reasoning co-located with Federated Logic Conference 2018 (FLoC 2018), Oxford, UK, July 19th, 2018., CEUR Workshop Proceedings, vol. 2162, pp. 2–16. CEUR-WS.org (2018)
Bhayat, A., Reger, G.: Restricted combinatory unification. In: P. Fontaine (ed.) Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11716, pp. 74–93. Springer (2019). https://doi.org/10.1007/978-3-030-29436-6_5
Blackburn, P., van Benthem, J.F., Wolter, F.: Handbook of modal logic, vol. 3. Elsevier, Amsterdam (2006)
Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109–128 (2013). https://doi.org/10.1007/s10817-013-9278-5
Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. Logical methods in computer science 12(4), (2016). https://doi.org/10.2168/LMCS-12(4:13)2016
Blanchette, J.C., Nipkow, T.: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: M. Kaufmann, L.C. Paulson (eds.) Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6172, pp. 131–146. Springer (2010). https://doi.org/10.1007/978-3-642-14052-5_11
Blanchette, J.C., Paskevich, A.: TFF1: the TPTP typed first-order form with rank-1 polymorphism. In: M.P. Bonacina (ed.) Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, LNCS, vol. 7898, pp. 414–420. Springer (2013). https://doi.org/10.1007/978-3-642-38574-2_29
Blanchette, J.C., Weber, T., Batty, M., Owens, S., Sarkar, S.: Nitpicking C++ concurrency. In: P. Schneider-Kamp, M. Hanus (eds.) Proceedings of the 13th International ACM SIGPLAN Conference on principles and practice of declarative programming, July 20-22, 2011, Odense, Denmark, pp. 113–124. ACM (2011). https://doi.org/10.1145/2003476.2003493
Böhme, S.: Proving theorems of higher-order logic with SMT solvers. Ph.D. thesis, Technische Universität München (2012)
Brown, C.E.: Satallax: An automatic higher-order prover. In: B. Gramlich, D. Miller, U. Sattler (eds.) Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7364, pp. 111–117. Springer (2012). https://doi.org/10.1007/978-3-642-31365-3_11
Brown, C.E., Gauthier, T., Kaliszyk, C., Sutcliffe, G., Urban, J.: GRUNGE: A grand unified ATP challenge. In: P. Fontaine (ed.) Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11716, pp. 123–141. Springer (2019). https://doi.org/10.1007/978-3-030-29436-6_8
Bruijn, N.G.D.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. INDAG. Math 34, 381–392 (1972)
Cervesato, I., Pfenning, F.: A linear spine calculus. J. Log. Comput. 13(5), 639–688 (2003). https://doi.org/10.1093/logcom/13.5.639
Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(2), 56–68 (1940). https://doi.org/10.2307/2266170
Couchot, J., Lescuyer, S.: Handling polymorphism in automated deduction. In: F. Pfenning (ed.) Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4603, pp. 263–278. Springer (2007). https://doi.org/10.1007/978-3-540-73595-3_18
Cruanes, S.: Extending superposition with integer arithmetic, structural induction, and beyond. (extensions de la superposition pour l’arithmétique linéaire entière, l’induction structurelle, et bien plus encore). Ph.D. thesis, École Polytechnique, Palaiseau, France (2015)
Denzinger, J., Kronenburg, M., Schulz, S.: Discount-a distributed and learning equational prover. J. Autom. Reason. 18(2), 189–198 (1997). https://doi.org/10.1023/A:1005879229581
Digricoli, V.J., Harrison, M.C.: Equality-based binary resolution. J. ACM 33(2), 253–289 (1986). https://doi.org/10.1145/5383.5389
Frege, G.: Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Verlag von Louis Nebert, Halle (1879)
Fuenmayor, D., Benzmüller, C.: Types, tableaus and Gödel’s God in Isabelle/HOL. Arch. Formal Proofs (2017)
Gleißner, T., Steen, A.: The MET: The art of flexible reasoning with modalities. In: C. Benzmüller, F. Ricca, X. Parent, D. Roman (eds.) Rules and Reasoning - Second International Joint Conference, RuleML+RR 2018, Luxembourg, September 18-21, 2018, Proceedings, LNCS, vol. 11092, pp. 274–284. Springer (2018). https://doi.org/10.1007/978-3-319-99906-7_19
Gleißner, T., Steen, A., Benzmüller, C.: Theorem provers for every normal modal logic. In: T. Eiter, D. Sands (eds.) LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, EPiC Series in Computing, vol. 46, pp. 14–30. EasyChair (2017). https://doi.org/10.29007/jsb9
Goldfarb, W.D.: The undecidability of the second-order unification problem. Theor. Comput. Sci. 13(2), 225–230 (1981)
Gordon, M.J., Melham, T.F.: Introduction to HOL A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)
Hales, T.C., et al.: A formal proof of the kepler conjecture. CoRR abs/1501.02155 (2015)
Harrison, J.: HOL Light: An overview. In: S. Berghofer, T. Nipkow, C. Urban, M. Wenzel (eds.) Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5674, pp. 60–66. Springer (2009). https://doi.org/10.1007/978-3-642-03359-9_4
Henkin, L.: Completeness in the theory of types. J. Symb. Log. 15(2), 81–91 (1950). https://doi.org/10.2307/2266967
Huet, G.P.: The undecidability of unification in third order logic. Inf. control 22(3), 257–267 (1973)
Hustadt, U., Schmidt, R.A.: MSPASS: modal reasoning by translation and first-order resolution. In: R. Dyckhoff (ed.) Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2000, St Andrews, Scotland, UK, July 3-7, 2000, Proceedings, Lecture Notes in Computer Science, vol. 1847, pp. 67–71. Springer (2000). https://doi.org/10.1007/10722086_7
Kaliszyk, C., Sutcliffe, G., Rabe, F.: TH1: the TPTP typed higher-order form with rank-1 polymorphism. In: P. Fontaine, S. Schulz, J. Urban (eds.) Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning, CEUR Workshop Proceedings, vol. 1635, pp. 41–55. CEUR-WS.org (2016)
Kfoury, A.J., Rocca, S.R.D., Tiuryn, J., Urzyczyn, P.: Alpha-conversion and typability. Inf. Comput. 150(1), 1–21 (1999). https://doi.org/10.1006/inco.1998.2756
Kirchner, D., Benzmüller, C., Zalta, E.N.: Computer science and metaphysics: a cross-fertilization. Open Philos. 2(1), 230–251 (2019). https://doi.org/10.1515/opphil-2019-0015
Korovin, K.: iProver - an instantiation-based theorem prover for first-order logic (system description). In: A. Armando, P. Baumgartner, G. Dowek (eds.) Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, LNCS, vol. 5195, pp. 292–298. Springer (2008). https://doi.org/10.1007/978-3-540-71070-7_24
Leibniz, G.W.: Discourse on metaphysics. In: L.E. Loemker (ed.) Philosophical Papers and Letters, pp. 303–330. Springer Netherlands, Dordrecht (1989). https://doi.org/10.1007/978-94-010-1426-7_36
Lindblad, F.: A focused sequent calculus for higher-order logic. In: S. Demri, D. Kapur, C. Weidenbach (eds.) Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8562, pp. 61–75. Springer (2014). https://doi.org/10.1007/978-3-319-08587-6_5
Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reasoning 40(1), 35–60 (2008). https://doi.org/10.1007/s10817-007-9085-y
Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Logic 7(1), 41–57 (2009)
Miller, D.A.: Proofs in higher-order logic. Ph.D. thesis, Carnegie-Mellon University (1983)
Miller, D.A.: A logic programming language with lambda-abstraction, function variables, and simple unification. J. Log. Comput. 1(4), 497–536 (1991). https://doi.org/10.1093/logcom/1.4.497
Muskens, R.: Intensional models for the theory of types. J. Symb. Log. 72(1), 98–118 (2007). https://doi.org/10.2178/jsl/1174668386
Nieuwenhuis, R., Rubio, A.: Theorem proving with ordering constrained clauses. In: D. Kapur (ed.) Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings, Lecture Notes in Computer Science, vol. 607, pp. 477–491. Springer (1992). https://doi.org/10.1007/3-540-55602-8_186
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science. Springer, Berlin (2002)
Otten, J.: MleanCoP: A connection prover for first-order modal logic. In: S. Demri, D. Kapur, C. Weidenbach (eds.) Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8562, pp. 269–276. Springer (2014). https://doi.org/10.1007/978-3-319-08587-6_20
Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: D. Kapur (ed.) Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings, Lecture Notes in Computer Science, vol. 607, pp. 748–752. Springer (1992). https://doi.org/10.1007/3-540-55602-8_217
Raths, T., Otten, J.: The QMLTP problem library for first-order modal logics. In: B. Gramlich, D. Miller, U. Sattler (eds.) Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, LNCS, vol. 7364, pp. 454–461. Springer (2012). https://doi.org/10.1007/978-3-642-31365-3_35
Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2–3), 91–110 (2002)
Robinson, G., Wos, L.: Paramodulation and theorem-proving in first-order theories with equality. Mach. Intell. 4, 135–150 (1969)
Schulz, S.: E-A Brainiac theorem prover. AI Commun. 15(3), 111–126 (2002)
Siekmann, J.H., Benzmüller, C., Autexier, S.: Computer supported mathematics with $$\Omega $$MEGA. J. Appl. Logic 4(4), 533–559 (2006). https://doi.org/10.1016/j.jal.2005.10.008
Slind, K., Norrish, M.: A brief overview of HOL4. In: O.A. Mohamed, C.A. Muñoz, S. Tahar (eds.) Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, Lecture Notes in Computer Science, vol. 5170, pp. 28–32. Springer (2008). https://doi.org/10.1007/978-3-540-71067-7_6
Snyder, W., Gallier, J.: Higher-Order unification revisited: complete sets of transformations. J. Symb. Comput. 8, 101–140 (1989)
Steen, A.: Extensional paramodulation for Higher-Order logic and its effective implementation Leo-III, DISKI, vol. 345. Akademische Verlagsgesellschaft AKA GmbH, Berlin, : Dissertation. Freie Universität Berlin, Germany (2018)
Steen, A., Benzmüller, C.: Sweet SIXTEEN: automation via embedding into classical higher-order logic. Logic Logical Philos. 25(4), 535–554 (2016)
Steen, A., Benzmüller, C.: The higher-order prover Leo-III. In: D. Galmiche, S. Schulz, R. Sebastiani (eds.) Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as part of the federated logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, LNCS, vol. 10900, pp. 108–116. Springer (2018). https://doi.org/10.1007/978-3-319-94205-6_8
Steen, A., Benzmüller, C.: On reductions of Hintikka sets for higher-Order logic. arXiv:2004.07506 (2020). arxiv.org/abs/2004.07506
Steen, A., Wisniewski, M., Benzmüller, C.: Agent-based HOL reasoning. In: G. Greuel, T. Koch, P. Paule, A.J. Sommese (eds.) Mathematical Software - ICMS 2016 - 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings, LNCS, vol. 9725, pp. 75–81. Springer (2016). https://doi.org/10.1007/978-3-319-42432-3_10
Steen, A., Wisniewski, M., Benzmüller, C.: Going polymorphic - TH1 reasoning for Leo-III. In: T. Eiter, D. Sands, G. Sutcliffe, A. Voronkov (eds.) IWIL@LPAR 2017 Workshop and LPAR-21 short presentations, Maun, Botswana, May 7-12, 2017, Kalpa Publications in Computing, vol. 1. EasyChair (2017). https://doi.org/10.29007/jgkw
Steen, A., Wisniewski, M., Schurr, H., Benzmüller, C.: Capability discovery for automated reasoning systems. In: T. Eiter, D. Sands, G. Sutcliffe, A. Voronkov (eds.) IWIL@LPAR 2017 Workshop and LPAR-21 Short presentations, Maun, Botswana, May 7-12, 2017, Kalpa Publications in Computing, vol. 1. EasyChair (2017). https://doi.org/10.29007/fsv3
Sutcliffe, G.: Semantic derivation verification: techniques and implementation. Int. J. Artif. Intell. Tools 15(6), 1053–1070 (2006). https://doi.org/10.1142/S0218213006003119
Sutcliffe, G.: TPTP, TSTP, CASC, etc. In: V. Diekert, M. Volkov, A. Voronkov (eds.) Proceedings of the 2nd International computer science Symposium in Russia, no. 4649 in lecture notes in computer science, pp. 7–23. Springer (2007)
Sutcliffe, G.: The SZS Ontologies for automated reasoning software. In: LPAR Workshops: knowledge exchange: automated provers and proof assistants, and The 7th International Workshop on the Implementation of Logics (Doha, Qatar), vol. 418, pp. 38–49. CEUR Workshop Proceedings (2008)
Sutcliffe, G.: The TPTP problem library and associated infrastructure - from CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483–502 (2017)
Sutcliffe, G., Benzmüller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formaliz. Reason. 3(1), 1–27 (2010). https://doi.org/10.6092/issn.1972-5787/1710
Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP typed first-order form with arithmetic. In: N. Bjørner, A. Voronkov (eds.) Logic for programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7180, pp. 406–419. Springer (2012). https://doi.org/10.1007/978-3-642-28717-6_32
Vukmirovic, P., Blanchette, J.C., Cruanes, S., Schulz, S.: Extending a brainiac prover to lambda-free higher-order logic. In: T. Vojnar, L. Zhang (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I, Lecture Notes in Computer Science, vol. 11427, pp. 192–210. Springer (2019). https://doi.org/10.1007/978-3-030-17462-0_11
Wand, D.: Superposition: Types and induction. (superposition: types et induction). Ph.D. thesis, Saarland University, Saarbrücken, Germany (2017)
Wisniewski, M., Steen, A., Benzmüller, C.: LeoPARD - A generic platform for the implementation of higher-order reasoners. In: M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, V. Sorge (eds.) Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings, LNCS, vol. 9150, pp. 325–330. Springer (2015). https://doi.org/10.1007/978-3-319-20615-8_22
Wisniewski, M., Steen, A., Benzmüller, C.: TPTP and beyond: Representation of quantified non-classical logics. In: C. Benzmüller, J. Otten (eds.) Proceedings of the 2nd International Workshop Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2016) affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2016)., Coimbra, Portugal, July 1, 2016., CEUR Workshop Proceedings, vol. 1770, pp. 51–65. CEUR-WS.org (2016)
Wisniewski, M., Steen, A., Kern, K., Benzmüller, C.: Effective normalization techniques for HOL. In: N. Olivetti, A. Tiwari (eds.) Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings, LNCS, vol. 9706, pp. 362–370. Springer (2016). https://doi.org/10.1007/978-3-319-40229-1_25