Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar Superposition for higher-order logic. (English) Zbl 07695713 J. Autom. Reasoning 67, No. 1, Paper No. 10, 54 p. (2023). MSC: 68V15 PDFBibTeX XMLCite \textit{A. Bentkamp} et al., J. Autom. Reasoning 67, No. 1, Paper No. 10, 54 p. (2023; Zbl 07695713) Full Text: DOI
Vukmirović, Petar; Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Nummelin, Visa; Tourret, Sophie Making higher-order superposition work. (English) Zbl 1512.68432 J. Autom. Reasoning 66, No. 4, 541-564 (2022). MSC: 68V15 03B16 PDFBibTeX XMLCite \textit{P. Vukmirović} et al., J. Autom. Reasoning 66, No. 4, 541--564 (2022; Zbl 1512.68432) Full Text: DOI
Dubut, Jérémy; Yamada, Akihisa Fixed points theorems for non-transitive relations. (English) Zbl 07471719 Log. Methods Comput. Sci. 18, No. 1, Paper No. 30, 24 p. (2022). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{J. Dubut} and \textit{A. Yamada}, Log. Methods Comput. Sci. 18, No. 1, Paper No. 30, 24 p. (2022; Zbl 07471719) Full Text: arXiv Link
Ţuţu, Ionuţ; Chiriţă, Claudia Elena; Fiadeiro, José Luiz Dynamic reconfiguration via typed modalities. (English) Zbl 1521.68037 Huisman, Marieke (ed.) et al., Formal methods. 24th international symposium, FM 2021, virtual event, November 20–26, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13047, 599-615 (2021). MSC: 68N30 03B45 PDFBibTeX XMLCite \textit{I. Ţuţu} et al., Lect. Notes Comput. Sci. 13047, 599--615 (2021; Zbl 1521.68037) Full Text: DOI
Vukmirović, Petar; Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Nummelin, Visa; Tourret, Sophie Making higher-order superposition work. (English) Zbl 1512.68431 Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 415-432 (2021). MSC: 68V15 03B16 PDFBibTeX XMLCite \textit{P. Vukmirović} et al., Lect. Notes Comput. Sci. 12699, 415--432 (2021; Zbl 1512.68431) Full Text: DOI
Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe Superposition with lambdas. (English) Zbl 07433023 J. Autom. Reasoning 65, No. 7, 893-940 (2021). MSC: 68V15 PDFBibTeX XMLCite \textit{A. Bentkamp} et al., J. Autom. Reasoning 65, No. 7, 893--940 (2021; Zbl 07433023) Full Text: DOI
Steen, Alexander; Benzmüller, Christoph Extensional higher-order paramodulation in Leo-III. (English) Zbl 1509.68321 J. Autom. Reasoning 65, No. 6, 775-807 (2021). MSC: 68V15 03B16 03B35 03B45 PDFBibTeX XMLCite \textit{A. Steen} and \textit{C. Benzmüller}, J. Autom. Reasoning 65, No. 6, 775--807 (2021; Zbl 1509.68321) Full Text: DOI arXiv
Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Waldmann, Uwe Superposition for lambda-free higher-order logic. (English) Zbl 07350767 Log. Methods Comput. Sci. 17, No. 2, Paper No. 1, 38 p. (2021). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{A. Bentkamp} et al., Log. Methods Comput. Sci. 17, No. 2, Paper No. 1, 38 p. (2021; Zbl 07350767) Full Text: arXiv Link
Fuenmayor, David; Benzmüller, Christoph Computer-supported analysis of arguments in climate engineering. (English) Zbl 1509.68246 Dastani, Mehdi (ed.) et al., Logic and argumentation. Third international conference, CLAR 2020, Hangzhou, China, April 6–9, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12061, 104-115 (2020). MSC: 68T27 03B16 68T30 68V15 68V20 86A08 PDFBibTeX XMLCite \textit{D. Fuenmayor} and \textit{C. Benzmüller}, Lect. Notes Comput. Sci. 12061, 104--115 (2020; Zbl 1509.68246) Full Text: DOI
Tiemens, Lucca; Scott, Dana S.; Benzmüller, Christoph; Benda, Miroslav Computer-supported exploration of a categorical axiomatization of modeloids. (English) Zbl 1509.68328 Fahrenberg, Uli (ed.) et al., Relational and algebraic methods in computer science. 18th international conference, RAMiCS 2020, Palaiseau, France, October 26–29, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12062, 302-317 (2020). MSC: 68V20 03B35 03C07 03C99 18A15 20M18 PDFBibTeX XMLCite \textit{L. Tiemens} et al., Lect. Notes Comput. Sci. 12062, 302--317 (2020; Zbl 1509.68328) Full Text: DOI arXiv
Benzmüller, Christoph; Parent, Xavier; van der Torre, Leendert Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support. (English) Zbl 1493.68286 Artif. Intell. 287, Article ID 103348, 28 p. (2020). MSC: 68T01 03A05 03B16 03B35 03B45 68T27 68T30 68V15 PDFBibTeX XMLCite \textit{C. Benzmüller} et al., Artif. Intell. 287, Article ID 103348, 28 p. (2020; Zbl 1493.68286) Full Text: DOI arXiv
Benzmüller, Christoph; Fuenmayor, David Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel’s ontological argument. (English) Zbl 1461.03021 Bull. Sect. Log., Univ. Łódź, Dep. Log. 49, No. 2, 127-148 (2020). MSC: 03B45 03B35 03-08 PDFBibTeX XMLCite \textit{C. Benzmüller} and \textit{D. Fuenmayor}, Bull. Sect. Log., Univ. Łódź, Dep. Log. 49, No. 2, 127--148 (2020; Zbl 1461.03021) Full Text: DOI arXiv
Benzmüller, Christoph; Scott, Dana S. Automating free logic in HOL, with an experimental application in category theory. (English) Zbl 1434.68639 J. Autom. Reasoning 64, No. 1, 53-72 (2020). MSC: 68V15 03B16 03B35 03B60 18A15 PDFBibTeX XMLCite \textit{C. Benzmüller} and \textit{D. S. Scott}, J. Autom. Reasoning 64, No. 1, 53--72 (2020; Zbl 1434.68639) Full Text: DOI Link
Yamada, Akihisa; Dubut, Jérémy Complete non-orders and fixed points. (English) Zbl 07649979 Harrison, John (ed.) et al., 10th international conference on interactive theorem proving, ITP 2019, September 9–12, 2019, Portland, OR, USA. Proceedings. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 141, Article 30, 16 p. (2019). MSC: 68V20 PDFBibTeX XMLCite \textit{A. Yamada} and \textit{J. Dubut}, LIPIcs -- Leibniz Int. Proc. Inform. 141, Article 30, 16 p. (2019; Zbl 07649979) Full Text: DOI
Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe Superposition with lambdas. (English) Zbl 1471.03014 Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 55-73 (2019). Reviewer: Łukasz Czajka (Dortmund) MSC: 03B35 03B16 03B40 68V15 PDFBibTeX XMLCite \textit{A. Bentkamp} et al., Lect. Notes Comput. Sci. 11716, 55--73 (2019; Zbl 1471.03014) Full Text: DOI arXiv HAL
Jensen, Alexander Birch; Larsen, John Bruntse; Schlichtkrull, Anders; Villadsen, Jørgen Programming and verifying a declarative first-order prover in Isabelle/HOL. (English) Zbl 1462.68214 AI Commun. 31, No. 3, 281-299 (2018). MSC: 68V15 68N18 PDFBibTeX XMLCite \textit{A. B. Jensen} et al., AI Commun. 31, No. 3, 281--299 (2018; Zbl 1462.68214) Full Text: DOI
Benzmüller, Christoph; Parent, Xavier; van der Torre, Leendert A deontic logic reasoning infrastructure. (English) Zbl 1509.68327 Manea, Florin (ed.) et al., Sailing routes in the world of computation. 14th conference on computability in Europe, CiE 2018, Kiel, Germany, July 30 – August 3, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10936, 60-69 (2018). MSC: 68V20 03B16 03B35 03B45 68T27 68T30 PDFBibTeX XMLCite \textit{C. Benzmüller} et al., Lect. Notes Comput. Sci. 10936, 60--69 (2018; Zbl 1509.68327) Full Text: DOI Link
Schlichtkrull, Anders Formalization of the resolution calculus for first-order logic. (English) Zbl 1451.03019 J. Autom. Reasoning 61, No. 1-4, 455-484 (2018). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{A. Schlichtkrull}, J. Autom. Reasoning 61, No. 1--4, 455--484 (2018; Zbl 1451.03019) Full Text: DOI Link
Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy Soundness and completeness proofs by coinductive methods. (English) Zbl 1409.68251 J. Autom. Reasoning 58, No. 1, 149-179 (2017). MSC: 68T15 03B10 03B35 03F03 68Q65 PDFBibTeX XMLCite \textit{J. C. Blanchette} et al., J. Autom. Reasoning 58, No. 1, 149--179 (2017; Zbl 1409.68251) Full Text: DOI
Zhan, Bohua AUTO2, a saturation-based heuristic prover for higher-order logic. (English) Zbl 1478.68439 Blanchette, Jasmin Christian (ed.) et al., Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22–25, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9807, 441-456 (2016). MSC: 68V15 03B16 68V20 PDFBibTeX XMLCite \textit{B. Zhan}, Lect. Notes Comput. Sci. 9807, 441--456 (2016; Zbl 1478.68439) Full Text: DOI arXiv
Benzmüller, Christoph; Scott, Dana Automating free logic in Isabelle/HOL. (English) Zbl 1434.68638 Greuel, Gert-Martin (ed.) et al., Mathematical software – ICMS 2016. 5th international conference, Berlin, Germany, July 11–14, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9725, 43-50 (2016). MSC: 68V15 03B16 03B35 03B60 18A15 PDFBibTeX XMLCite \textit{C. Benzmüller} and \textit{D. Scott}, Lect. Notes Comput. Sci. 9725, 43--50 (2016; Zbl 1434.68638) Full Text: DOI
Guttmann, Walter An algebraic approach to computations with progress. (English) Zbl 1344.68076 J. Log. Algebr. Methods Program. 85, No. 4, 520-539 (2016). MSC: 68Q05 PDFBibTeX XMLCite \textit{W. Guttmann}, J. Log. Algebr. Methods Program. 85, No. 4, 520--539 (2016; Zbl 1344.68076) Full Text: DOI
Sultana, Nik; Benzmüller, Christoph; Paulson, Lawrence C. Proofs and reconstructions. (English) Zbl 1471.68319 Lutz, Carsten (ed.) et al., Frontiers of combining systems. 10th international symposium, FroCoS 2015, Wrocław, Poland, September 21–24, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9322, 256-271 (2015). MSC: 68V15 03B16 PDFBibTeX XMLCite \textit{N. Sultana} et al., Lect. Notes Comput. Sci. 9322, 256--271 (2015; Zbl 1471.68319) Full Text: DOI
Benzmüller, Christoph Invited talk: On a (quite) universal theorem proving approach and its application in metaphysics. (English) Zbl 1471.68302 De Nivelle, Hans (ed.), Automated reasoning with analytic tableaux and related methods. 24th international conference, TABLEAUX 2015, Wrocław, Poland, September 21–24, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9323, 213-220 (2015). MSC: 68V15 03A05 03B16 03B35 PDFBibTeX XMLCite \textit{C. Benzmüller}, Lect. Notes Comput. Sci. 9323, 213--220 (2015; Zbl 1471.68302) Full Text: DOI
Brown, Chad E. Reducing higher-order theorem proving to a sequence of SAT problems. (English) Zbl 1314.68276 J. Autom. Reasoning 51, No. 1, 57-77 (2013). MSC: 68T15 PDFBibTeX XMLCite \textit{C. E. Brown}, J. Autom. Reasoning 51, No. 1, 57--77 (2013; Zbl 1314.68276) Full Text: DOI
Sultana, Nik; Blanchette, Jasmin Christian; Paulson, Lawrence C. LEO-II and Satallax on the Sledgehammer test bench. (English) Zbl 1262.68161 J. Appl. Log. 11, No. 1, 91-102 (2013). MSC: 68T15 PDFBibTeX XMLCite \textit{N. Sultana} et al., J. Appl. Log. 11, No. 1, 91--102 (2013; Zbl 1262.68161) Full Text: DOI
Brown, Chad E. Reducing higher-order theorem proving to a sequence of SAT problems. (English) Zbl 1314.68275 Bjørner, Nikolaj (ed.) et al., Automated deduction – CADE-23. 23rd international conference on automated deduction, Wrocław, Poland, July 31 – August 5, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22437-9/pbk; 978-3-642-22438-6/ebook). Lecture Notes in Computer Science 6803. Lecture Notes in Artificial Intelligence, 147-161 (2011). MSC: 68T15 PDFBibTeX XMLCite \textit{C. E. Brown}, Lect. Notes Comput. Sci. 6803, 147--161 (2011; Zbl 1314.68275) Full Text: DOI