Paulson, Lawrence C. A formalised theorem in the partition calculus. (English) Zbl 07748742 Ann. Pure Appl. Logic 175, No. 1, Article ID 103246, 10 p. (2024). MSC: 03E02 03E10 03B35 68V15 68V20 PDFBibTeX XMLCite \textit{L. C. Paulson}, Ann. Pure Appl. Logic 175, No. 1, Article ID 103246, 10 p. (2024; Zbl 07748742) Full Text: DOI arXiv
Malbos, Philippe; Massacrier, Tanguy; Struth, Georg Single-set cubical categories and their formalisation with a proof assistant. arXiv:2401.10553 Preprint, arXiv:2401.10553 [cs.LO] (2024). MSC: 18N30 68V15 03B35 68Q42 BibTeX Cite \textit{P. Malbos} et al., ``Single-set cubical categories and their formalisation with a proof assistant'', Preprint, arXiv:2401.10553 [cs.LO] (2024) Full Text: arXiv OA License
Corless, Robert M.; Jeffrey, David J.; Shakoori, Azar Teaching linear algebra in a mechanized mathematical environment. (English) Zbl 07810727 Dubois, Catherine (ed.) et al., Intelligent computer mathematics. 16th international conference, CICM 2023, Cambridge, UK, September 5–8, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14101, 113-129 (2023). MSC: 68Vxx PDFBibTeX XMLCite \textit{R. M. Corless} et al., Lect. Notes Comput. Sci. 14101, 113--129 (2023; Zbl 07810727) Full Text: DOI arXiv
Wang, Yuzheng; Leng, Tuo; Zeng, Zhenbing On the maximum of the sum of the distances of four points on the hemisphere. (Chinese. English summary) Zbl 07803016 Chin. Ann. Math., Ser. A 44, No. 4, 409-434 (2023). MSC: 41A10 52C35 68V05 PDFBibTeX XMLCite \textit{Y. Wang} et al., Chin. Ann. Math., Ser. A 44, No. 4, 409--434 (2023; Zbl 07803016) Full Text: DOI
Dudenhefner, Andrej Constructive many-one reduction from the halting problem to semi-unification (extended version). (English) Zbl 07788994 Log. Methods Comput. Sci. 19, No. 4, Paper No. 22, 27 p. (2023). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{A. Dudenhefner}, Log. Methods Comput. Sci. 19, No. 4, Paper No. 22, 27 p. (2023; Zbl 07788994) Full Text: DOI arXiv
Janičić, Predrag; Narboux, Julien Automated generation of illustrated proofs in geometry and beyond. (English) Zbl 07785121 Ann. Math. Artif. Intell. 91, No. 6, 797-820 (2023). MSC: 68T20 68T30 68T50 51-04 03B35 PDFBibTeX XMLCite \textit{P. Janičić} and \textit{J. Narboux}, Ann. Math. Artif. Intell. 91, No. 6, 797--820 (2023; Zbl 07785121) Full Text: DOI
Korniłowicz, Artur Elementary number theory problems. VIII. (English) Zbl 07771372 Formaliz. Math. 31, No. 1, 87-100 (2023). MSC: 68V20 11A41 03B35 PDFBibTeX XMLCite \textit{A. Korniłowicz}, Formaliz. Math. 31, No. 1, 87--100 (2023; Zbl 07771372) Full Text: DOI OA License
Korniłowicz, Artur Elementary number theory problems. VII. (English) Zbl 07771366 Formaliz. Math. 31, No. 1, 23-29 (2023). MSC: 68V20 11A41 03B35 PDFBibTeX XMLCite \textit{A. Korniłowicz}, Formaliz. Math. 31, No. 1, 23--29 (2023; Zbl 07771366) Full Text: DOI OA License
Pientka, Brigitte (ed.); Tinelli, Cesare (ed.) Automated deduction – CADE 29. 29th international conference on automated deduction, Rome, Italy, July 1–4, 2023. Proceedings. (English) Zbl 07768439 Lecture Notes in Computer Science 14132. Lecture Notes in Artificial Intelligence. Cham: Springer (ISBN 978-3-031-38498-1/pbk; 978-3-031-38499-8/ebook). xxv, 592 p., open access (2023). MSC: 68-06 03-06 03B35 68V15 00B25 PDFBibTeX XMLCite \textit{B. Pientka} (ed.) and \textit{C. Tinelli} (ed.), Automated deduction -- CADE 29. 29th international conference on automated deduction, Rome, Italy, July 1--4, 2023. Proceedings. Cham: Springer (2023; Zbl 07768439) Full Text: DOI
Stratulat, Sorin Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs. (English) Zbl 07759321 Ann. Math. Artif. Intell. 91, No. 5, 651-673 (2023). MSC: 03B35 03F07 68-04 68U99 PDFBibTeX XMLCite \textit{S. Stratulat}, Ann. Math. Artif. Intell. 91, No. 5, 651--673 (2023; Zbl 07759321) Full Text: DOI
Škrabánek, Pavel; Doležel, Petr; Matoušek, Radomil RGB images-driven recognition of grapevine varieties using a densely connected convolutional network. (English) Zbl 07737111 Log. J. IGPL 31, No. 4, 618-633 (2023). MSC: 03-XX 68-XX PDFBibTeX XMLCite \textit{P. Škrabánek} et al., Log. J. IGPL 31, No. 4, 618--633 (2023; Zbl 07737111) Full Text: DOI
Li, Dafa Simplifying the axiomatization for ordered affine geometry via a theorem prover. (English) Zbl 1518.51009 J. Geom. 114, No. 2, Paper No. 9, 6 p. (2023). Reviewer: Victor V. Pambuccian (Glendale) MSC: 51G05 03F55 03B30 03B35 PDFBibTeX XMLCite \textit{D. Li}, J. Geom. 114, No. 2, Paper No. 9, 6 p. (2023; Zbl 1518.51009) Full Text: DOI
Edmonds, Chelsea; Koutsoukou-Argyraki, Angeliki; Paulson, Lawrence C. Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL. (English) Zbl 07695705 J. Autom. Reasoning 67, No. 1, Paper No. 2, 21 p. (2023). MSC: 68V15 05C35 05A17 11P81 03B35 68V15 68V20 68V35 PDFBibTeX XMLCite \textit{C. Edmonds} et al., J. Autom. Reasoning 67, No. 1, Paper No. 2, 21 p. (2023; Zbl 07695705) Full Text: DOI arXiv
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 PDFBibTeX XMLCite \textit{J. Avigad} et al., Am. Math. Mon. 130, No. 5, 446--453 (2023; Zbl 07684392) Full Text: DOI arXiv
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 PDFBibTeX XMLCite \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
Avigad, Jeremy Mathematics and the formal turn. arXiv:2311.00007 Preprint, arXiv:2311.00007 [math.HO] (2023). MSC: 03B35 68V20 68Q60 68V15 68V25 68V35 68T01 97U50 BibTeX Cite \textit{J. Avigad}, ``Mathematics and the formal turn'', Preprint, arXiv:2311.00007 [math.HO] (2023) Full Text: arXiv OA License
Edmonds, Chelsea; Paulson, Lawrence C. Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma. arXiv:2310.00513 Preprint, arXiv:2310.00513 [cs.LO] (2023). MSC: 05D05 68V20 68V15 68V35 03B35 05C65 05C15 60C05 BibTeX Cite \textit{C. Edmonds} and \textit{L. C. Paulson}, ``Formal Probabilistic Methods for Combinatorial Structures using the Lov\'asz Local Lemma'', Preprint, arXiv:2310.00513 [cs.LO] (2023) Full Text: DOI arXiv OA License
Scheidt, Gregor vom Experimental results from applying GPT-4 to an unpublished formal language. arXiv:2305.12196 Preprint, arXiv:2305.12196 [cs.CL] (2023). MSC: 03B35 BibTeX Cite \textit{G. v. Scheidt}, ``Experimental results from applying GPT-4 to an unpublished formal language'', Preprint, arXiv:2305.12196 [cs.CL] (2023) Full Text: arXiv OA License
Chang, Ke-Ming; Chen, Kuo-Chang Toward finiteness of central configurations for the planar six-body problem by symbolic computations. arXiv:2303.02853 Preprint, arXiv:2303.02853 [math.DS] (2023). MSC: 70F10 70F15 68W30 03B35 BibTeX Cite \textit{K.-M. Chang} and \textit{K.-C. Chen}, ``Toward finiteness of central configurations for the planar six-body problem by symbolic computations'', Preprint, arXiv:2303.02853 [math.DS] (2023) Full Text: arXiv OA License
Schang, Fabien No, no, and no. (English) Zbl 07740528 Béziau, Jean-Yves (ed.) et al., Logic in question. Talks from the annual Sorbonne logic workshop (2011–2019), Paris, France, April 15–16, 2019. Cham: Birkhäuser. Stud. Univers. Log., 491-512 (2022). MSC: 03A05 03Bxx 01A25 01A55 03B35 03B05 03B65 PDFBibTeX XMLCite \textit{F. Schang}, in: Logic in question. Talks from the annual Sorbonne logic workshop (2011--2019), Paris, France, April 15--16, 2019. Cham: Birkhäuser. 491--512 (2022; Zbl 07740528) Full Text: DOI
Tao, Yichen; Cao, Qinxiang LOGIC: a Coq library for logics. (English) Zbl 1528.68397 Dong, Wei (ed.) et al., Dependable software engineering. Theories, tools, and applications. 8th international symposium, SETTA 2022, Beijing, China, October 27–29, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13649, 205-226 (2022). MSC: 68V20 03B35 03B70 PDFBibTeX XMLCite \textit{Y. Tao} and \textit{Q. Cao}, Lect. Notes Comput. Sci. 13649, 205--226 (2022; Zbl 1528.68397) Full Text: DOI
Brown, Christopher W.; Kovács, Zoltán; Recio, Tomás; Vajda, Róbert; Vélez, M. Pilar Is computer algebra ready for conjecturing and proving geometric inequalities in the classroom? (English) Zbl 07700011 Math. Comput. Sci. 16, No. 4, Paper No. 31, 14 p. (2022). MSC: 97G40 14H50 03B35 68T15 68V15 14Q30 51M16 51-04 51-08 PDFBibTeX XMLCite \textit{C. W. Brown} et al., Math. Comput. Sci. 16, No. 4, Paper No. 31, 14 p. (2022; Zbl 07700011) Full Text: DOI
Calude, Cristian S.; Staiger, Ludwig Long and short proofs. (English) Zbl 07691467 Bull. Math. Soc. Sci. Math. Roum., Nouv. Sér. 65(113), No. 2, 203-211 (2022). MSC: 03B22 03B35 00A30 03A10 PDFBibTeX XMLCite \textit{C. S. Calude} and \textit{L. Staiger}, Bull. Math. Soc. Sci. Math. Roum., Nouv. Sér. 65(113), No. 2, 203--211 (2022; Zbl 07691467)
Preto, Sandro; Finger, Marcelo Efficient representation of piecewise linear functions into Łukasiewicz logic modulo satisfiability. (English) Zbl 1512.68428 Math. Struct. Comput. Sci. 32, No. 9, 1119-1144 (2022). MSC: 68V15 03B35 03B50 68W40 PDFBibTeX XMLCite \textit{S. Preto} and \textit{M. Finger}, Math. Struct. Comput. Sci. 32, No. 9, 1119--1144 (2022; Zbl 1512.68428) Full Text: DOI
Goré, Rajeev; Shillito, Ian Direct elimination of additive-cuts in GL4ip: verified and extracted. (English) Zbl 1518.03015 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). Reviewer: Annika Kanckos (Helsinki) MSC: 03F45 03B35 03F05 PDFBibTeX XMLCite \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 1518.03015)
Rimatskiĭ, Vitaliĭ Valentinovich Globally admissible inference rules. (English) Zbl 07656248 Izv. Irkutsk. Gos. Univ., Ser. Mat. 42, 138-160 (2022). MSC: 03F25 03B35 PDFBibTeX XMLCite \textit{V. V. Rimatskiĭ}, Izv. Irkutsk. Gos. Univ., Ser. Mat. 42, 138--160 (2022; Zbl 07656248) Full Text: DOI Link
Hofstadler, Clemens; Raab, Clemens G.; Regensburger, Georg Computing elements of certain form in ideals to prove properties of operators. (English) Zbl 07646553 Math. Comput. Sci. 16, No. 2-3, Paper No. 17, 19 p. (2022). Reviewer: Xiangui Zhao (Huizhou) MSC: 16Z10 03B35 PDFBibTeX XMLCite \textit{C. Hofstadler} et al., Math. Comput. Sci. 16, No. 2--3, Paper No. 17, 19 p. (2022; Zbl 07646553) Full Text: DOI arXiv
Bonacina, Roberta; Misselbeck-Wessel, Daniel A formal approach to Menger’s theorem. (English) Zbl 1504.05136 Rep. Math. Logic 57, 45-51 (2022). MSC: 05C30 05C40 05C20 03B35 PDFBibTeX XMLCite \textit{R. Bonacina} and \textit{D. Misselbeck-Wessel}, Rep. Math. Logic 57, 45--51 (2022; Zbl 1504.05136) Full Text: DOI
Papacchini, Fabio; Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare Correction to: “Local is best: efficient reductions to modal logic K”. (English) Zbl 1512.68426 J. Autom. Reasoning 66, No. 4, 1099 (2022). MSC: 68V15 03B35 03B45 PDFBibTeX XMLCite \textit{F. Papacchini} et al., J. Autom. Reasoning 66, No. 4, 1099 (2022; Zbl 1512.68426) Full Text: DOI
Papacchini, Fabio; Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare Local is best: efficient reductions to modal logic K. (English) Zbl 1512.68425 J. Autom. Reasoning 66, No. 4, 639-666 (2022); correction ibid. 66, No. 4, 1099 (2022). MSC: 68V15 03B35 03B45 PDFBibTeX XMLCite \textit{F. Papacchini} et al., J. Autom. Reasoning 66, No. 4, 639--666 (2022; Zbl 1512.68425) Full Text: DOI
Hoefnagel, Michael; Jacqmin, Pierre-Alain Matrix taxonomy and Bourn localization. (English) Zbl 07629356 Appl. Categ. Struct. 30, No. 6, 1305-1340 (2022). Reviewer: Jose Avila (Cali) MSC: 18A20 03B35 18E13 18-08 08B05 68V20 03C35 68V05 18A35 18B15 08C05 PDFBibTeX XMLCite \textit{M. Hoefnagel} and \textit{P.-A. Jacqmin}, Appl. Categ. Struct. 30, No. 6, 1305--1340 (2022; Zbl 07629356) Full Text: DOI arXiv
Russell, Bertrand [Potter, Michael] An essay on the foundations of geometry. With a new foreword by Michael Potter. Reprint of the 1897 edition. (English) Zbl 1520.51001 Routledge Classics. Milton Park, Abingdon: Routledge (ISBN 978-1-032-31264-4/hbk; 978-1-032-31226-2/pbk; 978-1-003-30887-4/ebook). xviii, 221 p. (2022). MSC: 51-02 03-02 00A30 03B35 51P05 01A75 PDFBibTeX XMLCite \textit{B. Russell}, An essay on the foundations of geometry. With a new foreword by Michael Potter. Reprint of the 1897 edition. Milton Park, Abingdon: Routledge (2022; Zbl 1520.51001) Full Text: DOI
Rauch, Jan; Šimůnek, Milan; Chudán, David; Máša, Petr Mechanizing hypothesis formation. Principles and case studies. (English) Zbl 1502.68011 Boca Raton, FL: CRC Press/Science Publishers (ISBN 978-0-367-54980-0/hbk; 978-1-003-09144-8/ebook). xvi, 345 p. (2022). MSC: 68-02 62-02 03B35 62D20 62H15 62H17 62H20 62R07 68T05 68T09 68T27 PDFBibTeX XMLCite \textit{J. Rauch} et al., Mechanizing hypothesis formation. Principles and case studies. Boca Raton, FL: CRC Press/Science Publishers (2022; Zbl 1502.68011) Full Text: DOI
Rimatskiy, Vytalii Valentinovich Description of modal logics which enjoy co-cover property. (English) Zbl 07593949 Sib. Èlektron. Mat. Izv. 19, No. 1, 316-325 (2022). MSC: 03F25 03B35 PDFBibTeX XMLCite \textit{V. V. Rimatskiy}, Sib. Èlektron. Mat. Izv. 19, No. 1, 316--325 (2022; Zbl 07593949) Full Text: DOI
Farjami, Ali Experiments in Kratzer modal semantics using Isabelle/HOL. (English) Zbl 07582521 Liao, Beishui (ed.) et al., Logics for new-generation AI. Second international workshop, Zhuhai, China, June 10–12, 2022. London: College Publications. 36-42 (2022). MSC: 03B35 03B45 68V15 PDFBibTeX XMLCite \textit{A. Farjami}, in: Logics for new-generation AI. Second international workshop, Zhuhai, China, June 10--12, 2022. London: College Publications. 36--42 (2022; Zbl 07582521)
Ivanov, Ievgen On induction principles for partial orders. (English) Zbl 07580913 Log. Univers. 16, No. 1-2, 105-147 (2022). MSC: 03B70 03B35 06A06 PDFBibTeX XMLCite \textit{I. Ivanov}, Log. Univers. 16, No. 1--2, 105--147 (2022; Zbl 07580913) Full Text: DOI Backlinks: MO
Zhang, Shujun; Nishida, Naoki On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs. (English) Zbl 07570125 Hanus, Michael (ed.) et al., Functional and logic programming. 16th international symposium, FLOPS 2022, Kyoto, Japan, May 10–12, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13215, 262-281 (2022). MSC: 03B35 PDFBibTeX XMLCite \textit{S. Zhang} and \textit{N. Nishida}, Lect. Notes Comput. Sci. 13215, 262--281 (2022; Zbl 07570125) Full Text: DOI
Beeson, Michael Euclid after computer proof-checking. (English) Zbl 07566943 Am. Math. Mon. 129, No. 7, 623-646 (2022). MSC: 03B30 03B35 51M05 PDFBibTeX XMLCite \textit{M. Beeson}, Am. Math. Mon. 129, No. 7, 623--646 (2022; Zbl 07566943) Full Text: DOI arXiv
Koutsoukou-Argyraki, Angeliki; Li, Wenda; Paulson, Lawrence C. Irrationality and transcendence criteria for infinite series in Isabelle/HOL. (English) Zbl 1518.11003 Exp. Math. 31, No. 2, 401-412 (2022). Reviewer: Alexandra Shlapentokh (Greenville) MSC: 11-04 11J81 11J68 68V20 03B35 68V35 PDFBibTeX XMLCite \textit{A. Koutsoukou-Argyraki} et al., Exp. Math. 31, No. 2, 401--412 (2022; Zbl 1518.11003) Full Text: DOI arXiv
Džamonja, Mirna; Koutsoukou-Argyraki, Angeliki; Paulson, Lawrence C. Formalizing ordinal partition relations using Isabelle/HOL. (English) Zbl 1520.68217 Exp. Math. 31, No. 2, 383-400 (2022). Reviewer: Truong Hoang Le (Hà Nội) MSC: 68V20 03B35 03E02 03E05 PDFBibTeX XMLCite \textit{M. Džamonja} et al., Exp. Math. 31, No. 2, 383--400 (2022; Zbl 1520.68217) Full Text: DOI arXiv
Bordg, Anthony; Paulson, Lawrence; Li, Wenda Simple type theory is not too simple: Grothendieck’s schemes without dependent types. (English) Zbl 1498.14001 Exp. Math. 31, No. 2, 364-382 (2022). Reviewer: Ocean Teng (Beijing) MSC: 14-04 14-11 68V20 14A15 03B35 PDFBibTeX XMLCite \textit{A. Bordg} et al., Exp. Math. 31, No. 2, 364--382 (2022; Zbl 1498.14001) Full Text: DOI arXiv
Shramko, Yaroslav Between Hilbert and Gentzen: four-valued consequence systems and structural reasoning. (English) Zbl 07557505 Arch. Math. Logic 61, No. 5-6, 627-651 (2022). MSC: 03F03 03F07 03B35 03B47 03B70 PDFBibTeX XMLCite \textit{Y. Shramko}, Arch. Math. Logic 61, No. 5--6, 627--651 (2022; Zbl 07557505) 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
Coquand, Thierry; Tosun, Ayberk Formal topology and univalent foundations. (English) Zbl 1528.03251 Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 255-266 (2022). MSC: 03F65 03B35 03B38 PDFBibTeX XMLCite \textit{T. Coquand} and \textit{A. Tosun}, in: Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school ``Proof and computation'', September 20--26, 2019. Hackensack, NJ: World Scientific. 255--266 (2022; Zbl 1528.03251) Full Text: DOI
Platzer, André Correction to: “Differential dynamic logic for hybrid systems”. (English) Zbl 07498611 J. Autom. Reasoning 66, No. 1, 173 (2022). MSC: 68V15 03B70 03B35 68Q60 PDFBibTeX XMLCite \textit{A. Platzer}, J. Autom. Reasoning 66, No. 1, 173 (2022; Zbl 07498611) Full Text: DOI
Bickford, Mark; Kozen, Dexter; Silva, Alexandra Formalizing Moessner’s theorem and generalizations in Nuprl. (English) Zbl 07432496 J. Log. Algebr. Methods Program. 124, Article ID 100713, 6 p. (2022). MSC: 03B35 11B83 13F25 68V20 PDFBibTeX XMLCite \textit{M. Bickford} et al., J. Log. Algebr. Methods Program. 124, Article ID 100713, 6 p. (2022; Zbl 07432496) Full Text: DOI
Echenim, Mnacho; Iosif, Radu; Peltier, Nicolas Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules. (English) Zbl 07411507 Inf. Process. Lett. 173, Article ID 106169, 5 p. (2022). MSC: 03B70 03B25 03B35 PDFBibTeX XMLCite \textit{M. Echenim} et al., Inf. Process. Lett. 173, Article ID 106169, 5 p. (2022; Zbl 07411507) Full Text: DOI HAL
Fiorino, Guido A non-clausal tableau calculus for MinSat. (English) Zbl 1482.68269 Inf. Process. Lett. 173, Article ID 106167, 5 p. (2022). Reviewer: Łukasz Czajka (Dortmund) MSC: 68V15 03B05 03B35 68R07 PDFBibTeX XMLCite \textit{G. Fiorino}, Inf. Process. Lett. 173, Article ID 106167, 5 p. (2022; Zbl 1482.68269) Full Text: DOI
Hofstadler, Clemens; Raab, Clemens G.; Regensburger, Georg Universal truth of operator statements via ideal membership. arXiv:2212.11662 Preprint, arXiv:2212.11662 [math.LO] (2022). MSC: 03B35 18E05 68V15 16B50 BibTeX Cite \textit{C. Hofstadler} et al., ``Universal truth of operator statements via ideal membership'', Preprint, arXiv:2212.11662 [math.LO] (2022) Full Text: arXiv OA License
Kosaian, Katherine; Tan, Yong Kiam; Platzer, André A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. arXiv:2209.10978 Preprint, arXiv:2209.10978 [cs.LO] (2022). MSC: 68V20 68V15 03C10 03B35 03B10 BibTeX Cite \textit{K. Kosaian} et al., ``A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL'', Preprint, arXiv:2209.10978 [cs.LO] (2022) Full Text: DOI arXiv OA License
Benzmüller, Christoph; Fuenmayor, David; Steen, Alexander; Sutcliffe, Geoff Who Finds the Short Proof? An Exploration of Variants of Boolos’ Curious Inference using Higher-order Automated Theorem Provers. arXiv:2208.06879 Preprint, arXiv:2208.06879 [math.LO] (2022). MSC: 03B35 03B10 03B16 68T27 68T30 03A05 00A30 BibTeX Cite \textit{C. Benzmüller} et al., ``Who Finds the Short Proof? An Exploration of Variants of Boolos' Curious Inference using Higher-order Automated Theorem Provers'', Preprint, arXiv:2208.06879 [math.LO] (2022) Full Text: DOI arXiv OA License
Waszek, David; Schlimm, Dirk Calculus as method or calculus as rules? Boole and Frege on the aims of a logical calculus. (English) Zbl 1528.03005 Synthese 199, No. 5-6, 11913-11943 (2021). MSC: 03-03 01A55 PDFBibTeX XMLCite \textit{D. Waszek} and \textit{D. Schlimm}, Synthese 199, No. 5--6, 11913--11943 (2021; Zbl 1528.03005) Full Text: DOI
Cao, Feng; Xu, Yang; Liu, Jun; Chen, Shuwei; Yi, Jianbing A multi-clause dynamic deduction algorithm based on standard contradiction separation rule. (English) Zbl 1527.68257 Inf. Sci. 566, 281-299 (2021). MSC: 68V15 03B35 PDFBibTeX XMLCite \textit{F. Cao} et al., Inf. Sci. 566, 281--299 (2021; Zbl 1527.68257) Full Text: DOI
Scharager, Matias; Cordwell, Katherine; Mitsch, Stefan; Platzer, André Verified quadratic virtual substitution for real arithmetic. (English) Zbl 1521.68246 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, 200-217 (2021). MSC: 68V20 03B35 03C10 03F30 PDFBibTeX XMLCite \textit{M. Scharager} et al., Lect. Notes Comput. Sci. 13047, 200--217 (2021; Zbl 1521.68246) Full Text: DOI arXiv
Rublev, V. S.; Kondakov, M. D. Automated teaching system “sets”. I. (English) Zbl 07645046 Model. Anal. Inf. Sist. 28, No. 1, 90-103 (2021). MSC: 03B35 03F03 97E60 PDFBibTeX XMLCite \textit{V. S. Rublev} and \textit{M. D. Kondakov}, Model. Anal. Inf. Sist. 28, No. 1, 90--103 (2021; Zbl 07645046) Full Text: DOI MNR
Tabareau, Nicolas; Tanter, Éric; Sozeau, Matthieu The marriage of univalence and parametricity. (English) Zbl 1499.68379 J. ACM 68, No. 1, Paper No. 5, 44 p. (2021). MSC: 68V15 03B35 03B38 PDFBibTeX XMLCite \textit{N. Tabareau} et al., J. ACM 68, No. 1, Paper No. 5, 44 p. (2021; Zbl 1499.68379) Full Text: DOI arXiv
Bentkamp, Alexander The embedding path order for \(\lambda\)-free higher-order terms. (English) Zbl 1515.03059 J. Appl. Log. - IfCoLog J. Log. Appl. 8, No. 10, 2447-2469 (2021). MSC: 03B35 03B16 68V15 PDFBibTeX XMLCite \textit{A. Bentkamp}, J. Appl. Log. - IfCoLog J. Log. Appl. 8, No. 10, 2447--2469 (2021; Zbl 1515.03059)
Stevens, Lukas; Nipkow, Tobias A verified decision procedure for orders in Isabelle/HOL. (English) Zbl 1497.68549 Hou, Zhe (ed.) et al., Automated technology for verification and analysis. 19th international symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18–22, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12971, 127-143 (2021). MSC: 68V20 03B35 68V15 PDFBibTeX XMLCite \textit{L. Stevens} and \textit{T. Nipkow}, Lect. Notes Comput. Sci. 12971, 127--143 (2021; Zbl 1497.68549) Full Text: DOI arXiv
Coghetto, Roland Pappus’s hexagon theorem in real projective plane. (English) Zbl 1483.68487 Formaliz. Math. 29, No. 2, 69-76 (2021). MSC: 68V20 03B35 51N15 PDFBibTeX XMLCite \textit{R. Coghetto}, Formaliz. Math. 29, No. 2, 69--76 (2021; Zbl 1483.68487) Full Text: DOI
Zou, Yu; Peng, Xicheng; Rao, Yongsheng An identity method for proving geometry theorems based on Wu’s method. (Chinese. English summary) Zbl 1499.03011 Sci. Sin., Math. 51, No. 1, 289-300 (2021). MSC: 03B35 51-08 PDFBibTeX XMLCite \textit{Y. Zou} et al., Sci. Sin., Math. 51, No. 1, 289--300 (2021; Zbl 1499.03011) Full Text: DOI
Paulson, Lawrence C. Ackermann’s function in iterative form: a proof assistant experiment. (English) Zbl 07482180 Bull. Symb. Log. 27, No. 4, 426-435 (2021). MSC: 03B35 03D20 68V20 PDFBibTeX XMLCite \textit{L. C. Paulson}, Bull. Symb. Log. 27, No. 4, 426--435 (2021; Zbl 07482180) Full Text: DOI arXiv
Forster, Yannick; Kirst, Dominik; Wehr, Dominik Completeness theorems for first-order logic analysed in constructive type theory. Extended version. (English) Zbl 07471462 J. Log. Comput. 31, No. 1, 112-151 (2021). MSC: 03F50 03B35 03B38 03B10 PDFBibTeX XMLCite \textit{Y. Forster} et al., J. Log. Comput. 31, No. 1, 112--151 (2021; Zbl 07471462) Full Text: DOI
de Lima, Thaynara Arielly; Galdino, André Luiz; Avelar, Andréia Borges; Ayala-Rincón, Mauricio Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem. (English) Zbl 1493.68389 J. Autom. Reasoning 65, No. 8, 1231-1263 (2021). Reviewer: Filippo Nuccio (Saint-Étienne) MSC: 68V20 03B35 13P99 16Z05 20N02 68V15 PDFBibTeX XMLCite \textit{T. A. de Lima} et al., J. Autom. Reasoning 65, No. 8, 1231--1263 (2021; Zbl 1493.68389) Full Text: DOI
Ichikawa, Tsubasa The Born rule and logical inference in quantum mechanics. (English) Zbl 1503.81008 PTEP, Prog. Theor. Exper. Phys. 2021, No. 12, Article ID 123A01, 18 p. (2021). MSC: 81P05 03B35 PDFBibTeX XMLCite \textit{T. Ichikawa}, PTEP, Prog. Theor. Exper. Phys. 2021, No. 12, Article ID 123A01, 18 p. (2021; Zbl 1503.81008) Full Text: DOI arXiv
Li, Chu-Min; Xiao, Fan; Manyà, Felip A resolution calculus for MinSAT. (English) Zbl 1524.68427 Log. J. IGPL 29, No. 1, 28-44 (2021). MSC: 68V15 03B35 PDFBibTeX XMLCite \textit{C.-M. Li} et al., Log. J. IGPL 29, No. 1, 28--44 (2021; Zbl 1524.68427) Full Text: DOI
Argelich, Josep; Li, Chu Min; Manyà, Felip; Soler, Joan Ramon Clause tableaux for maximum and minimum satisfiability. (English) Zbl 1524.68426 Log. J. IGPL 29, No. 1, 7-27 (2021). MSC: 68V15 03B35 PDFBibTeX XMLCite \textit{J. Argelich} et al., Log. J. IGPL 29, No. 1, 7--27 (2021; Zbl 1524.68426) Full Text: DOI
Errington, Jacob; Jang, Junyoung; Pientka, Brigitte Harpoon: mechanizing metatheory interactively. (English) Zbl 07437106 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, 636-648 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{J. Errington} et al., Lect. Notes Comput. Sci. 12699, 636--648 (2021; Zbl 07437106) Full Text: DOI
de Moura, Leonardo; Ullrich, Sebastian The Lean 4 theorem prover and programming language. (English) Zbl 07437105 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, 625-635 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{L. de Moura} and \textit{S. Ullrich}, Lect. Notes Comput. Sci. 12699, 625--635 (2021; Zbl 07437105) Full Text: DOI
De Lon, Adrian; Koepke, Peter; Lorenzen, Anton; Marti, Adrian; Schütz, Marcel; Wenzel, Makarius The Isabelle/Naproche natural language proof assistant. (English) Zbl 07437104 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, 614-624 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{A. De Lon} et al., Lect. Notes Comput. Sci. 12699, 614--624 (2021; Zbl 07437104) Full Text: DOI
Smallbone, Nicholas Twee: an equational theorem prover. (English) Zbl 07437103 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, 602-613 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{N. Smallbone}, Lect. Notes Comput. Sci. 12699, 602--613 (2021; Zbl 07437103) Full Text: DOI
Baumgartner, Peter The Fusemate logic programming system. (English) Zbl 07437102 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, 589-601 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{P. Baumgartner}, Lect. Notes Comput. Sci. 12699, 589--601 (2021; Zbl 07437102) Full Text: DOI
Krueger, Ryan; Han, Jesse Michael; Selsam, Daniel Automatically building diagrams for olympiad geometry problems. (English) Zbl 07437101 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, 577-588 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{R. Krueger} et al., Lect. Notes Comput. Sci. 12699, 577--588 (2021; Zbl 07437101) Full Text: DOI arXiv
Neufeld, Emery; Bartocci, Ezio; Ciabattoni, Agata; Governatori, Guido A normative supervisor for reinforcement learning agents. (English) Zbl 07437100 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, 565-576 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{E. Neufeld} et al., Lect. Notes Comput. Sci. 12699, 565--576 (2021; Zbl 07437100) Full Text: DOI
Suda, Martin Improving ENIGMA-style clause selection while learning from history. (English) Zbl 07437099 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, 543-561 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{M. Suda}, Lect. Notes Comput. Sci. 12699, 543--561 (2021; Zbl 07437099) Full Text: DOI arXiv
Bártek, Filip; Suda, Martin Neural precedence recommender. (English) Zbl 07437098 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, 525-542 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{F. Bártek} and \textit{M. Suda}, Lect. Notes Comput. Sci. 12699, 525--542 (2021; Zbl 07437098) Full Text: DOI
Tammet, Tanel; Draheim, Dirk; Järv, Priit Confidences for commonsense reasoning. (English) Zbl 07437097 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, 507-524 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{T. Tammet} et al., Lect. Notes Comput. Sci. 12699, 507--524 (2021; Zbl 07437097) Full Text: DOI
Xu, Runqing; Li, Liming; Zhan, Bohua Verified interactive computation of definite integrals. (English) Zbl 07437096 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, 485-503 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{R. Xu} et al., Lect. Notes Comput. Sci. 12699, 485--503 (2021; Zbl 07437096) Full Text: DOI
Yolcu, Emre; Aaronson, Scott; Heule, Marijn J. H. An automated approach to the Collatz conjecture. (English) Zbl 07437095 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, 468-484 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{E. Yolcu} et al., Lect. Notes Comput. Sci. 12699, 468--484 (2021; Zbl 07437095) Full Text: DOI arXiv
Schurr, Hans-Jörg; Fleury, Mathias; Desharnais, Martin Reliable reconstruction of fine-grained proofs in a proof assistant. (English) Zbl 07437094 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, 450-467 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{H.-J. Schurr} et al., Lect. Notes Comput. Sci. 12699, 450--467 (2021; Zbl 07437094) Full Text: DOI
Bryant, Randal E.; Heule, Marijn J. H. Dual proof generation for quantified Boolean formulas with a BDD-based solver. (English) Zbl 07437093 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, 433-449 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{R. E. Bryant} and \textit{M. J. H. Heule}, Lect. Notes Comput. Sci. 12699, 433--449 (2021; Zbl 07437093) Full Text: DOI
Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar Superposition for full higher-order logic. (English) Zbl 1497.03030 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, 396-412 (2021). Reviewer: Łukasz Czajka (Dortmund) MSC: 03B35 03B16 68V15 PDFBibTeX XMLCite \textit{A. Bentkamp} et al., Lect. Notes Comput. Sci. 12699, 396--412 (2021; Zbl 1497.03030) Full Text: DOI
Nummelin, Visa; Bentkamp, Alexander; Tourret, Sophie; Vukmirović, Petar Superposition with first-class booleans and inprocessing clausification. (English) Zbl 07437090 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, 378-395 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{V. Nummelin} et al., Lect. Notes Comput. Sci. 12699, 378--395 (2021; Zbl 07437090) Full Text: DOI
Hozzová, Petra; Kovács, Laura; Voronkov, Andrei Integer induction in saturation. (English) Zbl 07437089 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, 361-377 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{P. Hozzová} et al., Lect. Notes Comput. Sci. 12699, 361--377 (2021; Zbl 07437089) Full Text: DOI
Ebner, Gabriel; Blanchette, Jasmin; Tourret, Sophie A unifying splitting framework. (English) Zbl 07437088 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, 344-360 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{G. Ebner} et al., Lect. Notes Comput. Sci. 12699, 344--360 (2021; Zbl 07437088) Full Text: DOI
Haifani, Fajar; Tourret, Sophie; Weidenbach, Christoph Generalized completeness for SOS resolution and its application to a new notion of relevance. (English) Zbl 07437087 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, 327-343 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{F. Haifani} et al., Lect. Notes Comput. Sci. 12699, 327--343 (2021; Zbl 07437087) Full Text: DOI
Baader, Franz; Koopmann, Patrick; Kriegel, Francesco; Nuradiansyah, Adrian Computing optimal repairs of quantified ABoxes w.r.t. static \(\mathcal{EL}\) TBoxes. (English) Zbl 07437086 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, 309-326 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{F. Baader} et al., Lect. Notes Comput. Sci. 12699, 309--326 (2021; Zbl 07437086) Full Text: DOI
Alrabbaa, Christian; Baader, Franz; Borgwardt, Stefan; Koopmann, Patrick; Kovtunova, Alisa Finding good proofs for description logic entailments using recursive quality measures. (English) Zbl 07437085 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, 291-308 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{C. Alrabbaa} et al., Lect. Notes Comput. Sci. 12699, 291--308 (2021; Zbl 07437085) Full Text: DOI arXiv
Yamada, Akihisa Multi-dimensional interpretations for termination of term rewriting. (English) Zbl 07437084 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, 273-290 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{A. Yamada}, Lect. Notes Comput. Sci. 12699, 273--290 (2021; Zbl 07437084) Full Text: DOI
Barnett, Lee A.; Biere, Armin Non-clausal redundancy properties. (English) Zbl 07437083 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, 252-272 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{L. A. Barnett} and \textit{A. Biere}, Lect. Notes Comput. Sci. 12699, 252--272 (2021; Zbl 07437083) Full Text: DOI
Nigam, Vivek; Reis, Giselle; Rahmouni, Samar; Ruess, Harald Proof search and certificates for evidential transactions. (English) Zbl 07437082 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, 234-251 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{V. Nigam} et al., Lect. Notes Comput. Sci. 12699, 234--251 (2021; Zbl 07437082) Full Text: DOI
Fiorentini, Camillo Efficient SAT-based proof search in intuitionistic propositional logic. (English) Zbl 07437081 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, 217-233 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{C. Fiorentini}, Lect. Notes Comput. Sci. 12699, 217--233 (2021; Zbl 07437081) Full Text: DOI
Chaudhuri, Kaustuv Subformula linking for intuitionistic logic with application to type theory. (English) Zbl 07437080 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, 200-216 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{K. Chaudhuri}, Lect. Notes Comput. Sci. 12699, 200--216 (2021; Zbl 07437080) Full Text: DOI
Echenim, Mnacho; Iosif, Radu; Peltier, Nicolas Unifying decidable entailments in separation logic with inductive definitions. (English) Zbl 07437079 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, 183-199 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{M. Echenim} et al., Lect. Notes Comput. Sci. 12699, 183--199 (2021; Zbl 07437079) Full Text: DOI arXiv
Kim, Dohan; Lynch, Christopher Equational theorem proving modulo. (English) Zbl 07437078 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, 166-182 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{D. Kim} and \textit{C. Lynch}, Lect. Notes Comput. Sci. 12699, 166--182 (2021; Zbl 07437078) Full Text: DOI
Sheng, Ying; Zohar, Yoni; Ringeissen, Christophe; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare Politeness and stable infiniteness: stronger together. (English) Zbl 07437077 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, 148-165 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{Y. Sheng} et al., Lect. Notes Comput. Sci. 12699, 148--165 (2021; Zbl 07437077) Full Text: DOI arXiv
Cimatti, Alessandro; Griggio, Alberto; Redondi, Gianluca Universal invariant checking of parametric systems with quantifier-free SMT reasoning. (English) Zbl 07437076 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, 131-147 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{A. Cimatti} et al., Lect. Notes Comput. Sci. 12699, 131--147 (2021; Zbl 07437076) Full Text: DOI
Brauße, Franz; Korovin, Konstantin; Korovina, Margarita V.; Müller, Norbert Th. The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints. (English) Zbl 07437075 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, 113-130 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{F. Brauße} et al., Lect. Notes Comput. Sci. 12699, 113--130 (2021; Zbl 07437075) Full Text: DOI arXiv
Nipkow, Tobias; Roßkopf, Simon Isabelle’s metalogic: formalization and proof checker. (English) Zbl 07437074 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, 93-110 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{T. Nipkow} and \textit{S. Roßkopf}, Lect. Notes Comput. Sci. 12699, 93--110 (2021; Zbl 07437074) Full Text: DOI arXiv
Papacchini, Fabio; Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare Efficient local reductions to basic modal logic. (English) Zbl 07437073 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, 76-92 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{F. Papacchini} et al., Lect. Notes Comput. Sci. 12699, 76--92 (2021; Zbl 07437073) Full Text: DOI
Wernhard, Christoph; Bibel, Wolfgang Learning from Łukasiewicz and Meredith: investigations into proof structures. (English) Zbl 07437072 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, 58-75 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{C. Wernhard} and \textit{W. Bibel}, Lect. Notes Comput. Sci. 12699, 58--75 (2021; Zbl 07437072) Full Text: DOI arXiv