Sutcliffe, Geoff; Desharnais, Martin The 11th IJCAR automated theorem proving system competition – CASC-J11. (English) Zbl 07735787 AI Commun. 36, No. 2, 73-91 (2023). MSC: 68V15 PDFBibTeX XMLCite \textit{G. Sutcliffe} and \textit{M. Desharnais}, AI Commun. 36, No. 2, 73--91 (2023; Zbl 07735787) Full Text: DOI
Leidinger, Hendrik; Weidenbach, Christoph SCL(EQ): SCL for first-order logic with equality. (English) Zbl 07722429 J. Autom. Reasoning 67, No. 3, Paper No. 22, 35 p. (2023). MSC: 68V15 PDFBibTeX XMLCite \textit{H. Leidinger} and \textit{C. Weidenbach}, J. Autom. Reasoning 67, No. 3, Paper No. 22, 35 p. (2023; Zbl 07722429) Full Text: DOI
Bonacina, Maria Paola; Winkler, Sarah Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover. (English) Zbl 07695709 J. Autom. Reasoning 67, No. 1, Paper No. 6, 42 p. (2023). MSC: 68V15 PDFBibTeX XMLCite \textit{M. P. Bonacina} and \textit{S. Winkler}, J. Autom. Reasoning 67, No. 1, Paper No. 6, 42 p. (2023; Zbl 07695709) Full Text: DOI
Leidinger, Hendrik; Weidenbach, Christoph SCL(EQ): SCL for first-order logic with equality. (English) Zbl 07628190 Blanchette, Jasmin (ed.) et al., Automated reasoning. 11th international joint conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13385, 228-247 (2022). MSC: 68V15 PDFBibTeX XMLCite \textit{H. Leidinger} and \textit{C. Weidenbach}, Lect. Notes Comput. Sci. 13385, 228--247 (2022; Zbl 07628190) Full Text: DOI arXiv
Rawson, Michael; Reger, Giles Eliminating models during model elimination. (English) Zbl 07532520 Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 250-265 (2021). MSC: 68V15 PDFBibTeX XMLCite \textit{M. Rawson} and \textit{G. Reger}, Lect. Notes Comput. Sci. 12842, 250--265 (2021; Zbl 07532520) Full Text: DOI
Sutcliffe, Geoff; Desharnais, Martin The CADE-28 automated theorem proving system competition – CASC-28. (English) Zbl 1487.68249 AI Commun. 34, No. 4, 259-276 (2021). MSC: 68V15 PDFBibTeX XMLCite \textit{G. Sutcliffe} and \textit{M. Desharnais}, AI Commun. 34, No. 4, 259--276 (2021; Zbl 1487.68249) Full Text: DOI
Duarte, André; Korovin, Konstantin Implementing superposition in iProver (system description). (English) Zbl 07614685 Peltier, Nicolas (ed.) et al., Automated reasoning. 10th international joint conference, IJCAR 2020, Paris, France, July 1–4, 2020. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12167, 388-397 (2020). MSC: 68V15 PDFBibTeX XMLCite \textit{A. Duarte} and \textit{K. Korovin}, Lect. Notes Comput. Sci. 12167, 388--397 (2020; Zbl 07614685) Full Text: DOI
Bonacina, Maria Paola; Winkler, Sarah SGGS decision procedures. (English) Zbl 07614522 Peltier, Nicolas (ed.) et al., Automated reasoning. 10th international joint conference, IJCAR 2020, Paris, France, July 1–4, 2020. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12166, 356-374 (2020). MSC: 68V15 PDFBibTeX XMLCite \textit{M. P. Bonacina} and \textit{S. Winkler}, Lect. Notes Comput. Sci. 12166, 356--374 (2020; Zbl 07614522) Full Text: DOI
Teucke, Andreas; Weidenbach, Christoph SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment. (English) Zbl 1468.68308 J. Autom. Reasoning 64, No. 3, 611-640 (2020). MSC: 68V15 03B20 03B25 03B35 PDFBibTeX XMLCite \textit{A. Teucke} and \textit{C. Weidenbach}, J. Autom. Reasoning 64, No. 3, 611--640 (2020; Zbl 1468.68308) Full Text: DOI HAL
Schulz, Stephan; Cruanes, Simon; Vukmirović, Petar Faster, higher, stronger: E 2.3. (English) Zbl 07178994 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, 495-507 (2019). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{S. Schulz} et al., Lect. Notes Comput. Sci. 11716, 495--507 (2019; Zbl 07178994) Full Text: DOI HAL
Fiori, Alberto; Weidenbach, Christoph SCL clause learning from simple models. (English) Zbl 07178979 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, 233-249 (2019). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{A. Fiori} and \textit{C. Weidenbach}, Lect. Notes Comput. Sci. 11716, 233--249 (2019; Zbl 07178979) Full Text: DOI HAL
Pulina, Luca; Seidl, Martina The 2016 and 2017 QBF solvers evaluations (QBFEVAL’16 and QBFEVAL’17). (English) Zbl 1478.68332 Artif. Intell. 274, 224-248 (2019). MSC: 68T20 68T27 68V15 PDFBibTeX XMLCite \textit{L. Pulina} and \textit{M. Seidl}, Artif. Intell. 274, 224--248 (2019; Zbl 1478.68332) Full Text: DOI
Slaney, John; Woltzenlogel Paleo, Bruno Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning. (English) Zbl 1425.68379 J. Autom. Reasoning 60, No. 2, 133-156 (2018). MSC: 68T15 03B35 68T20 PDFBibTeX XMLCite \textit{J. Slaney} and \textit{B. Woltzenlogel Paleo}, J. Autom. Reasoning 60, No. 2, 133--156 (2018; Zbl 1425.68379) Full Text: DOI arXiv
Bonacina, Maria Paola; Plaisted, David A. Semantically-guided goal-sensitive reasoning: inference system and completeness. (English) Zbl 1437.68189 J. Autom. Reasoning 59, No. 2, 165-218 (2017). MSC: 68V15 03B35 PDFBibTeX XMLCite \textit{M. P. Bonacina} and \textit{D. A. Plaisted}, J. Autom. Reasoning 59, No. 2, 165--218 (2017; Zbl 1437.68189) Full Text: DOI
Khasidashvili, Zurab; Korovin, Konstantin Predicate elimination for preprocessing in first-order theorem proving. (English) Zbl 1475.68441 Creignou, Nadia (ed.) et al., Theory and applications of satisfiability testing – SAT 2016. 19th international conference, Bordeaux, France, July 5–8, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9710, 361-372 (2016). MSC: 68V15 PDFBibTeX XMLCite \textit{Z. Khasidashvili} and \textit{K. Korovin}, Lect. Notes Comput. Sci. 9710, 361--372 (2016; Zbl 1475.68441) Full Text: DOI
Bonacina, Maria Paola; Plaisted, David A. Semantically-guided goal-sensitive reasoning: model representation. (English) Zbl 1356.68180 J. Autom. Reasoning 56, No. 2, 113-141 (2016). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{M. P. Bonacina} and \textit{D. A. Plaisted}, J. Autom. Reasoning 56, No. 2, 113--141 (2016; Zbl 1356.68180) Full Text: DOI
Teucke, Andreas; Weidenbach, Christoph First-order logic theorem proving and model building via approximation and instantiation. (English) Zbl 1471.03020 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, 85-100 (2015). MSC: 03B35 03B25 PDFBibTeX XMLCite \textit{A. Teucke} and \textit{C. Weidenbach}, Lect. Notes Comput. Sci. 9322, 85--100 (2015; Zbl 1471.03020) Full Text: DOI arXiv
Alagi, Gábor; Weidenbach, Christoph NRCL – a model building approach to the Bernays-Schönfinkel fragment. (English) Zbl 1471.03013 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, 69-84 (2015). MSC: 03B35 03B25 PDFBibTeX XMLCite \textit{G. Alagi} and \textit{C. Weidenbach}, Lect. Notes Comput. Sci. 9322, 69--84 (2015; Zbl 1471.03013) Full Text: DOI arXiv Link
Sato, Haruhiko; Winkler, Sarah Encoding dependency pair techniques and control strategies for maximal completion. (English) Zbl 1465.68126 Felty, Amy P. (ed.) et al., Automated deduction – CADE-25. 25th international conference on automated deduction, Berlin, Germany, August 1–7, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9195, 152-162 (2015). MSC: 68Q42 68V15 PDFBibTeX XMLCite \textit{H. Sato} and \textit{S. Winkler}, Lect. Notes Comput. Sci. 9195, 152--162 (2015; Zbl 1465.68126) Full Text: DOI