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
Janičić, Predrag; Narboux, Julien Theorem proving as constraint solving with coherent logic. (English) Zbl 1511.68316 J. Autom. Reasoning 66, No. 4, 689-746 (2022). MSC: 68V15 PDFBibTeX XMLCite \textit{P. Janičić} and \textit{J. Narboux}, J. Autom. Reasoning 66, No. 4, 689--746 (2022; Zbl 1511.68316) Full Text: DOI
Tourret, Sophie; Weidenbach, Christoph A posthumous contribution by Larry Wos: excerpts from an unpublished column. (English) Zbl 1512.68429 J. Autom. Reasoning 66, No. 4, 575-584 (2022). MSC: 68V15 68-03 PDFBibTeX XMLCite \textit{S. Tourret} and \textit{C. Weidenbach}, J. Autom. Reasoning 66, No. 4, 575--584 (2022; Zbl 1512.68429) Full Text: DOI
Waldmann, Uwe; Tourret, Sophie; Robillard, Simon; Blanchette, Jasmin A comprehensive framework for saturation theorem proving. (English) Zbl 1512.68434 J. Autom. Reasoning 66, No. 4, 499-539 (2022). MSC: 68V15 PDFBibTeX XMLCite \textit{U. Waldmann} et al., J. Autom. Reasoning 66, No. 4, 499--539 (2022; Zbl 1512.68434) Full Text: DOI
Bonacina, Maria Paola Set of support, demodulation, paramodulation: a historical perspective. (English) Zbl 1511.68305 J. Autom. Reasoning 66, No. 4, 463-497 (2022). MSC: 68V15 68-03 PDFBibTeX XMLCite \textit{M. P. Bonacina}, J. Autom. Reasoning 66, No. 4, 463--497 (2022; Zbl 1511.68305) Full Text: DOI
Beeson, Michael; Bonacina, Maria Paola; Kinyon, Michael; Sutcliffe, Geoff Larry Wos: visions of automated reasoning. (English) Zbl 1511.68005 J. Autom. Reasoning 66, No. 4, 439-461 (2022). MSC: 68-03 01A70 68V15 PDFBibTeX XMLCite \textit{M. Beeson} et al., J. Autom. Reasoning 66, No. 4, 439--461 (2022; Zbl 1511.68005) 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
Duarte, André; Korovin, Konstantin Ground joinability and connectedness in the superposition calculus. (English) Zbl 07628187 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, 169-187 (2022). MSC: 68V15 PDFBibTeX XMLCite \textit{A. Duarte} and \textit{K. Korovin}, Lect. Notes Comput. Sci. 13385, 169--187 (2022; Zbl 07628187) Full Text: DOI
Ge-Ernst, Aile; Scholl, Christoph; Síč, Juraj; Wimmer, Ralf Solving dependency quantified Boolean formulas using quantifier localization. (English) Zbl 1489.68394 Theor. Comput. Sci. 925, 1-24 (2022). MSC: 68V15 03B35 PDFBibTeX XMLCite \textit{A. Ge-Ernst} et al., Theor. Comput. Sci. 925, 1--24 (2022; Zbl 1489.68394) Full Text: DOI arXiv
Duarte, André; Korovin, Konstantin AC simplifications and closure redundancies in the superposition calculus. (English) Zbl 07532517 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, 200-217 (2021). MSC: 68V15 PDFBibTeX XMLCite \textit{A. Duarte} and \textit{K. Korovin}, Lect. Notes Comput. Sci. 12842, 200--217 (2021; Zbl 07532517) Full Text: DOI arXiv
Holden, Edvard K.; Korovin, Konstantin Heterogeneous heuristic optimisation and scheduling for first-order theorem proving. (English) Zbl 1485.68282 Kamareddine, Fairouz (ed.) et al., Intelligent computer mathematics. 14th international conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12833, 107-123 (2021). MSC: 68V15 68T05 68T20 PDFBibTeX XMLCite \textit{E. K. Holden} and \textit{K. Korovin}, Lect. Notes Comput. Sci. 12833, 107--123 (2021; Zbl 1485.68282) 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
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
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
Schulz, Stephan; Pease, Adam Teaching automated theorem proving by example: PyRes 1.2 (system description). (English) Zbl 07614667 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, 158-166 (2020). MSC: 68V15 PDFBibTeX XMLCite \textit{S. Schulz} and \textit{A. Pease}, Lect. Notes Comput. Sci. 12167, 158--166 (2020; Zbl 07614667) 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
Burel, Guillaume; Bury, Guillaume; Cauderlier, Raphaël; Delahaye, David; Halmagrand, Pierre; Hermant, Olivier First-order automated reasoning with theories: when deduction modulo theory meets practice. (English) Zbl 1468.68282 J. Autom. Reasoning 64, No. 6, 1001-1050 (2020). MSC: 68V15 03B35 PDFBibTeX XMLCite \textit{G. Burel} et al., J. Autom. Reasoning 64, No. 6, 1001--1050 (2020; Zbl 1468.68282) Full Text: DOI HAL
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 Link
Rawson, Michael; Reger, Giles A neurally-guided, parallel theorem prover. (English) Zbl 1435.68374 Herzig, Andreas (ed.) et al., Frontiers of combining systems. 12th international symposium, FroCoS 2019, London, UK, September 4–6, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11715, 40-56 (2019). MSC: 68V15 PDFBibTeX XMLCite \textit{M. Rawson} and \textit{G. Reger}, Lect. Notes Comput. Sci. 11715, 40--56 (2019; Zbl 1435.68374) Full Text: DOI Link
Rawson, Michael; Reger, Giles Old or heavy? Decaying gracefully with age/weight shapes. (English) Zbl 07178992 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, 462-476 (2019). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{M. Rawson} and \textit{G. Reger}, Lect. Notes Comput. Sci. 11716, 462--476 (2019; Zbl 07178992) Full Text: DOI Link
Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef GRUNGE: a grand unified ATP challenge. (English) Zbl 07178973 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, 123-141 (2019). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{C. E. Brown} et al., Lect. Notes Comput. Sci. 11716, 123--141 (2019; Zbl 07178973) Full Text: DOI arXiv
Lopez Hernandez, Julio Cesar; Korovin, Konstantin An abstraction-refinement framework for reasoning with large theories. (English) Zbl 1511.68326 Galmiche, Didier (ed.) et al., 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. Cham: Springer. Lect. Notes Comput. Sci. 10900, 663-679 (2018). MSC: 68V15 PDFBibTeX XMLCite \textit{J. C. Lopez Hernandez} and \textit{K. Korovin}, Lect. Notes Comput. Sci. 10900, 663--679 (2018; Zbl 1511.68326) Full Text: DOI Link
Charrier, Tristan; Pinchinat, Sophie; Schwarzentruber, François Model checking against arbitrary public announcement logic: a first-order-logic prover approach for the existential fragment. (English) Zbl 1503.68180 Madeira, Alexandre (ed.) et al., Dynamic logic. New trends and applications. First international workshop, DALI 2017, Brasilia, Brazil, September 23–24, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10669, 133-152 (2018). MSC: 68Q60 03B42 68V15 PDFBibTeX XMLCite \textit{T. Charrier} et al., Lect. Notes Comput. Sci. 10669, 133--152 (2018; Zbl 1503.68180) Full Text: DOI HAL
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
Itegulov, Daniyar; Slaney, John; Woltzenlogel Paleo, Bruno Scavenger 0.1: a theorem prover based on conflict resolution. (English) Zbl 1494.68287 de Moura, Leonardo (ed.), Automated deduction – CADE 26. 26th international conference on automated deduction, Gothenburg, Sweden, August 6–11, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10395, 344-356 (2017). MSC: 68V15 PDFBibTeX XMLCite \textit{D. Itegulov} et al., Lect. Notes Comput. Sci. 10395, 344--356 (2017; Zbl 1494.68287) Full Text: DOI arXiv
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
Reger, Giles; Suda, Martin; Voronkov, Andrei Finding finite models in multi-sorted first-order logic. (English) Zbl 1475.68447 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, 323-341 (2016). MSC: 68V15 03C13 68T20 PDFBibTeX XMLCite \textit{G. Reger} et al., Lect. Notes Comput. Sci. 9710, 323--341 (2016; Zbl 1475.68447) Full Text: DOI arXiv
Dowek, Gilles Deduction modulo theory. (English) Zbl 1431.03023 Woltzenlogel Paleo, Bruno (ed.) et al., All about proofs, proofs for all. London: College Publications. Stud. Log. (Lond.) 55, 134-149 (2015). MSC: 03B35 03F07 68V15 PDFBibTeX XMLCite \textit{G. Dowek}, Stud. Log. (Lond.) 55, 134--149 (2015; Zbl 1431.03023) Full Text: arXiv
Schulz, Stephan; Sutcliffe, Geoff Proof generation for saturating first-order theorem provers. (English) Zbl 1431.68124 Woltzenlogel Paleo, Bruno (ed.) et al., All about proofs, proofs for all. London: College Publications. Stud. Log. (Lond.) 55, 45-61 (2015). MSC: 68V15 PDFBibTeX XMLCite \textit{S. Schulz} and \textit{G. Sutcliffe}, Stud. Log. (Lond.) 55, 45--61 (2015; Zbl 1431.68124)
Kaliszyk, Cezary Efficient low-level connection tableaux. (English) Zbl 1471.68311 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, 102-111 (2015). MSC: 68V15 PDFBibTeX XMLCite \textit{C. Kaliszyk}, Lect. Notes Comput. Sci. 9323, 102--111 (2015; Zbl 1471.68311) Full Text: DOI
Saghafi, Salman; Danas, Ryan; Dougherty, Daniel J. Exploring theories with a model-finding assistant. (English) Zbl 1465.68298 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, 434-449 (2015). MSC: 68V15 68Q60 PDFBibTeX XMLCite \textit{S. Saghafi} et al., Lect. Notes Comput. Sci. 9195, 434--449 (2015; Zbl 1465.68298) Full Text: DOI
Ji, Kailiang CTL model checking in deduction modulo. (English) Zbl 1465.68180 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, 295-310 (2015). MSC: 68Q60 03B44 68V15 PDFBibTeX XMLCite \textit{K. Ji}, Lect. Notes Comput. Sci. 9195, 295--310 (2015; Zbl 1465.68180) Full Text: DOI Link
Plaisted, David A. History and prospects for first-order automated deduction. (English) Zbl 1465.03055 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, 3-28 (2015). MSC: 03B35 03-03 68-03 68V15 PDFBibTeX XMLCite \textit{D. A. Plaisted}, Lect. Notes Comput. Sci. 9195, 3--28 (2015; Zbl 1465.03055) Full Text: DOI
Gupta, Ashutosh; Kovács, Laura; Kragl, Bernhard; Voronkov, Andrei Extensional crisis and proving identity. (English) Zbl 1448.68459 Cassez, Franck (ed.) et al., Automated technology for verification and analysis. 12th international symposium, ATVA 2014, Sydney, NSW, Australia, November 3–7, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8837, 185-200 (2014). MSC: 68V15 PDFBibTeX XMLCite \textit{A. Gupta} et al., Lect. Notes Comput. Sci. 8837, 185--200 (2014; Zbl 1448.68459) Full Text: DOI