Jackson, Marcel; Stokes, Tim Override and update. (English) Zbl 07251305 J. Pure Appl. Algebra 225, No. 3, Article ID 106532, 17 p. (2021). MSC: 08A70 03B35 20M20 03B70 68V15 PDF BibTeX XML Cite \textit{M. Jackson} and \textit{T. Stokes}, J. Pure Appl. Algebra 225, No. 3, Article ID 106532, 17 p. (2021; Zbl 07251305) Full Text: DOI
Mansky, Susannah; Gunter, Elsa L. Safety of a smart classes-used regression test selection algorithm. (English) Zbl 07313965 Nalon, Cláudia (ed.) et al., Proceedings of the 15th international workshop on logical and semantic frameworks, with applications, LSFA 2020, virtual workshop, August 27–28, 2020. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 351, 51-73 (2020). MSC: 03B70 68Q55 68T27 PDF BibTeX XML Cite \textit{S. Mansky} and \textit{E. L. Gunter}, Electron. Notes Theor. Comput. Sci. 351, 51--73 (2020; Zbl 07313965) Full Text: DOI
Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos; Pichardie, David System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory. (English) Zbl 07311962 J. Autom. Reasoning 64, No. 8, 1685-1729 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{G. Barthe} et al., J. Autom. Reasoning 64, No. 8, 1685--1729 (2020; Zbl 07311962) Full Text: DOI
Alonderis, R.; Pliuškevičius, R.; Pliuškevičienė, A.; Giedra, H. Loop-type sequent calculi for temporal logic. (English) Zbl 07311961 J. Autom. Reasoning 64, No. 8, 1663-1684 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{R. Alonderis} et al., J. Autom. Reasoning 64, No. 8, 1663--1684 (2020; Zbl 07311961) Full Text: DOI
Lucas, Salvador; Meseguer, José; Gutiérrez, Raúl The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques. (English) Zbl 07311960 J. Autom. Reasoning 64, No. 8, 1611-1662 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{S. Lucas} et al., J. Autom. Reasoning 64, No. 8, 1611--1662 (2020; Zbl 07311960) Full Text: DOI
Hustadt, Ullrich; Ozaki, Ana; Dixon, Clare Theorem proving for pointwise metric temporal logic over the naturals via translations. (English) Zbl 07311959 J. Autom. Reasoning 64, No. 8, 1553-1610 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{U. Hustadt} et al., J. Autom. Reasoning 64, No. 8, 1553--1610 (2020; Zbl 07311959) Full Text: DOI
Buzzard, Kevin Proving theorems with computers. (English) Zbl 07308947 Notices Am. Math. Soc. 67, No. 11, 1791-1799 (2020). MSC: 68V05 68V15 PDF BibTeX XML Cite \textit{K. Buzzard}, Notices Am. Math. Soc. 67, No. 11, 1791--1799 (2020; Zbl 07308947) Full Text: DOI
del Carmen González Huesca, Lourdes; Miranda Perea, Favio Ezequiel; Linares-Arévalo, P. Selene Dual and axiomatic systems for constructive S4, a formally verified equivalence. (English) Zbl 07297792 Felty, Amy (ed.) et al., 14th international workshop on logical and semantic frameworks, with applications, LSFA 2019, Natal, Brazil, in August 2019. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 348, 61-83 (2020). MSC: 03B45 68V15 PDF BibTeX XML Cite \textit{L. del Carmen González Huesca} et al., Electron. Notes Theor. Comput. Sci. 348, 61--83 (2020; Zbl 07297792) Full Text: DOI
Åman Pohjola, Johannes Psi-calculi revisited: connectivity and compositionality. (English) Zbl 07288621 Log. Methods Comput. Sci. 16, No. 4, Paper No. 16, 28 p. (2020). MSC: 03B70 68 PDF BibTeX XML Cite \textit{J. Åman Pohjola}, Log. Methods Comput. Sci. 16, No. 4, Paper No. 16, 28 p. (2020; Zbl 07288621) Full Text: Link arXiv
Botana, Francisco; Kovács, Zoltán; Recio, Tomás; Vélez, M. Pilar Towards an automatic geometer. (Spanish) Zbl 07274311 Gac. R. Soc. Mat. Esp. 23, No. 2, 343-371 (2020). Reviewer: Frank Stephan (Singapore) MSC: 68V15 01A73 51-03 51-04 PDF BibTeX XML Cite \textit{F. Botana} et al., Gac. R. Soc. Mat. Esp. 23, No. 2, 343--371 (2020; Zbl 07274311)
Neider, Daniel; Madhusudan, P.; Saha, Shambwaditya; Garg, Pranav; Park, Daejun A learning-based approach to synthesizing invariants for incomplete verification engines. (English) Zbl 07268912 J. Autom. Reasoning 64, No. 7, 1523-1552 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{D. Neider} et al., J. Autom. Reasoning 64, No. 7, 1523--1552 (2020; Zbl 07268912) Full Text: DOI
Hartmanns, Arnd; Junges, Sebastian; Katoen, Joost-Pieter; Quatmann, Tim Multi-cost bounded tradeoff analysis in MDP. (English) Zbl 07268911 J. Autom. Reasoning 64, No. 7, 1483-1522 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{A. Hartmanns} et al., J. Autom. Reasoning 64, No. 7, 1483--1522 (2020; Zbl 07268911) Full Text: DOI
Costa, Gabriele; Galletta, Letterio; Degano, Pierpaolo; Basin, David; Bodei, Chiara Natural projection as partial model checking. (English) Zbl 07268910 J. Autom. Reasoning 64, No. 7, 1445-1481 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{G. Costa} et al., J. Autom. Reasoning 64, No. 7, 1445--1481 (2020; Zbl 07268910) Full Text: DOI
Chini, Peter; Meyer, Roland; Saivasan, Prakash Fine-grained complexity of safety verification. (English) Zbl 07268909 J. Autom. Reasoning 64, No. 7, 1419-1444 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{P. Chini} et al., J. Autom. Reasoning 64, No. 7, 1419--1444 (2020; Zbl 07268909) Full Text: DOI
Champion, Adrien; Chiba, Tomoya; Kobayashi, Naoki; Sato, Ryosuke ICE-based refinement type discovery for higher-order functional programs. (English) Zbl 07268908 J. Autom. Reasoning 64, No. 7, 1393-1418 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{A. Champion} et al., J. Autom. Reasoning 64, No. 7, 1393--1418 (2020; Zbl 07268908) Full Text: DOI
Bryant, Randal E. Chain reduction for binary and zero-suppressed decision diagrams. (English) Zbl 07268907 J. Autom. Reasoning 64, No. 7, 1361-1391 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{R. E. Bryant}, J. Autom. Reasoning 64, No. 7, 1361--1391 (2020; Zbl 07268907) Full Text: DOI
Bansal, Kshitij; Koskinen, Eric; Tripp, Omer Synthesizing precise and useful commutativity conditions. (English) Zbl 07268906 J. Autom. Reasoning 64, No. 7, 1333-1359 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{K. Bansal} et al., J. Autom. Reasoning 64, No. 7, 1333--1359 (2020; Zbl 07268906) Full Text: DOI
Beyer, Dirk (ed.); Huisman, Marieke (ed.) Selected and extended papers from TACAS 2018: preface. (English) Zbl 07268905 J. Autom. Reasoning 64, No. 7, 1331-1332 (2020). MSC: 00Bxx 68V15 PDF BibTeX XML Cite \textit{D. Beyer} (ed.) and \textit{M. Huisman} (ed.), J. Autom. Reasoning 64, No. 7, 1331--1332 (2020; Zbl 07268905) Full Text: DOI
Conchon, Sylvain; Declerck, David; Zaïdi, Fatiha Parameterized model checking on the TSO weak memory model. (English) Zbl 07268904 J. Autom. Reasoning 64, No. 7, 1307-1330 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{S. Conchon} et al., J. Autom. Reasoning 64, No. 7, 1307--1330 (2020; Zbl 07268904) Full Text: DOI
Abrahamsson, Oskar; Ho, Son; Kanabar, Hrutvik; Kumar, Ramana; Myreen, Magnus O.; Norrish, Michael; Tan, Yong Kiam Proof-producing synthesis of CakeML from monadic HOL functions. (English) Zbl 07268903 J. Autom. Reasoning 64, No. 7, 1287-1306 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{O. Abrahamsson} et al., J. Autom. Reasoning 64, No. 7, 1287--1306 (2020; Zbl 07268903) Full Text: DOI
Finger, Marcelo; Preto, Sandro Probably partially true: satisfiability for Łukasiewicz infinitely-valued probabilistic logic and related topics. (English) Zbl 07268902 J. Autom. Reasoning 64, No. 7, 1269-1286 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{M. Finger} and \textit{S. Preto}, J. Autom. Reasoning 64, No. 7, 1269--1286 (2020; Zbl 07268902) Full Text: DOI
Kiesl, Benjamin; Rebola-Pardo, Adrián; Heule, Marijn J. H.; Biere, Armin Simulating strong practical proof systems with extended resolution. (English) Zbl 07268901 J. Autom. Reasoning 64, No. 7, 1247-1267 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{B. Kiesl} et al., J. Autom. Reasoning 64, No. 7, 1247--1267 (2020; Zbl 07268901) Full Text: DOI
Das, Anupam From QBFs to MALL and back via focussing. (English) Zbl 07268900 J. Autom. Reasoning 64, No. 7, 1221-1245 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{A. Das}, J. Autom. Reasoning 64, No. 7, 1221--1245 (2020; Zbl 07268900) Full Text: DOI
Larchey-Wendling, Dominique Constructive decision via redundancy-free proof-search. (English) Zbl 07268899 J. Autom. Reasoning 64, No. 7, 1197-1219 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{D. Larchey-Wendling}, J. Autom. Reasoning 64, No. 7, 1197--1219 (2020; Zbl 07268899) Full Text: DOI
Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; Waldmann, Uwe Formalizing Bachmair and Ganzinger’s ordered resolution prover. (English) Zbl 07268898 J. Autom. Reasoning 64, No. 7, 1169-1195 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{A. Schlichtkrull} et al., J. Autom. Reasoning 64, No. 7, 1169--1195 (2020; Zbl 07268898) Full Text: DOI
Affeldt, Reynald; Garrigue, Jacques; Saikawa, Takafumi A library for formalization of linear error-correcting codes. (English) Zbl 07268896 J. Autom. Reasoning 64, No. 6, 1123-1164 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{R. Affeldt} et al., J. Autom. Reasoning 64, No. 6, 1123--1164 (2020; Zbl 07268896) Full Text: DOI
Ballarin, Clemens Exploring the structure of an algebra text with locales. (English) Zbl 07268895 J. Autom. Reasoning 64, No. 6, 1093-1121 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{C. Ballarin}, J. Autom. Reasoning 64, No. 6, 1093--1121 (2020; Zbl 07268895) Full Text: DOI
Hajdu, Ákos; Micskei, Zoltán Efficient strategies for CEGAR-based model checking. (English) Zbl 07268894 J. Autom. Reasoning 64, No. 6, 1051-1091 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{Á. Hajdu} and \textit{Z. Micskei}, J. Autom. Reasoning 64, No. 6, 1051--1091 (2020; Zbl 07268894) 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 07268893 J. Autom. Reasoning 64, No. 6, 1001-1050 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{G. Burel} et al., J. Autom. Reasoning 64, No. 6, 1001--1050 (2020; Zbl 07268893) Full Text: DOI
Sozeau, Matthieu; Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Forster, Yannick; Kunze, Fabian; Malecha, Gregory; Tabareau, Nicolas; Winterhalter, Théo The MetaCoq project. (English) Zbl 07268892 J. Autom. Reasoning 64, No. 5, 947-999 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{M. Sozeau} et al., J. Autom. Reasoning 64, No. 5, 947--999 (2020; Zbl 07268892) Full Text: DOI
Syeda, Hira Taqdees; Klein, Gerwin Formal reasoning under cached address translation. (English) Zbl 07268891 J. Autom. Reasoning 64, No. 5, 911-945 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{H. T. Syeda} and \textit{G. Klein}, J. Autom. Reasoning 64, No. 5, 911--945 (2020; Zbl 07268891) Full Text: DOI
Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias Verified analysis of random binary tree structures. (English) Zbl 07268890 J. Autom. Reasoning 64, No. 5, 879-910 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{M. Eberl} et al., J. Autom. Reasoning 64, No. 5, 879--910 (2020; Zbl 07268890) Full Text: DOI
Daggitt, Matthew L.; Zmigrod, Ran; Griffin, Timothy G. A relaxation of Üresin and Dubois’ asynchronous fixed-point theory in Agda. (English) Zbl 07268889 J. Autom. Reasoning 64, No. 5, 857-877 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{M. L. Daggitt} et al., J. Autom. Reasoning 64, No. 5, 857--877 (2020; Zbl 07268889) Full Text: DOI
Thiemann, René; Bottesch, Ralph; Divasón, Jose; Haslbeck, Max W.; Joosten, Sebastiaan J. C.; Yamada, Akihisa Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL. (English) Zbl 07268888 J. Autom. Reasoning 64, No. 5, 827-856 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{R. Thiemann} et al., J. Autom. Reasoning 64, No. 5, 827--856 (2020; Zbl 07268888) Full Text: DOI
Doczkal, Christian; Pous, Damien Graph theory in Coq: minors, treewidth, and isomorphisms. (English) Zbl 07268887 J. Autom. Reasoning 64, No. 5, 795-825 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{C. Doczkal} and \textit{D. Pous}, J. Autom. Reasoning 64, No. 5, 795--825 (2020; Zbl 07268887) Full Text: DOI
Burel, Guillaume Linking focusing and resolution with selection. (English) Zbl 1446.03099 ACM Trans. Comput. Log. 21, No. 3, Article No. 18, 30 p. (2020). MSC: 03F03 03B35 03F05 68V15 PDF BibTeX XML Cite \textit{G. Burel}, ACM Trans. Comput. Log. 21, No. 3, Article No. 18, 30 p. (2020; Zbl 1446.03099) Full Text: DOI
Jiang, Nan; Li, Qing’an; Wang, Lumeng; Zhang, Xiaotong; He, Yanxiang Overview on mechanized theorem proving. (Chinese. English summary) Zbl 1449.68143 J. Softw. 31, No. 1, 82-112 (2020). MSC: 68V15 03B35 03B70 68Q60 68-02 PDF BibTeX XML Cite \textit{N. Jiang} et al., J. Softw. 31, No. 1, 82--112 (2020; Zbl 1449.68143) Full Text: DOI
Ladra, Manuel; Páez-Guillán, Pilar; Recio, Tomás Dealing with negative conditions in automated proving: tools and challenges. The unexpected consequences of Rabinowitsch’s trick. (English) Zbl 07232901 Rev. R. Acad. Cienc. Exactas Fís. Nat., Ser. A Mat., RACSAM 114, No. 4, Paper No. 162, 16 p. (2020). MSC: 68V15 14Q20 PDF BibTeX XML Cite \textit{M. Ladra} et al., Rev. R. Acad. Cienc. Exactas Fís. Nat., Ser. A Mat., RACSAM 114, No. 4, Paper No. 162, 16 p. (2020; Zbl 07232901) Full Text: DOI
Borus, Gergő Gyula; Gilányi, Attila Computer assisted solution of systems of two variable linear functional equations. (English) Zbl 1444.39024 Aequationes Math. 94, No. 4, 723-736 (2020). MSC: 39B52 68V05 68V15 PDF BibTeX XML Cite \textit{G. G. Borus} and \textit{A. Gilányi}, Aequationes Math. 94, No. 4, 723--736 (2020; Zbl 1444.39024) Full Text: DOI
Montes, Antonio Presentation of the book The Gröbner cover. (English) Zbl 07225433 Math. Comput. Sci. 14, No. 2, 471-482 (2020). MSC: 13P10 00A17 03B35 13F20 68V15 PDF BibTeX XML Cite \textit{A. Montes}, Math. Comput. Sci. 14, No. 2, 471--482 (2020; Zbl 07225433) Full Text: DOI
Bowen, Jonathan P. Book review of: G. O’Regan, Concise guide to formal methods: theory, fundamentals and industry applications. (English) Zbl 1451.00026 Formal Asp. Comput. 32, No. 1, 147-148 (2020). MSC: 00A17 68-01 03B70 68N30 68Q45 68Q60 68V15 PDF BibTeX XML Cite \textit{J. P. Bowen}, Formal Asp. Comput. 32, No. 1, 147--148 (2020; Zbl 1451.00026) Full Text: DOI
Ahmad, Waqar; Hasan, Osman; Tahar, Sofiène Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation. (English) Zbl 1451.68057 Formal Asp. Comput. 32, No. 1, 71-111 (2020). MSC: 68M15 68M10 68V15 PDF BibTeX XML Cite \textit{W. Ahmad} et al., Formal Asp. Comput. 32, No. 1, 71--111 (2020; Zbl 1451.68057) Full Text: DOI
Vlasov, Dmitriĭ Yur’evich Proof search algorithm in pure logical framework. (English) Zbl 1451.68327 Sib. Èlektron. Mat. Izv. 17, 988-998 (2020). MSC: 68V15 03B35 PDF BibTeX XML Cite \textit{D. Y. Vlasov}, Sib. Èlektron. Mat. Izv. 17, 988--998 (2020; Zbl 1451.68327) Full Text: DOI
Bradford, Alexander; Day, J. Kain; Hutchinson, Laura; Kaperick, Bryan; Larson, Craig E.; Mills, Matthew; Muncy, David; Van Cleemput, Nico Automated conjecturing. II: Chomp and reasoned game play. (English) Zbl 1445.68328 J. Artif. Intell. Res. (JAIR) 68, 447-461 (2020). MSC: 68V15 91A46 PDF BibTeX XML Cite \textit{A. Bradford} et al., J. Artif. Intell. Res. (JAIR) 68, 447--461 (2020; Zbl 1445.68328) Full Text: DOI
Chen, Shiping; Liu, Zhong Automated proof of mixed trigonometric-polynomial inequalities. (English) Zbl 1444.68284 J. Symb. Comput. 101, 318-329 (2020). MSC: 68V15 26D05 PDF BibTeX XML Cite \textit{S. Chen} and \textit{Z. Liu}, J. Symb. Comput. 101, 318--329 (2020; Zbl 1444.68284) Full Text: DOI
Ishii, Daisuke; Yabu, Tomohito Computer-assisted verification of four interval arithmetic operators. (English) Zbl 1434.65063 J. Comput. Appl. Math. 377, Article ID 112893, 12 p. (2020). MSC: 65G30 68Q60 68V15 PDF BibTeX XML Cite \textit{D. Ishii} and \textit{T. Yabu}, J. Comput. Appl. Math. 377, Article ID 112893, 12 p. (2020; Zbl 1434.65063) Full Text: DOI
Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza CryptHOL: game-based proofs in higher-order logic. (English) Zbl 07194394 J. Cryptology 33, No. 2, 494-566 (2020). MSC: 94A60 94A62 68V15 91A99 PDF BibTeX XML Cite \textit{D. A. Basin} et al., J. Cryptology 33, No. 2, 494--566 (2020; Zbl 07194394) Full Text: DOI
Abrahamsson, Oskar A verified proof checker for higher-order logic. (English) Zbl 1433.68527 J. Log. Algebr. Methods Program. 112, Article ID 100530, 19 p. (2020). MSC: 68V15 03B16 PDF BibTeX XML Cite \textit{O. Abrahamsson}, J. Log. Algebr. Methods Program. 112, Article ID 100530, 19 p. (2020; Zbl 1433.68527) Full Text: DOI
Peña, Ricardo An assertional proof of red-black trees using Dafny. (English) Zbl 07187046 J. Autom. Reasoning 64, No. 4, 767-791 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{R. Peña}, J. Autom. Reasoning 64, No. 4, 767--791 (2020; Zbl 07187046) Full Text: DOI
Echenim, Mnacho; Guiol, Hervé; Peltier, Nicolas Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL. (English) Zbl 07187045 J. Autom. Reasoning 64, No. 4, 737-765 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{M. Echenim} et al., J. Autom. Reasoning 64, No. 4, 737--765 (2020; Zbl 07187045) Full Text: DOI
Divasón, Jose; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa A verified implementation of the Berlekamp-Zassenhaus factorization algorithm. (English) Zbl 07187044 J. Autom. Reasoning 64, No. 4, 699-735 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{J. Divasón} et al., J. Autom. Reasoning 64, No. 4, 699--735 (2020; Zbl 07187044) Full Text: DOI
Moghaddam, G. I.; Padmanabhan, R.; Zhang, Yang Automated reasoning with power maps. (English) Zbl 07187043 J. Autom. Reasoning 64, No. 4, 689-697 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{G. I. Moghaddam} et al., J. Autom. Reasoning 64, No. 4, 689--697 (2020; Zbl 07187043) Full Text: DOI
Gadgil, Siddhartha Homogeneous length functions on groups: intertwined computer and human proofs. (English) Zbl 07187042 J. Autom. Reasoning 64, No. 4, 677-688 (2020). MSC: 68V15 03B15 20F12 20F65 PDF BibTeX XML Cite \textit{S. Gadgil}, J. Autom. Reasoning 64, No. 4, 677--688 (2020; Zbl 07187042) Full Text: DOI
Gheri, Lorenzo; Popescu, Andrei A formalized general theory of syntax with bindings: extended version. (English) Zbl 07187041 J. Autom. Reasoning 64, No. 4, 641-675 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{L. Gheri} and \textit{A. Popescu}, J. Autom. Reasoning 64, No. 4, 641--675 (2020; Zbl 07187041) Full Text: DOI
Kirchner, Daniel; Benzmüller, Christoph; Zalta, Edward N. Mechanizing Principia Logico-Metaphysica in functional type-theory. (English) Zbl 07181947 Rev. Symb. Log. 13, No. 1, 206-218 (2020). MSC: 03A05 03B35 03B45 03B60 03B80 68V15 68T27 68T30 PDF BibTeX XML Cite \textit{D. Kirchner} et al., Rev. Symb. Log. 13, No. 1, 206--218 (2020; Zbl 07181947) Full Text: DOI
Bromberger, Martin; Sturm, Thomas; Weidenbach, Christoph A complete and terminating approach to linear integer solving. (English) Zbl 1432.68597 J. Symb. Comput. 100, 102-136 (2020). MSC: 68W30 68Q60 68R07 68V15 90C10 PDF BibTeX XML Cite \textit{M. Bromberger} et al., J. Symb. Comput. 100, 102--136 (2020; Zbl 1432.68597) Full Text: DOI
Teucke, Andreas; Weidenbach, Christoph SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment. (English) Zbl 07176612 J. Autom. Reasoning 64, No. 3, 611-640 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{A. Teucke} and \textit{C. Weidenbach}, J. Autom. Reasoning 64, No. 3, 611--640 (2020; Zbl 07176612) Full Text: DOI
Bonacina, Maria Paola; Graham-Lengrand, Stéphane; Shankar, Natarajan Conflict-driven satisfiability for theory combination: transition system and completeness. (English) Zbl 07176611 J. Autom. Reasoning 64, No. 3, 579-609 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{M. P. Bonacina} et al., J. Autom. Reasoning 64, No. 3, 579--609 (2020; Zbl 07176611) Full Text: DOI
Tellez, Gadi; Brotherston, James Automatically verifying temporal properties of pointer programs with cyclic proof. (English) Zbl 07176610 J. Autom. Reasoning 64, No. 3, 555-578 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{G. Tellez} and \textit{J. Brotherston}, J. Autom. Reasoning 64, No. 3, 555--578 (2020; Zbl 07176610) Full Text: DOI
Heule, Marijn J. H.; Kiesl, Benjamin; Biere, Armin Strong extension-free proof systems. (English) Zbl 07176609 J. Autom. Reasoning 64, No. 3, 533-554 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{M. J. H. Heule} et al., J. Autom. Reasoning 64, No. 3, 533--554 (2020; Zbl 07176609) Full Text: DOI
Lammich, Peter Efficient verified (UN)SAT certificate checking. (English) Zbl 07176608 J. Autom. Reasoning 64, No. 3, 513-532 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{P. Lammich}, J. Autom. Reasoning 64, No. 3, 513--532 (2020; Zbl 07176608) Full Text: DOI
Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal Scalable fine-grained proofs for formula processing. (English) Zbl 07176606 J. Autom. Reasoning 64, No. 3, 485-510 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{H. Barbosa} et al., J. Autom. Reasoning 64, No. 3, 485--510 (2020; Zbl 07176606) Full Text: DOI
Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments. (English) Zbl 07176605 J. Autom. Reasoning 64, No. 3, 461-484 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{C. Nalon} et al., J. Autom. Reasoning 64, No. 3, 461--484 (2020; Zbl 07176605) Full Text: DOI
Sebastiani, Roberto; Trentin, Patrick OptiMathSAT: a tool for optimization modulo theories. (English) Zbl 07176604 J. Autom. Reasoning 64, No. 3, 423-460 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{R. Sebastiani} and \textit{P. Trentin}, J. Autom. Reasoning 64, No. 3, 423--460 (2020; Zbl 07176604) Full Text: DOI
Kaufmann, Matt; Moore, J. Strother Limited second-order functionality in a first-order setting. (English) Zbl 07176603 J. Autom. Reasoning 64, No. 3, 391-422 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{M. Kaufmann} and \textit{J. S. Moore}, J. Autom. Reasoning 64, No. 3, 391--422 (2020; Zbl 07176603) Full Text: DOI
Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa A verified implementation of algebraic numbers in Isabelle/HOL. (English) Zbl 07176602 J. Autom. Reasoning 64, No. 3, 363-389 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{S. J. C. Joosten} et al., J. Autom. Reasoning 64, No. 3, 363--389 (2020; Zbl 07176602) Full Text: DOI
Li, Wenda; Paulson, Lawrence C. Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL. (English) Zbl 07176600 J. Autom. Reasoning 64, No. 2, 331-360 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{W. Li} and \textit{L. C. Paulson}, J. Autom. Reasoning 64, No. 2, 331--360 (2020; Zbl 07176600) Full Text: DOI
Cristiá, Maximiliano; Rossi, Gianfranco Solving quantifier-free first-order constraints over finite sets and binary relations. (English) Zbl 07176599 J. Autom. Reasoning 64, No. 2, 295-330 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{M. Cristiá} and \textit{G. Rossi}, J. Autom. Reasoning 64, No. 2, 295--330 (2020; Zbl 07176599) Full Text: DOI
Echenim, M.; Peltier, N. Combining induction and saturation-based theorem proving. (English) Zbl 07176598 J. Autom. Reasoning 64, No. 2, 253-294 (2020). MSC: 68V15 03B35 PDF BibTeX XML Cite \textit{M. Echenim} and \textit{N. Peltier}, J. Autom. Reasoning 64, No. 2, 253--294 (2020; Zbl 07176598) Full Text: DOI
Baumgartner, Peter; Schmidt, Renate A. Blocking and other enhancements for bottom-up model generation methods. (English) Zbl 07176597 J. Autom. Reasoning 64, No. 2, 197-251 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{P. Baumgartner} and \textit{R. A. Schmidt}, J. Autom. Reasoning 64, No. 2, 197--251 (2020; Zbl 07176597) Full Text: DOI
Lucas, Salvador Using well-founded relations for proving operational termination. (English) Zbl 07176596 J. Autom. Reasoning 64, No. 2, 167-195 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{S. Lucas}, J. Autom. Reasoning 64, No. 2, 167--195 (2020; Zbl 07176596) Full Text: DOI
Cialdea Mayer, Marta A prover dealing with nominals, binders, transitivity and relation hierarchies. (English) Zbl 07176595 J. Autom. Reasoning 64, No. 1, 135-165 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{M. Cialdea Mayer}, J. Autom. Reasoning 64, No. 1, 135--165 (2020; Zbl 07176595) Full Text: DOI
Chocron, Paula; Fontaine, Pascal; Ringeissen, Christophe Politeness and combination methods for theories with bridging functions. (English) Zbl 07176594 J. Autom. Reasoning 64, No. 1, 97-134 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{P. Chocron} et al., J. Autom. Reasoning 64, No. 1, 97--134 (2020; Zbl 07176594) Full Text: DOI
Zhang, Xingyuan; Urban, Christian; Wu, Chunhan Priority inheritance protocol proved correct. (English) Zbl 07176593 J. Autom. Reasoning 64, No. 1, 73-95 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{X. Zhang} et al., J. Autom. Reasoning 64, No. 1, 73--95 (2020; Zbl 07176593) Full Text: DOI
Benzmüller, Christoph; Scott, Dana S. Automating free logic in HOL, with an experimental application in category theory. (English) Zbl 1434.68639 J. Autom. Reasoning 64, No. 1, 53-72 (2020). MSC: 68V15 03B16 03B35 03B60 18A15 PDF BibTeX XML Cite \textit{C. Benzmüller} and \textit{D. S. Scott}, J. Autom. Reasoning 64, No. 1, 53--72 (2020; Zbl 1434.68639) Full Text: DOI
Nguyen, Linh Anh ExpTime tableaux with global caching for hybrid PDL. (English) Zbl 07176591 J. Autom. Reasoning 64, No. 1, 21-52 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{L. A. Nguyen}, J. Autom. Reasoning 64, No. 1, 21--52 (2020; Zbl 07176591) Full Text: DOI
Huang, Cheng-Chao; Xu, Ming; Li, Zhi-Bin A conflict-driven solving procedure for poly-power constraints. (English) Zbl 07176590 J. Autom. Reasoning 64, No. 1, 1-20 (2020). MSC: 68V15 PDF BibTeX XML Cite \textit{C.-C. Huang} et al., J. Autom. Reasoning 64, No. 1, 1--20 (2020; Zbl 07176590) Full Text: DOI
Roffé, Ariel Jonathan Reconstructor: a computer program that uses three-valued logics to represent lack of information in empirical scientific contexts. (English) Zbl 1444.68288 J. Appl. Non-Class. Log. 30, No. 1, 68-91 (2020). MSC: 68V15 03B50 70A05 PDF BibTeX XML Cite \textit{A. J. Roffé}, J. Appl. Non-Class. Log. 30, No. 1, 68--91 (2020; Zbl 1444.68288) Full Text: DOI
Berkholz, Christoph; Nordström, Jakob Supercritical space-width trade-offs for resolution. (English) Zbl 07166152 SIAM J. Comput. 49, No. 1, 98-118 (2020). MSC: 03B70 03D15 03F20 68Q15 68Q17 68V15 PDF BibTeX XML Cite \textit{C. Berkholz} and \textit{J. Nordström}, SIAM J. Comput. 49, No. 1, 98--118 (2020; Zbl 07166152) Full Text: DOI
Beyersdorff, Olaf; Blinkhorn, Joshua Dynamic QBF dependencies in reduction and expansion. (English) Zbl 1433.03138 ACM Trans. Comput. Log. 21, No. 2, Article No. 8, 27 p. (2020). MSC: 03F20 68Q17 68V15 PDF BibTeX XML Cite \textit{O. Beyersdorff} and \textit{J. Blinkhorn}, ACM Trans. Comput. Log. 21, No. 2, Article No. 8, 27 p. (2020; Zbl 1433.03138) Full Text: DOI
Foster, Simon; Cavalcanti, Ana; Canham, Samuel; Woodcock, Jim; Zeyda, Frank Unifying theories of reactive design contracts. (English) Zbl 1436.68195 Theor. Comput. Sci. 802, 105-140 (2020). MSC: 68Q60 68Q55 68V15 PDF BibTeX XML Cite \textit{S. Foster} et al., Theor. Comput. Sci. 802, 105--140 (2020; Zbl 1436.68195) Full Text: DOI
Dana-Picard, Thierry An automated study of isoptic curves of an astroid. (English) Zbl 1444.68302 J. Symb. Comput. 97, 56-68 (2020). MSC: 68W30 13P10 68U05 68V15 PDF BibTeX XML Cite \textit{T. Dana-Picard}, J. Symb. Comput. 97, 56--68 (2020; Zbl 1444.68302) Full Text: DOI
Quaresma, Pedro; Santos, Vanda; Graziani, Pierluigi; Baeta, Nuno Taxonomies of geometric problems. (English) Zbl 1444.68292 J. Symb. Comput. 97, 31-55 (2020). MSC: 68V30 68U05 68V15 68V35 PDF BibTeX XML Cite \textit{P. Quaresma} et al., J. Symb. Comput. 97, 31--55 (2020; Zbl 1444.68292) Full Text: DOI
Kovács, Zoltán; Recio, Tomás; Vélez, M. Pilar Reasoning about linkages with dynamic geometry. (English) Zbl 1440.68341 J. Symb. Comput. 97, 16-30 (2020). Reviewer: Nelly Villamizar (Swansea) MSC: 68W30 51M15 68U05 68V15 70B15 PDF BibTeX XML Cite \textit{Z. Kovács} et al., J. Symb. Comput. 97, 16--30 (2020; Zbl 1440.68341) Full Text: DOI
Hanna, Gila (ed.); Reid, David A. (ed.); De Villiers, Michael (ed.) Proof technology in mathematics research and teaching. (English) Zbl 1451.97008 Mathematics Education in the Digital Era 14. Cham: Springer (ISBN 978-3-030-28482-4/hbk; 978-3-030-28485-5/pbk; 978-3-030-28483-1/ebook). viii, 379 p. (2019). MSC: 97-06 97U50 97E50 68V15 00B15 PDF BibTeX XML Cite \textit{G. Hanna} (ed.) et al., Proof technology in mathematics research and teaching. Cham: Springer (2019; Zbl 1451.97008) Full Text: DOI
Hart, K. P. Machine learning and the continuum hypothesis. (English) Zbl 1446.03085 Nieuw Arch. Wiskd. (5) 20, No. 3, 214-217 (2019). MSC: 03E50 03E10 03D35 68V15 PDF BibTeX XML Cite \textit{K. P. Hart}, Nieuw Arch. Wiskd. (5) 20, No. 3, 214--217 (2019; Zbl 1446.03085)
Rieu-Helft, Raphaël A Why3 proof of GMP algorithms. (English) Zbl 1451.68342 J. Formaliz. Reason. 12, No. 1, 53-97 (2019). MSC: 68V20 68Q60 68V15 PDF BibTeX XML Cite \textit{R. Rieu-Helft}, J. Formaliz. Reason. 12, No. 1, 53--97 (2019; Zbl 1451.68342) Full Text: DOI
Eberl, Manuel Verified real asymptotics in Isabelle/HOL. (English) Zbl 07246241 Bradford, Russell (ed.), Proceedings of the 44th international symposium on symbolic and algebraic computation, ISSAC ’19, Beijing, China, July 15–18, 2019. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-6084-5). 147-154 (2019). MSC: 68W30 PDF BibTeX XML Cite \textit{M. Eberl}, in: Proceedings of the 44th international symposium on symbolic and algebraic computation, ISSAC '19, Beijing, China, July 15--18, 2019. New York, NY: Association for Computing Machinery (ACM). 147--154 (2019; Zbl 07246241) Full Text: DOI
Augusto, Luis M. Formal logic. Classical problems and proofs. (English) Zbl 1451.03001 Studies in Logic (London) 82. London: College Publications (ISBN 978-1-84890-317-3). xix, 404 p. (2019). MSC: 03-01 03A05 03B10 03B25 03B35 68V15 PDF BibTeX XML Cite \textit{L. M. Augusto}, Formal logic. Classical problems and proofs. London: College Publications (2019; Zbl 1451.03001)
Alvarez, Aurélien Prime numbers, Euclid and Coq. (Nombres premiers, Euclide et Coq.) (French) Zbl 1439.11018 Quadrature 111, 25-30 (2019). MSC: 11A41 11-04 68V15 68V20 PDF BibTeX XML Cite \textit{A. Alvarez}, Quadrature 111, 25--30 (2019; Zbl 1439.11018)
Davis, Ernest Proof verification technology and elementary physics. (English) Zbl 07218077 Fillion, Nicolas (ed.) et al., Algorithms and complexity in mathematics, epistemology, and science. Proceedings of 2015 and 2016 ACMES conferences, London, UK. Selected papers. New York, NY: Springer; Toronto: The Fields Institute for Research in the Mathematical Sciences (ISBN 978-1-4939-9050-4/hbk; 978-1-4939-9051-1/ebook). Fields Institute Communications 82, 81-132 (2019). MSC: 68V15 PDF BibTeX XML Cite \textit{E. Davis}, Fields Inst. Commun. 82, 81--132 (2019; Zbl 07218077) Full Text: DOI
Zohar, Yoni; Tishkovsky, Dmitry; Schmidt, Renate A.; Zamansky, Anna Automating automated reasoning. The case of two generic automated reasoning tools. (English) Zbl 1444.68290 Lutz, Carsten (ed.) et al., Description logic, theory combination, and all that. Essays dedicated to Franz Baader on the occasion of his 60th birthday. Cham: Springer. Lect. Notes Comput. Sci. 11560, 610-638 (2019). MSC: 68V15 68T20 PDF BibTeX XML Cite \textit{Y. Zohar} et al., Lect. Notes Comput. Sci. 11560, 610--638 (2019; Zbl 1444.68290) Full Text: DOI
Tena Cucala, David; Cuenca Grau, Bernardo; Horrocks, Ian 15 years of consequence-based reasoning. (English) Zbl 1444.68192 Lutz, Carsten (ed.) et al., Description logic, theory combination, and all that. Essays dedicated to Franz Baader on the occasion of his 60th birthday. Cham: Springer. Lect. Notes Comput. Sci. 11560, 573-587 (2019). MSC: 68T27 68T30 68V15 PDF BibTeX XML Cite \textit{D. Tena Cucala} et al., Lect. Notes Comput. Sci. 11560, 573--587 (2019; Zbl 1444.68192) Full Text: DOI
Baumgartner, Peter; Waldmann, Uwe Hierarchic superposition revisited. (English) Zbl 1443.68212 Lutz, Carsten (ed.) et al., Description logic, theory combination, and all that. Essays dedicated to Franz Baader on the occasion of his 60th birthday. Cham: Springer. Lect. Notes Comput. Sci. 11560, 15-56 (2019). MSC: 68V15 PDF BibTeX XML Cite \textit{P. Baumgartner} and \textit{U. Waldmann}, Lect. Notes Comput. Sci. 11560, 15--56 (2019; Zbl 1443.68212) Full Text: DOI
Lutz, Carsten; Sattler, Uli; Tinelli, Cesare; Turhan, Anni-Yasmin; Wolter, Frank A tour of Franz Baader’s contributions to knowledge representation and automated deduction. (English) Zbl 1443.68010 Lutz, Carsten (ed.) et al., Description logic, theory combination, and all that. Essays dedicated to Franz Baader on the occasion of his 60th birthday. Cham: Springer. Lect. Notes Comput. Sci. 11560, 1-14 (2019). MSC: 68-03 01A70 68T30 68V15 PDF BibTeX XML Cite \textit{C. Lutz} et al., Lect. Notes Comput. Sci. 11560, 1--14 (2019; Zbl 1443.68010) Full Text: DOI
Abel, Andreas; Allais, Guillaume; Hameer, Aliya; Pientka, Brigitte; Momigliano, Alberto; Schäfer, Steven; Stark, Kathrin POPLMark reloaded: mechanizing proofs by logical relations. (English) Zbl 1442.68257 J. Funct. Program. 29, Paper No. e19, 43 p. (2019). MSC: 68V15 68N15 PDF BibTeX XML Cite \textit{A. Abel} et al., J. Funct. Program. 29, Paper No. e19, 43 p. (2019; Zbl 1442.68257) Full Text: DOI
Hamana, Makoto How to prove decidability of equational theories with second-order computation analyser SOL. (English) Zbl 1442.68027 J. Funct. Program. 29, Paper No. e20, 53 p. (2019). MSC: 68N18 03B25 03B40 03B70 18M05 68N15 68N30 68V15 PDF BibTeX XML Cite \textit{M. Hamana}, J. Funct. Program. 29, Paper No. e20, 53 p. (2019; Zbl 1442.68027) Full Text: DOI
Ozdemir, Alex; Niemetz, Aina; Preiner, Mathias; Zohar, Yoni; Barrett, Clark DRAT-based bit-vector proofs in CVC4. (English) Zbl 1441.68235 Janota, Mikoláš (ed.) et al., Theory and applications of satisfiability testing – SAT 2019. 22nd international conference, SAT 2019, Lisbon, Portugal, July 9–12, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11628, 298-305 (2019). MSC: 68T20 68V15 PDF BibTeX XML Cite \textit{A. Ozdemir} et al., Lect. Notes Comput. Sci. 11628, 298--305 (2019; Zbl 1441.68235) Full Text: DOI
Chew, Leroy; Clymo, Judith The equivalences of refutational QRAT. (English) Zbl 1441.68154 Janota, Mikoláš (ed.) et al., Theory and applications of satisfiability testing – SAT 2019. 22nd international conference, SAT 2019, Lisbon, Portugal, July 9–12, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11628, 100-116 (2019). MSC: 68R07 03F20 68V15 PDF BibTeX XML Cite \textit{L. Chew} and \textit{J. Clymo}, Lect. Notes Comput. Sci. 11628, 100--116 (2019; Zbl 1441.68154) Full Text: DOI
Goertzel, Zarathustra; Jakubův, Jan; Urban, Josef ENIGMAWatch: ProofWatch meets ENIGMA. (English) Zbl 1435.68370 Cerrito, Serenella (ed.) et al., Automated reasoning with analytic tableaux and related methods. 28th international conference, TABLEAUX 2019, London, UK, September 3–5, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11714, 374-388 (2019). MSC: 68V15 68T05 PDF BibTeX XML Cite \textit{Z. Goertzel} et al., Lect. Notes Comput. Sci. 11714, 374--388 (2019; Zbl 1435.68370) Full Text: DOI