Avigad, Jeremy; Baek, Seulkee; Bentkamp, Alexander; Heule, Marijn; Nawrocki, Wojciech An impossible asylum. (English) Zbl 07684392 Am. Math. Mon. 130, No. 5, 446-453 (2023). MSC: 03-01 03B35 68V15 PDF BibTeX XML Cite \textit{J. Avigad} et al., Am. Math. Mon. 130, No. 5, 446--453 (2023; Zbl 07684392) Full Text: DOI arXiv OpenURL
Banković, Milan; Drecun, Ivan; Marić, Filip A proof system for graph (non)-isomorphism verification. (English) Zbl 07667099 Log. Methods Comput. Sci. 19, No. 1, Paper No. 9, 40 p. (2023). MSC: 03B70 68-XX PDF BibTeX XML Cite \textit{M. Banković} et al., Log. Methods Comput. Sci. 19, No. 1, Paper No. 9, 40 p. (2023; Zbl 07667099) Full Text: DOI arXiv OpenURL
Rampersad, Narad Prefixes of the Fibonacci word that end with a cube. (English) Zbl 07652650 C. R., Math., Acad. Sci. Paris 361, 323-330 (2023). Reviewer: Anna Frid (Marseille) MSC: 68R15 68V15 68V20 PDF BibTeX XML Cite \textit{N. Rampersad}, C. R., Math., Acad. Sci. Paris 361, 323--330 (2023; Zbl 07652650) Full Text: DOI arXiv OpenURL
Roßkopf, Simon; Nipkow, Tobias A formalization and proof checker for Isabelle’s metalogic. (English) Zbl 1502.68353 J. Autom. Reasoning 67, No. 1, Paper No. 1, 21 p. (2023). MSC: 68V15 03B35 68V20 PDF BibTeX XML Cite \textit{S. Roßkopf} and \textit{T. Nipkow}, J. Autom. Reasoning 67, No. 1, Paper No. 1, 21 p. (2023; Zbl 1502.68353) Full Text: DOI OpenURL
Hetzl, Stefan; Vierling, Jannik Induction and Skolemization in saturation theorem proving. (English) Zbl 07601550 Ann. Pure Appl. Logic 174, No. 1, Article ID 103167, 37 p. (2023). MSC: 03F30 68V15 03B70 03H15 PDF BibTeX XML Cite \textit{S. Hetzl} and \textit{J. Vierling}, Ann. Pure Appl. Logic 174, No. 1, Article ID 103167, 37 p. (2023; Zbl 07601550) Full Text: DOI arXiv OpenURL
Shallit, Jeffrey The logical approach to automatic sequences. Exploring combinatorics on words with Walnut. (English) Zbl 07565707 London Mathematical Society Lecture Note Series 482. Cambridge: Cambridge University Press (ISBN 978-1-108-74524-6/pbk; 978-1-108-77526-7/ebook). xvi, 358 p. (2023). MSC: 68-02 11B85 68R15 68V15 PDF BibTeX XML Cite \textit{J. Shallit}, The logical approach to automatic sequences. Exploring combinatorics on words with Walnut. Cambridge: Cambridge University Press (2023; Zbl 07565707) Full Text: DOI OpenURL
Hemaspaandra, Edith; Narváez, David E. Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification. (English) Zbl 07691303 Buzzard, Kevin (ed.) et al., Intelligent computer mathematics. 15th international conference, CICM 2022, Tbilisi, Georgia, September 19–23, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13467, 241-255 (2022). MSC: 68Vxx PDF BibTeX XML Cite \textit{E. Hemaspaandra} and \textit{D. E. Narváez}, Lect. Notes Comput. Sci. 13467, 241--255 (2022; Zbl 07691303) Full Text: DOI OpenURL
Kurpiewski, Damian; Jamroga, Wojciech; Maśko, Łukasz; Mikulski, Łukasz; Pazderski, Witold; Penczek, Wojciech; Sidoruk, Teofil Verification of multi-agent properties in electronic voting: a case study. (English) Zbl 07668114 Fernández-Duque, David (ed.) et al., Advances in modal logic. Vol. 14. Proceedings of the 14th conference (AiML 2022), Rennes, France, August 22–25, 2022. London: College Publications. 531-555 (2022). MSC: 03-XX 68V15 03B70 68T42 PDF BibTeX XML Cite \textit{D. Kurpiewski} et al., in: Advances in modal logic. Vol. 14. Proceedings of the 14th conference (AiML 2022), Rennes, France, August 22--25, 2022. London: College Publications. 531--555 (2022; Zbl 07668114) OpenURL
Goré, Rajeev; Shillito, Ian Direct elimination of additive-cuts in GL4ip: verified and extracted. (English) Zbl 07668109 Fernández-Duque, David (ed.) et al., Advances in modal logic. Vol. 14. Proceedings of the 14th conference (AiML 2022), Rennes, France, August 22–25, 2022. London: College Publications. 429-449 (2022). MSC: 03F45 03B35 03F05 PDF BibTeX XML Cite \textit{R. Goré} and \textit{I. Shillito}, in: Advances in modal logic. Vol. 14. Proceedings of the 14th conference (AiML 2022), Rennes, France, August 22--25, 2022. London: College Publications. 429--449 (2022; Zbl 07668109) OpenURL
Papacchini, Fabio; Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare Correction to: “Local is best: efficient reductions to modal logic K”. (English) Zbl 07632101 J. Autom. Reasoning 66, No. 4, 1099 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{F. Papacchini} et al., J. Autom. Reasoning 66, No. 4, 1099 (2022; Zbl 07632101) Full Text: DOI OpenURL
Divasón, Jose; Thiemann, René Correction to: “A formalization of the Smith normal form in higher-order logic”. (English) Zbl 07632100 J. Autom. Reasoning 66, No. 4, 1097 (2022). MSC: 68V15 13F10 15A21 15B33 68V20 PDF BibTeX XML Cite \textit{J. Divasón} and \textit{R. Thiemann}, J. Autom. Reasoning 66, No. 4, 1097 (2022; Zbl 07632100) Full Text: DOI OpenURL
Divasón, Jose; Thiemann, René A formalization of the Smith normal form in higher-order logic. (English) Zbl 07632099 J. Autom. Reasoning 66, No. 4, 1065-1095 (2022); correction ibid. 66, No. 4, 1097 (2022). Reviewer: Filippo Nuccio (Saint-Étienne) MSC: 68V15 13F10 15A21 15B33 68V20 PDF BibTeX XML Cite \textit{J. Divasón} and \textit{R. Thiemann}, J. Autom. Reasoning 66, No. 4, 1065--1095 (2022; Zbl 07632099) Full Text: DOI OpenURL
Schmoetten, Richard; Palmer, Jake E.; Fleuriot, Jacques D. Towards formalising Schutz’ axioms for Minkowski spacetime in Isabelle/HOL. (English) Zbl 07632096 J. Autom. Reasoning 66, No. 4, 953-988 (2022). MSC: 68V15 68V20 83A05 PDF BibTeX XML Cite \textit{R. Schmoetten} et al., J. Autom. Reasoning 66, No. 4, 953--988 (2022; Zbl 07632096) Full Text: DOI arXiv OpenURL
Soldevila, Mallku; Ziliani, Beta; Silvestre, Bruno From specification to testing: semantics engineering for Lua 5.2. (English) Zbl 07632095 J. Autom. Reasoning 66, No. 4, 905-952 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{M. Soldevila} et al., J. Autom. Reasoning 66, No. 4, 905--952 (2022; Zbl 07632095) Full Text: DOI OpenURL
Macedo, Nuno; Brunel, Julien; Chemouil, David; Cunha, Alcino Pardinus: a temporal relational model finder. (English) Zbl 07632094 J. Autom. Reasoning 66, No. 4, 861-904 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{N. Macedo} et al., J. Autom. Reasoning 66, No. 4, 861--904 (2022; Zbl 07632094) Full Text: DOI OpenURL
de Champeaux, Dennis Faster linear unification algorithm. (English) Zbl 07632093 J. Autom. Reasoning 66, No. 4, 845-860 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{D. de Champeaux}, J. Autom. Reasoning 66, No. 4, 845--860 (2022; Zbl 07632093) Full Text: DOI OpenURL
Meyers, Joshua; Spivak, David I.; Wisnesky, Ryan Fast left Kan extensions using the chase. (English) Zbl 07632092 J. Autom. Reasoning 66, No. 4, 805-844 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{J. Meyers} et al., J. Autom. Reasoning 66, No. 4, 805--844 (2022; Zbl 07632092) Full Text: DOI arXiv OpenURL
Pearce, David J.; Utting, Mark; Groves, Lindsay Verifying Whiley programs with Boogie. (English) Zbl 07632091 J. Autom. Reasoning 66, No. 4, 747-803 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{D. J. Pearce} et al., J. Autom. Reasoning 66, No. 4, 747--803 (2022; Zbl 07632091) Full Text: DOI OpenURL
Janičić, Predrag; Narboux, Julien Theorem proving as constraint solving with coherent logic. (English) Zbl 07632090 J. Autom. Reasoning 66, No. 4, 689-746 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{P. Janičić} and \textit{J. Narboux}, J. Autom. Reasoning 66, No. 4, 689--746 (2022; Zbl 07632090) Full Text: DOI OpenURL
Papacchini, Fabio; Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare Local is best: efficient reductions to modal logic K. (English) Zbl 07632088 J. Autom. Reasoning 66, No. 4, 639-666 (2022); correction ibid. 66, No. 4, 1099 (2022). MSC: 68V15 03B35 03B45 PDF BibTeX XML Cite \textit{F. Papacchini} et al., J. Autom. Reasoning 66, No. 4, 639--666 (2022; Zbl 07632088) Full Text: DOI OpenURL
Lochbihler, Andreas A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory. (English) Zbl 07632086 J. Autom. Reasoning 66, No. 4, 585-610 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{A. Lochbihler}, J. Autom. Reasoning 66, No. 4, 585--610 (2022; Zbl 07632086) Full Text: DOI OpenURL
Tourret, Sophie; Weidenbach, Christoph A posthumous contribution by Larry Wos: excerpts from an unpublished column. (English) Zbl 07632085 J. Autom. Reasoning 66, No. 4, 575-584 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{S. Tourret} and \textit{C. Weidenbach}, J. Autom. Reasoning 66, No. 4, 575--584 (2022; Zbl 07632085) Full Text: DOI OpenURL
Veroff, Robert A Wos Challenge Met. (English) Zbl 07632084 J. Autom. Reasoning 66, No. 4, 565-574 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{R. Veroff}, J. Autom. Reasoning 66, No. 4, 565--574 (2022; Zbl 07632084) Full Text: DOI OpenURL
Vukmirović, Petar; Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Nummelin, Visa; Tourret, Sophie Making higher-order superposition work. (English) Zbl 07632083 J. Autom. Reasoning 66, No. 4, 541-564 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{P. Vukmirović} et al., J. Autom. Reasoning 66, No. 4, 541--564 (2022; Zbl 07632083) Full Text: DOI OpenURL
Waldmann, Uwe; Tourret, Sophie; Robillard, Simon; Blanchette, Jasmin A comprehensive framework for saturation theorem proving. (English) Zbl 07632082 J. Autom. Reasoning 66, No. 4, 499-539 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{U. Waldmann} et al., J. Autom. Reasoning 66, No. 4, 499--539 (2022; Zbl 07632082) Full Text: DOI OpenURL
Bonacina, Maria Paola Set of support, demodulation, paramodulation: a historical perspective. (English) Zbl 07632081 J. Autom. Reasoning 66, No. 4, 463-497 (2022). MSC: 68V15 68-03 PDF BibTeX XML Cite \textit{M. P. Bonacina}, J. Autom. Reasoning 66, No. 4, 463--497 (2022; Zbl 07632081) Full Text: DOI OpenURL
Beeson, Michael; Bonacina, Maria Paola; Kinyon, Michael; Sutcliffe, Geoff Larry Wos: visions of automated reasoning. (English) Zbl 07632080 J. Autom. Reasoning 66, No. 4, 439-461 (2022). MSC: 68-03 01A70 68V15 PDF BibTeX XML Cite \textit{M. Beeson} et al., J. Autom. Reasoning 66, No. 4, 439--461 (2022; Zbl 07632080) Full Text: DOI OpenURL
Bonacina, Maria Paola (ed.) Six decades of automated reasoning: papers in memory of Larry Wos. Foreword. (English) Zbl 07632079 J. Autom. Reasoning 66, No. 4, 437-438 (2022). MSC: 68-06 01A70 68-03 68V15 00B15 PDF BibTeX XML Cite \textit{M. P. Bonacina} (ed.), J. Autom. Reasoning 66, No. 4, 437--438 (2022; Zbl 07632079) Full Text: DOI OpenURL
Ognjanović, Zoran; Perović, Aleksandar; Ilić-Stepić, Angelina Tableau for the logic ILP. (English) Zbl 07629112 Publ. Inst. Math., Nouv. Sér. 112(126), 1-11 (2022). MSC: 03B20 03B48 68V15 PDF BibTeX XML Cite \textit{Z. Ognjanović} et al., Publ. Inst. Math., Nouv. Sér. 112(126), 1--11 (2022; Zbl 07629112) Full Text: DOI OpenURL
Lommen, Nils; Meyer, Fabian; Giesl, Jürgen Automatic complexity analysis of integer programs via triangular weakly non-linear loops. (English) Zbl 07628219 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, 734-754 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{N. Lommen} et al., Lect. Notes Comput. Sci. 13385, 734--754 (2022; Zbl 07628219) Full Text: DOI arXiv OpenURL
Gallicchio, James; Tan, Yong Kiam; Mitsch, Stefan; Platzer, André Implicit definitions with differential equations for KeYmaera X (system description). (English) Zbl 07628218 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, 723-733 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{J. Gallicchio} et al., Lect. Notes Comput. Sci. 13385, 723--733 (2022; Zbl 07628218) Full Text: DOI arXiv OpenURL
Frohn, Florian; Giesl, Jürgen Proving non-termination and lower runtime bounds with LoAT (system description). (English) Zbl 07628217 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, 712-722 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{F. Frohn} and \textit{J. Giesl}, Lect. Notes Comput. Sci. 13385, 712--722 (2022; Zbl 07628217) Full Text: DOI OpenURL
Bozga, Marius; Bueri, Lucas; Iosif, Radu Decision problems in a logic for reasoning about reconfigurable distributed systems. (English) Zbl 07628216 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, 691-711 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{M. Bozga} et al., Lect. Notes Comput. Sci. 13385, 691--711 (2022; Zbl 07628216) Full Text: DOI arXiv OpenURL
Akshay, S.; Chakraborty, Supratik; Pal, Debtanu On eventual non-negativity and positivity for the weighted sum of powers of matrices. (English) Zbl 07628215 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, 671-690 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{S. Akshay} et al., Lect. Notes Comput. Sci. 13385, 671--690 (2022; Zbl 07628215) Full Text: DOI arXiv OpenURL
Suda, Martin Vampire getting noisy: Will random bits help conquer chaos? (system description). (English) Zbl 07628214 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, 659-667 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{M. Suda}, Lect. Notes Comput. Sci. 13385, 659--667 (2022; Zbl 07628214) Full Text: DOI OpenURL
Greati, Vitor; Marcos, João Finite two-dimensional proof systems for non-finitely axiomatizable logics. (English) Zbl 07628213 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, 640-658 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{V. Greati} and \textit{J. Marcos}, Lect. Notes Comput. Sci. 13385, 640--658 (2022; Zbl 07628213) Full Text: DOI arXiv OpenURL
Popescu, Andrei Rensets and renaming-based recursion for syntax with bindings. (English) Zbl 07628212 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, 618-639 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{A. Popescu}, Lect. Notes Comput. Sci. 13385, 618--639 (2022; Zbl 07628212) Full Text: DOI arXiv OpenURL
Piepenbrock, Jelle; Heskes, Tom; Janota, Mikoláš; Urban, Josef Guiding an automated theorem prover with neural rewriting. (English) Zbl 07628211 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, 597-617 (2022). Reviewer: Truong Hoang Le (Hanoi) MSC: 68V15 20N05 68T05 PDF BibTeX XML Cite \textit{J. Piepenbrock} et al., Lect. Notes Comput. Sci. 13385, 597--617 (2022; Zbl 07628211) Full Text: DOI OpenURL
Kutsia, Temur; Pau, Cleo A framework for approximate generalization in quantitative theories. (English) Zbl 07628210 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, 578-596 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{T. Kutsia} and \textit{C. Pau}, Lect. Notes Comput. Sci. 13385, 578--596 (2022; Zbl 07628210) Full Text: DOI OpenURL
Mangla, Chaitanya; Holden, Sean B.; Paulson, Lawrence C. Bayesian ranking for strategy scheduling in automated theorem provers. (English) Zbl 07628209 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, 559-577 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{C. Mangla} et al., Lect. Notes Comput. Sci. 13385, 559--577 (2022; Zbl 07628209) Full Text: DOI OpenURL
Indrzejczak, Andrzej Leśniewski’s ontology – proof-theoretic characterization. (English) Zbl 07628208 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, 541-558 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{A. Indrzejczak}, Lect. Notes Comput. Sci. 13385, 541--558 (2022; Zbl 07628208) Full Text: DOI OpenURL
Durán, Francisco; Eker, Steven; Escobar, Santiago; Martí-Oliet, Narciso; Meseguer, José; Rubio, Rubén; Talcott, Carolyn Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description). (English) Zbl 07628207 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, 529-540 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{F. Durán} et al., Lect. Notes Comput. Sci. 13385, 529--540 (2022; Zbl 07628207) Full Text: DOI OpenURL
Das, Anupam; Girlando, Marianna Cyclic proofs, hypersequents, and transitive closure logic. (English) Zbl 07628206 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, 509-528 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{A. Das} and \textit{M. Girlando}, Lect. Notes Comput. Sci. 13385, 509--528 (2022; Zbl 07628206) Full Text: DOI arXiv OpenURL
Nalon, Cláudia; Hustadt, Ullrich; Papacchini, Fabio; Dixon, Clare Local reductions for the modal cube. (English) Zbl 07628205 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, 486-505 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{C. Nalon} et al., Lect. Notes Comput. Sci. 13385, 486--505 (2022; Zbl 07628205) Full Text: DOI OpenURL
Lahav, Ori; Zohar, Yoni Effective semantics for the modal logics K and KT via non-deterministic matrices. (English) Zbl 07628204 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, 468-485 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{O. Lahav} and \textit{Y. Zohar}, Lect. Notes Comput. Sci. 13385, 468--485 (2022; Zbl 07628204) Full Text: DOI OpenURL
Blaisdell, Eben; Kanovich, Max; Kuznetsov, Stepan L.; Pimentel, Elaine; Scedrov, Andre Non-associative, non-commutative multi-modal linear logic. (English) Zbl 07628203 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, 449-467 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{E. Blaisdell} et al., Lect. Notes Comput. Sci. 13385, 449--467 (2022; Zbl 07628203) Full Text: DOI OpenURL
Bílková, Marta; Frittella, Sabine; Kozhemiachenko, Daniil Paraconsistent Gödel modal logic. (English) Zbl 07628202 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, 429-448 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{M. Bílková} et al., Lect. Notes Comput. Sci. 13385, 429--448 (2022; Zbl 07628202) Full Text: DOI arXiv OpenURL
Sochański, Michał; Leszczyńska-Jasion, Dorota; Chlebowski, Szymon; Tomczyk, Agata; Jukiewicz, Marcin Synthetic tableaux: Minimal tableau search heuristics. (English) Zbl 07628201 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, 407-425 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{M. Sochański} et al., Lect. Notes Comput. Sci. 13385, 407--425 (2022; Zbl 07628201) Full Text: DOI OpenURL
Matsuzaki, Takuya; Fujita, Tomohiro Formula simplification via invariance detection by algebraically indexed types. (English) Zbl 07628200 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, 388-406 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{T. Matsuzaki} and \textit{T. Fujita}, Lect. Notes Comput. Sci. 13385, 388--406 (2022; Zbl 07628200) Full Text: DOI OpenURL
Holub, Štěpán; Raška, Martin; Starosta, Štěpán Binary codes that do not preserve primitivity. (English) Zbl 07628199 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, 369-387 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{Š. Holub} et al., Lect. Notes Comput. Sci. 13385, 369--387 (2022; Zbl 07628199) Full Text: DOI arXiv OpenURL
Cailler, Julie; Rosain, Johann; Delahaye, David; Robillard, Simon; Bouziane, Hinde Lilia Goéland: a concurrent tableau-based theorem prover (system description). (English) Zbl 07628198 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, 359-368 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{J. Cailler} et al., Lect. Notes Comput. Sci. 13385, 359--368 (2022; Zbl 07628198) Full Text: DOI OpenURL
Brown, Chad E.; Kaliszyk, Cezary Lash 1.0 (system description). (English) Zbl 07628197 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, 350-358 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{C. E. Brown} and \textit{C. Kaliszyk}, Lect. Notes Comput. Sci. 13385, 350--358 (2022; Zbl 07628197) Full Text: DOI arXiv OpenURL
Bernreiter, Michael; Lolic, Anela; Maly, Jan; Woltran, Stefan Sequent calculi for choice logics. (English) Zbl 07628196 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, 331-349 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{M. Bernreiter} et al., Lect. Notes Comput. Sci. 13385, 331--349 (2022; Zbl 07628196) Full Text: DOI OpenURL
Yang, Hui; Ma, Yue; Bidoit, Nicole Hypergraph-based inference rules for computing \(\mathcal{EL}^+\)-ontology justifications. (English) Zbl 07628195 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, 310-328 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{H. Yang} et al., Lect. Notes Comput. Sci. 13385, 310--328 (2022; Zbl 07628195) Full Text: DOI OpenURL
Tammet, Tanel; Draheim, Dirk; Järv, Priit GK: implementing full first order default logic for commonsense reasoning (system description). (English) Zbl 07628194 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, 300-309 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{T. Tammet} et al., Lect. Notes Comput. Sci. 13385, 300--309 (2022; Zbl 07628194) Full Text: DOI OpenURL
Cauli, Claudia; Ortiz, Magdalena; Piterman, Nir Actions over core-closed knowledge bases. (English) Zbl 07628193 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, 281-299 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{C. Cauli} et al., Lect. Notes Comput. Sci. 13385, 281--299 (2022; Zbl 07628193) Full Text: DOI arXiv OpenURL
Alrabbaa, Christian; Baader, Franz; Borgwardt, Stefan; Dachselt, Raimund; Koopmann, Patrick; Méndez, Julián Evonne: interactive proof visualization for description logics (system description). (English) Zbl 07628192 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, 271-280 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{C. Alrabbaa} et al., Lect. Notes Comput. Sci. 13385, 271--280 (2022; Zbl 07628192) Full Text: DOI arXiv OpenURL
Yamada, Akihisa Term orderings for non-reachability of (conditional) rewriting. (English) Zbl 07628191 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, 248-267 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{A. Yamada}, Lect. Notes Comput. Sci. 13385, 248--267 (2022; Zbl 07628191) Full Text: DOI OpenURL
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 PDF BibTeX XML Cite \textit{H. Leidinger} and \textit{C. Weidenbach}, Lect. Notes Comput. Sci. 13385, 228--247 (2022; Zbl 07628190) Full Text: DOI arXiv OpenURL
Haifani, Fajar; Weidenbach, Christoph Semantic relevance. (English) Zbl 07628189 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, 208-227 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{F. Haifani} and \textit{C. Weidenbach}, Lect. Notes Comput. Sci. 13385, 208--227 (2022; Zbl 07628189) Full Text: DOI OpenURL
Haifani, Fajar; Koopmann, Patrick; Tourret, Sophie; Weidenbach, Christoph Connection-minimal abduction in \(\mathcal{EL}\) via translation to FOL. (English) Zbl 07628188 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, 188-207 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{F. Haifani} et al., Lect. Notes Comput. Sci. 13385, 188--207 (2022; Zbl 07628188) Full Text: DOI arXiv OpenURL
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 PDF BibTeX XML Cite \textit{A. Duarte} and \textit{K. Korovin}, Lect. Notes Comput. Sci. 13385, 169--187 (2022; Zbl 07628187) Full Text: DOI OpenURL
Bromberger, Martin; Leutgeb, Lorenz; Weidenbach, Christoph An efficient subsumption test pipeline for BS(LRA) clauses. (English) Zbl 07628186 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, 147-168 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{M. Bromberger} et al., Lect. Notes Comput. Sci. 13385, 147--168 (2022; Zbl 07628186) Full Text: DOI OpenURL
Sheng, Ying; Nötzli, Andres; Reynolds, Andrew; Zohar, Yoni; Dill, David; Grieskamp, Wolfgang; Park, Junkil; Qadeer, Shaz; Barrett, Clark; Tinelli, Cesare Reasoning about vectors using an SMT theory of sequences. (English) Zbl 07628185 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, 125-143 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{Y. Sheng} et al., Lect. Notes Comput. Sci. 13385, 125--143 (2022; Zbl 07628185) Full Text: DOI arXiv OpenURL
Reeves, Joseph E.; Heule, Marijn J. H.; Bryant, Randal E. Preprocessing of propagation redundant clauses. (English) Zbl 07628184 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, 106-124 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{J. E. Reeves} et al., Lect. Notes Comput. Sci. 13385, 106--124 (2022; Zbl 07628184) Full Text: DOI OpenURL
Kremer, Gereon; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare Cooperating techniques for solving nonlinear real arithmetic in the cvc5 SMT solver (system description). (English) Zbl 07628183 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, 95-105 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{G. Kremer} et al., Lect. Notes Comput. Sci. 13385, 95--105 (2022; Zbl 07628183) Full Text: DOI OpenURL
Ihalainen, Hannes; Berg, Jeremias; Järvisalo, Matti Clause redundancy and preprocessing in maximum satisfiability. (English) Zbl 07628182 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, 75-94 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{H. Ihalainen} et al., Lect. Notes Comput. Sci. 13385, 75--94 (2022; Zbl 07628182) Full Text: DOI OpenURL
Fiorentini, Camillo; Ferrari, Mauro SAT-based proof search in intermediate propositional logics. (English) Zbl 07628181 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, 57-74 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{C. Fiorentini} and \textit{M. Ferrari}, Lect. Notes Comput. Sci. 13385, 57--74 (2022; Zbl 07628181) Full Text: DOI OpenURL
Felli, Paolo; Montali, Marco; Winkler, Sarah CTL* model checking for data-aware dynamic systems with arithmetic. (English) Zbl 07628180 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, 36-56 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{P. Felli} et al., Lect. Notes Comput. Sci. 13385, 36--56 (2022; Zbl 07628180) Full Text: DOI arXiv OpenURL
Barbosa, Haniel; Reynolds, Andrew; Kremer, Gereon; Lachnitt, Hanna; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias; Viswanathan, Arjun; Viteri, Scott; Zohar, Yoni; Tinelli, Cesare; Barrett, Clark Flexible proof production in an industrial-strength SMT solver. (English) Zbl 07628179 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, 15-35 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{H. Barbosa} et al., Lect. Notes Comput. Sci. 13385, 15--35 (2022; Zbl 07628179) Full Text: DOI OpenURL
Dowek, Gilles From the universality of mathematical truth to the interoperability of proof systems. (English) Zbl 07628178 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, 8-11 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{G. Dowek}, Lect. Notes Comput. Sci. 13385, 8--11 (2022; Zbl 07628178) Full Text: DOI OpenURL
Albert, Elvira; Gordillo, Pablo; Hernández-Cerezo, Alejandro; Rodríguez-Núñez, Clara; Rubio, Albert Using automated reasoning techniques for enhancing the efficiency and security of (Ethereum) smart contracts. (English) Zbl 07628177 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, 3-7 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{E. Albert} et al., Lect. Notes Comput. Sci. 13385, 3--7 (2022; Zbl 07628177) Full Text: DOI OpenURL
Danvy, Olivier Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant. (English) Zbl 07620649 J. Funct. Program. 32, Paper No. e13, 27 p. (2022). MSC: 68N18 68V15 PDF BibTeX XML Cite \textit{O. Danvy}, J. Funct. Program. 32, Paper No. e13, 27 p. (2022; Zbl 07620649) Full Text: DOI OpenURL
Commelin, Johan Liquid tensor experiment. (German) Zbl 07606352 Mitt. Dtsch. Math.-Ver. 30, No. 3, 166-170 (2022). MSC: 14-01 68V15 00A09 PDF BibTeX XML Cite \textit{J. Commelin}, Mitt. Dtsch. Math.-Ver. 30, No. 3, 166--170 (2022; Zbl 07606352) Full Text: DOI OpenURL
Calvanese, Diego; Ghilardi, Silvio; Gianola, Alessandro; Montali, Marco; Rivkin, Andrey Combination of uniform interpolants via Beth definability. (English) Zbl 07606344 J. Autom. Reasoning 66, No. 3, 409-435 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{D. Calvanese} et al., J. Autom. Reasoning 66, No. 3, 409--435 (2022; Zbl 07606344) Full Text: DOI OpenURL
Baader, Franz; Rydval, Jakub Using model theory to find decidable and tractable description logics with concrete domains. (English) Zbl 07606343 J. Autom. Reasoning 66, No. 3, 357-407 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{F. Baader} and \textit{J. Rydval}, J. Autom. Reasoning 66, No. 3, 357--407 (2022; Zbl 07606343) Full Text: DOI OpenURL
Sheng, Ying; Zohar, Yoni; Ringeissen, Christophe; Lange, Jane; Fontaine, Pascal; Barrett, Clark Polite combination of algebraic datatypes. (English) Zbl 07606342 J. Autom. Reasoning 66, No. 3, 331-355 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{Y. Sheng} et al., J. Autom. Reasoning 66, No. 3, 331--355 (2022; Zbl 07606342) Full Text: DOI arXiv OpenURL
Baader, Franz; Kapur, Deepak Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols. (English) Zbl 07606341 J. Autom. Reasoning 66, No. 3, 301-329 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{F. Baader} and \textit{D. Kapur}, J. Autom. Reasoning 66, No. 3, 301--329 (2022; Zbl 07606341) Full Text: DOI OpenURL
Brakensiek, Joshua; Heule, Marijn; Mackey, John; Narváez, David The resolution of Keller’s conjecture. (English) Zbl 07606340 J. Autom. Reasoning 66, No. 3, 277-300 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{J. Brakensiek} et al., J. Autom. Reasoning 66, No. 3, 277--300 (2022; Zbl 07606340) Full Text: DOI arXiv OpenURL
Peltier, Nicolas (ed.); Sofronie-Stokkermans, Viorica (ed.) Special issue of selected extended papers of IJCAR 2020. (English) Zbl 07606339 J. Autom. Reasoning 66, No. 3, 275-276 (2022). MSC: 00Bxx 68V15 PDF BibTeX XML Cite \textit{N. Peltier} (ed.) and \textit{V. Sofronie-Stokkermans} (ed.), J. Autom. Reasoning 66, No. 3, 275--276 (2022; Zbl 07606339) Full Text: DOI OpenURL
Shallit, Jeffrey Intertwining of complementary Thue-Morse factors. (English) Zbl 07604030 Australas. J. Comb. 84, Part 3, 419-430 (2022). Reviewer: Anna Frid (Marseille) MSC: 68R15 11B85 68V15 68V20 PDF BibTeX XML Cite \textit{J. Shallit}, Australas. J. Comb. 84, Part 3, 419--430 (2022; Zbl 07604030) Full Text: arXiv Link OpenURL
Löh, Clara Exploring formalisation. A primer in human-readable mathematics in Lean 3 with examples from simplicial topology. (English) Zbl 1496.68006 Surveys and Tutorials in the Applied Mathematical Sciences 11. Cham: Springer (ISBN 978-3-031-14648-0/pbk; 978-3-031-14649-7/ebook). iv, 147 p. (2022). MSC: 68-01 55-08 68V15 68V20 PDF BibTeX XML Cite \textit{C. Löh}, Exploring formalisation. A primer in human-readable mathematics in Lean 3 with examples from simplicial topology. Cham: Springer (2022; Zbl 1496.68006) Full Text: DOI OpenURL
Rampersad, Narad; Shallit, Jeffrey Congruence properties of combinatorial sequences via Walnut and the Rowland-Yassawi-Zeilberger automaton. (English) Zbl 07582306 Electron. J. Comb. 29, No. 3, Research Paper P3.36, 13 p. (2022). MSC: 68R15 68Q45 68V15 PDF BibTeX XML Cite \textit{N. Rampersad} and \textit{J. Shallit}, Electron. J. Comb. 29, No. 3, Research Paper P3.36, 13 p. (2022; Zbl 07582306) Full Text: DOI arXiv OpenURL
Ekici, Burak Formal categorical reasoning. (English) Zbl 07582177 Turk. J. Math. 46, No. 4, 1538-1552 (2022). MSC: 68V15 18C50 PDF BibTeX XML Cite \textit{B. Ekici}, Turk. J. Math. 46, No. 4, 1538--1552 (2022; Zbl 07582177) Full Text: DOI OpenURL
Mull, Nathan; Pang, Shuo; Razborov, Alexander On CDCL-based proof systems with the ordered decision strategy. (English) Zbl 07575639 SIAM J. Comput. 51, No. 4, 1368-1399 (2022). MSC: 03F20 68R07 68V15 PDF BibTeX XML Cite \textit{N. Mull} et al., SIAM J. Comput. 51, No. 4, 1368--1399 (2022; Zbl 07575639) Full Text: DOI OpenURL
Andronick, June (ed.); de Moura, Leonardo (ed.) 13th international conference on interactive theorem proving, ITP 2022, Haifa, Israel, August 7–10, 2022. (English) Zbl 1494.68006 LIPIcs – Leibniz International Proceedings in Informatics 237. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik (ISBN 978-3-95977-252-5). ix, 33 articles, not consecutively paged, electronic only, open access (2022). MSC: 68-06 68V15 00B25 PDF BibTeX XML Cite \textit{J. Andronick} (ed.) and \textit{L. de Moura} (ed.), 13th international conference on interactive theorem proving, ITP 2022, Haifa, Israel, August 7--10, 2022. Wadern: Schloss Dagstuhl -- Leibniz-Zentrum für Informatik (2022; Zbl 1494.68006) Full Text: DOI Link OpenURL
Blanchette, Jasmin (ed.); Kovács, Laura (ed.); Pattinson, Dirk (ed.) Automated reasoning. 11th international joint conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022. Proceedings. (English) Zbl 1499.68012 Lecture Notes in Computer Science 13385. Lecture Notes in Artificial Intelligence. Cham: Springer (ISBN 978-3-031-10768-9/pbk; 978-3-031-10769-6/ebook). xv, 756 p. (2022). MSC: 68-06 68V15 00B25 PDF BibTeX XML Cite \textit{J. Blanchette} (ed.) et al., Automated reasoning. 11th international joint conference, IJCAR 2022, Haifa, Israel, August 8--10, 2022. Proceedings. Cham: Springer (2022; Zbl 1499.68012) Full Text: DOI OpenURL
Browning, Thomas; Lutz, Patrick Formalizing Galois theory. (English) Zbl 07566891 Exp. Math. 31, No. 2, 413-424 (2022). MSC: 68-XX 12-XX PDF BibTeX XML Cite \textit{T. Browning} and \textit{P. Lutz}, Exp. Math. 31, No. 2, 413--424 (2022; Zbl 07566891) Full Text: DOI arXiv OpenURL
Koutsoukou-Argyraki, Angeliki; Li, Wenda; Paulson, Lawrence C. Irrationality and transcendence criteria for infinite series in Isabelle/HOL. (English) Zbl 07566890 Exp. Math. 31, No. 2, 401-412 (2022). Reviewer: Alexandra Shlapentokh (Greenville) MSC: 11-04 11J81 11J68 68V20 03B35 68V35 PDF BibTeX XML Cite \textit{A. Koutsoukou-Argyraki} et al., Exp. Math. 31, No. 2, 401--412 (2022; Zbl 07566890) Full Text: DOI arXiv OpenURL
Džamonja, Mirna; Koutsoukou-Argyraki, Angeliki; Paulson, Lawrence C. Formalizing ordinal partition relations using Isabelle/HOL. (English) Zbl 07566889 Exp. Math. 31, No. 2, 383-400 (2022). Reviewer: Truong Hoang Le (Hanoi) MSC: 03E02 03E05 03E10 03B35 68V20 68V35 PDF BibTeX XML Cite \textit{M. Džamonja} et al., Exp. Math. 31, No. 2, 383--400 (2022; Zbl 07566889) Full Text: DOI arXiv OpenURL
Fiore, Marcelo P.; Pitts, Andrew M.; Steenkamp, S. C. Quotients, inductive types, and quotient inductive types. (English) Zbl 1502.18046 Log. Methods Comput. Sci. 18, No. 2, Paper No. 15, 37 p. (2022). Reviewer: Philippe Malbos (Lyon) MSC: 18N45 03B38 68V15 PDF BibTeX XML Cite \textit{M. P. Fiore} et al., Log. Methods Comput. Sci. 18, No. 2, Paper No. 15, 37 p. (2022; Zbl 1502.18046) Full Text: arXiv Link OpenURL
Geuvers, Herman; Nederpelt, Rob Characteristics of de Bruijn’s early proof checker Automath. (English) Zbl 07556718 Fundam. Inform. 185, No. 4, 313-336 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{H. Geuvers} and \textit{R. Nederpelt}, Fundam. Inform. 185, No. 4, 313--336 (2022; Zbl 07556718) Full Text: DOI arXiv OpenURL
Schmid, Georg Stefan; Kunčak, Viktor Generalized arrays for Stainless frames. (English) Zbl 1498.68172 Finkbeiner, Bernd (ed.) et al., Verification, model checking, and abstract interpretation. 23rd international conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13182, 332-354 (2022). MSC: 68Q60 03B70 68N30 68V15 PDF BibTeX XML Cite \textit{G. S. Schmid} and \textit{V. Kunčak}, Lect. Notes Comput. Sci. 13182, 332--354 (2022; Zbl 1498.68172) Full Text: DOI OpenURL
Kovács, Laura (ed.); Meinke, Karl (ed.) Tests and proofs. 16th international conference, TAP 2022, held as part of STAF 2022, Nantes, France, July 5, 2022. Proceedings. (English) Zbl 1499.68018 Lecture Notes in Computer Science 13361. Cham: Springer (ISBN 978-3-031-09826-0/pbk; 978-3-031-09827-7/ebook). viii, 127 p. (2022). MSC: 68-06 68Q60 68V15 00B25 PDF BibTeX XML Cite \textit{L. Kovács} (ed.) and \textit{K. Meinke} (ed.), Tests and proofs. 16th international conference, TAP 2022, held as part of STAF 2022, Nantes, France, July 5, 2022. Proceedings. Cham: Springer (2022; Zbl 1499.68018) Full Text: DOI OpenURL
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 PDF BibTeX XML Cite \textit{A. Ge-Ernst} et al., Theor. Comput. Sci. 925, 1--24 (2022; Zbl 1489.68394) Full Text: DOI arXiv OpenURL
Sumners, Rob (ed.); Chau, Cuong (ed.) Proceedings of the seventeenth international workshop on the ACL2 theorem prover and its applications, Austin, Texas, USA, May 26–27, 2022. (English) Zbl 1489.68031 Electronic Proceedings in Theoretical Computer Science (EPTCS) 359. Waterloo: Open Publishing Association (OPA). 216 p., electronic only, open access (2022). MSC: 68-06 68V15 68V20 00B25 PDF BibTeX XML Cite \textit{R. Sumners} (ed.) and \textit{C. Chau} (ed.), Proceedings of the seventeenth international workshop on the ACL2 theorem prover and its applications, Austin, Texas, USA, May 26--27, 2022. Waterloo: Open Publishing Association (OPA) (2022; Zbl 1489.68031) Full Text: DOI Link OpenURL
Fici, Gabriele; Shallit, Jeffrey Properties of a class of Toeplitz words. (English) Zbl 1492.68112 Theor. Comput. Sci. 922, 1-12 (2022). Reviewer: Michel Rigo (Liège) MSC: 68R15 11B85 68V15 PDF BibTeX XML Cite \textit{G. Fici} and \textit{J. Shallit}, Theor. Comput. Sci. 922, 1--12 (2022; Zbl 1492.68112) Full Text: DOI arXiv OpenURL
Wojciechowski, Piotr; Subramani, K.; Chandrasekaran, R. Analyzing read-once cutting plane proofs in Horn systems. (English) Zbl 07538896 J. Autom. Reasoning 66, No. 2, 239-274 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{P. Wojciechowski} et al., J. Autom. Reasoning 66, No. 2, 239--274 (2022; Zbl 07538896) Full Text: DOI OpenURL
Lewis, Robert Y.; Wu, Minchao A bi-directional extensible interface between Lean and Mathematica. (English) Zbl 07538895 J. Autom. Reasoning 66, No. 2, 215-238 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{R. Y. Lewis} and \textit{M. Wu}, J. Autom. Reasoning 66, No. 2, 215--238 (2022; Zbl 07538895) Full Text: DOI arXiv OpenURL
Boldo, Sylvie; Clément, François; Faissole, Florian; Martin, Vincent; Mayero, Micaela A Coq formalization of Lebesgue integration of nonnegative functions. (English) Zbl 07538894 J. Autom. Reasoning 66, No. 2, 175-213 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{S. Boldo} et al., J. Autom. Reasoning 66, No. 2, 175--213 (2022; Zbl 07538894) Full Text: DOI arXiv OpenURL