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
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
Runge, Tobias; Bordis, Tabea; Potanin, Alex; Thüm, Thomas; Schaefer, Ina Flexible correct-by-construction programming. (English) Zbl 07731927 Log. Methods Comput. Sci. 19, No. 2, Paper No. 16, 36 p. (2023). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{T. Runge} et al., Log. Methods Comput. Sci. 19, No. 2, Paper No. 16, 36 p. (2023; Zbl 07731927) Full Text: DOI arXiv
Blanchette, Jasmin; Vukmirović, Petar SAT-inspired higher-order eliminations. (English) Zbl 07731920 Log. Methods Comput. Sci. 19, No. 2, Paper No. 9, 23 p. (2023). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{J. Blanchette} and \textit{P. Vukmirović}, Log. Methods Comput. Sci. 19, No. 2, Paper No. 9, 23 p. (2023; Zbl 07731920) Full Text: DOI arXiv
Mehdipour, Noushin; Althoff, Matthias; Tebbens, Radboud Duintjer; Belta, Calin Formal methods to comply with rules of the road in autonomous driving: state of the art and grand challenges. (English) Zbl 1519.93159 Automatica 152, Article ID 110692, 15 p. (2023). MSC: 93C85 93B03 03B44 93B50 PDFBibTeX XMLCite \textit{N. Mehdipour} et al., Automatica 152, Article ID 110692, 15 p. (2023; Zbl 1519.93159) 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
Konnov, Igor; Lazić, Marijana; Stoilkovska, Ilina; Widder, Josef Survey on parameterized verification with threshold automata and the Byzantine Model Checker. (English) Zbl 07667095 Log. Methods Comput. Sci. 19, No. 1, Paper No. 5, 25 p. (2023). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{I. Konnov} et al., Log. Methods Comput. Sci. 19, No. 1, Paper No. 5, 25 p. (2023; Zbl 07667095) 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
Singh, Lavanya Automated Kantian ethics: a faithful implementation. (English) Zbl 1522.68442 Bergmann, Ralph (ed.) et al., KI 2022: advances in artificial intelligence. 45th German conference on AI, Trier, Germany, September 19–23, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13404, 187-208 (2022). MSC: 68T01 03A05 03B45 68V20 PDFBibTeX XMLCite \textit{L. Singh}, Lect. Notes Comput. Sci. 13404, 187--208 (2022; Zbl 1522.68442) Full Text: DOI arXiv
Mantovani, Marco; Momigliano, Alberto Towards substructural property-based testing. (English) Zbl 1521.68035 De Angelis, Emanuele (ed.) et al., Logic-based program synthesis and transformation. 31st international symposium, LOPSTR 2021, Tallinn, Estonia, September 7–8, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13290, 92-112 (2022). MSC: 68N30 03B47 68N15 68Q55 68W20 PDFBibTeX XMLCite \textit{M. Mantovani} and \textit{A. Momigliano}, Lect. Notes Comput. Sci. 13290, 92--112 (2022; Zbl 1521.68035) Full Text: DOI arXiv
Wolter, U. E.; Martini, A. R.; Häusler, E. H. Indexed and fibered structures for partial and total correctness assertions. (English) Zbl 1512.68060 Math. Struct. Comput. Sci. 32, No. 9, 1145-1175 (2022). MSC: 68N30 03B70 03G30 18D30 PDFBibTeX XMLCite \textit{U. E. Wolter} et al., Math. Struct. Comput. Sci. 32, No. 9, 1145--1175 (2022; Zbl 1512.68060) Full Text: DOI
Sadykov, R. F.; Mandrykin, M. U. Complete decision procedure for the theory of bounded pointer arithmetic. (English) Zbl 1517.68082 Program. Comput. Softw. 48, No. 8, 770-780 (2022). MSC: 68N30 03B70 68V20 PDFBibTeX XMLCite \textit{R. F. Sadykov} and \textit{M. U. Mandrykin}, Program. Comput. Softw. 48, No. 8, 770--780 (2022; Zbl 1517.68082) 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)
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
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 PDFBibTeX XMLCite \textit{G. S. Schmid} and \textit{V. Kunčak}, Lect. Notes Comput. Sci. 13182, 332--354 (2022; Zbl 1498.68172) Full Text: DOI
Dubut, Jérémy; Yamada, Akihisa Fixed points theorems for non-transitive relations. (English) Zbl 07471719 Log. Methods Comput. Sci. 18, No. 1, Paper No. 30, 24 p. (2022). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{J. Dubut} and \textit{A. Yamada}, Log. Methods Comput. Sci. 18, No. 1, Paper No. 30, 24 p. (2022; Zbl 07471719) Full Text: arXiv Link
Fürer, Basil; Lochbihler, Andreas; Schneider, Joshua; Traytel, Dmitriy Quotients of bounded natural functors. (English) Zbl 07471712 Log. Methods Comput. Sci. 18, No. 1, Paper No. 23, 28 p. (2022). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{B. Fürer} et al., Log. Methods Comput. Sci. 18, No. 1, Paper No. 23, 28 p. (2022; Zbl 07471712) Full Text: arXiv Link
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)
From, Asta Halkjær Formalized soundness and completeness of epistemic logic. (English) Zbl 07547730 Silva, Alexandra (ed.) et al., Logic, language, information, and computation. 27th international workshop, WoLLIC 2021, virtual event, October 5–8, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13038, 1-15 (2021). MSC: 03B70 PDFBibTeX XMLCite \textit{A. H. From}, Lect. Notes Comput. Sci. 13038, 1--15 (2021; Zbl 07547730) Full Text: DOI Link
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
From, Asta Halkjær; Eschen, Agnes Moesgård; Villadsen, Jørgen Formalizing axiomatic systems for propositional logic in Isabelle/HOL. (English) Zbl 1485.68292 Kamareddine, Fairouz (ed.) et al., Intelligent computer mathematics. 14th international conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12833, 32-46 (2021). MSC: 68V20 03B05 03B20 PDFBibTeX XMLCite \textit{A. H. From} et al., Lect. Notes Comput. Sci. 12833, 32--46 (2021; Zbl 1485.68292) Full Text: DOI Link
Streit, David Experiments in causality and STIT. (English) Zbl 1484.68314 Liao, Beishui (ed.) et al., Logics for new-generation AI 2021. First international workshop, LNGAI 2021, June, 18–20 2021, Hangzhou, China. London: College Publications. 33-45 (2021). MSC: 68V15 03B42 68T27 PDFBibTeX XMLCite \textit{D. Streit}, in: Logics for new-generation AI 2021. First international workshop, LNGAI 2021, June, 18--20 2021, Hangzhou, China. London: College Publications. 33--45 (2021; Zbl 1484.68314)
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
Siek, Jeremy G.; Chen, Tianyu Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi. (English) Zbl 07453898 J. Funct. Program. 31, Paper No. e30, 73 p. (2021). MSC: 68N18 03B40 68V20 PDFBibTeX XMLCite \textit{J. G. Siek} and \textit{T. Chen}, J. Funct. Program. 31, Paper No. e30, 73 p. (2021; Zbl 07453898) Full Text: DOI arXiv
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
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
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
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
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
Steen, Alexander; Benzmüller, Christoph Extensional higher-order paramodulation in Leo-III. (English) Zbl 1509.68321 J. Autom. Reasoning 65, No. 6, 775-807 (2021). MSC: 68V15 03B16 03B35 03B45 PDFBibTeX XMLCite \textit{A. Steen} and \textit{C. Benzmüller}, J. Autom. Reasoning 65, No. 6, 775--807 (2021; Zbl 1509.68321) Full Text: DOI arXiv
Bordg, Anthony; Lachnitt, Hanna; He, Yijun Certified quantum computation in Isabelle/HOL. (English) Zbl 07432184 J. Autom. Reasoning 65, No. 5, 691-709 (2021). MSC: 03B35 03B15 81P68 68Q12 PDFBibTeX XMLCite \textit{A. Bordg} et al., J. Autom. Reasoning 65, No. 5, 691--709 (2021; Zbl 07432184) Full Text: DOI arXiv
Tan, Yong Kiam; Platzer, André Deductive stability proofs for ordinary differential equations. (English) Zbl 1474.68195 Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12652, 181-199 (2021). MSC: 68Q60 03B70 34D99 68V20 93C15 PDFBibTeX XMLCite \textit{Y. K. Tan} and \textit{A. Platzer}, Lect. Notes Comput. Sci. 12652, 181--199 (2021; Zbl 1474.68195) Full Text: DOI arXiv
Chan, Hing Lun; Norrish, Michael Mechanisation of the AKS algorithm. (English) Zbl 1465.68301 J. Autom. Reasoning 65, No. 2, 205-256 (2021). MSC: 68V20 03B35 11A51 11Y11 11Y16 68Q25 PDFBibTeX XMLCite \textit{H. L. Chan} and \textit{M. Norrish}, J. Autom. Reasoning 65, No. 2, 205--256 (2021; Zbl 1465.68301) Full Text: DOI
Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Waldmann, Uwe Superposition for lambda-free higher-order logic. (English) Zbl 07350767 Log. Methods Comput. Sci. 17, No. 2, Paper No. 1, 38 p. (2021). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{A. Bentkamp} et al., Log. Methods Comput. Sci. 17, No. 2, Paper No. 1, 38 p. (2021; Zbl 07350767) Full Text: arXiv Link
Koutsoukou-Argyraki, Angeliki Formalising mathematics – in praxis; a mathematician’s first experiences with Isabelle/HOL and the why and how of getting started. (English) Zbl 1495.68241 Jahresber. Dtsch. Math.-Ver. 123, No. 1, 3-26 (2021). Reviewer: Truong Hoang Le (Hanoi) MSC: 68V20 03B35 68V15 68V35 PDFBibTeX XMLCite \textit{A. Koutsoukou-Argyraki}, Jahresber. Dtsch. Math.-Ver. 123, No. 1, 3--26 (2021; Zbl 1495.68241) Full Text: DOI Backlinks: MO
Rusu, Vlad; Nowak, David (Co)inductive proof systems for compositional proofs in reachability logic. (English) Zbl 1455.03040 J. Log. Algebr. Methods Program. 118, Article ID 100619, 28 p. (2021). MSC: 03B70 68V20 PDFBibTeX XMLCite \textit{V. Rusu} and \textit{D. Nowak}, J. Log. Algebr. Methods Program. 118, Article ID 100619, 28 p. (2021; Zbl 1455.03040) Full Text: DOI arXiv
Tiemens, Lucca; Scott, Dana S.; Benzmüller, Christoph; Benda, Miroslav Computer-supported exploration of a categorical axiomatization of modeloids. (English) Zbl 1509.68328 Fahrenberg, Uli (ed.) et al., Relational and algebraic methods in computer science. 18th international conference, RAMiCS 2020, Palaiseau, France, October 26–29, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12062, 302-317 (2020). MSC: 68V20 03B35 03C07 03C99 18A15 20M18 PDFBibTeX XMLCite \textit{L. Tiemens} et al., Lect. Notes Comput. Sci. 12062, 302--317 (2020; Zbl 1509.68328) Full Text: DOI arXiv
Ribeiro, Maria; Adão, Pedro; Mateus, Paulo Formal verification of Ethereum smart contracts using Isabelle/HOL. (English) Zbl 1476.68156 Nigam, Vivek (ed.) et al., Logic, language, and security. Essays dedicated to Andre Scedrov on the occasion of his 65th birthday. Cham: Springer. Lect. Notes Comput. Sci. 12300, 71-97 (2020). MSC: 68Q60 03B70 68V15 91B41 94A60 PDFBibTeX XMLCite \textit{M. Ribeiro} et al., Lect. Notes Comput. Sci. 12300, 71--97 (2020; Zbl 1476.68156) Full Text: DOI
Carnielli, Walter; Fuenmayor, David Gödel’s incompleteness theorems from a paraconsistent perspective. (English) Zbl 1487.03069 Costa-Leite, Alexandre (ed.), Abstract consequence and logics. Essays in honor of Edelcio G. de Souza. London: College Publications. Tributes 42, 173-197 (2020). MSC: 03F40 03B53 PDFBibTeX XMLCite \textit{W. Carnielli} and \textit{D. Fuenmayor}, Tributes 42, 173--197 (2020; Zbl 1487.03069)
Sickert, Salomon; Esparza, Javier An efficient normalisation procedure for linear temporal logic and very weak alternating automata. (English) Zbl 07299516 Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM). 831-844 (2020). MSC: 68-XX 03B44 PDFBibTeX XMLCite \textit{S. Sickert} and \textit{J. Esparza}, in: Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8--11, 2020. New York, NY: Association for Computing Machinery (ACM). 831--844 (2020; Zbl 07299516) Full Text: DOI arXiv
Benzmüller, Christoph; Parent, Xavier; van der Torre, Leendert Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support. (English) Zbl 1493.68286 Artif. Intell. 287, Article ID 103348, 28 p. (2020). MSC: 68T01 03A05 03B16 03B35 03B45 68T27 68T30 68V15 PDFBibTeX XMLCite \textit{C. Benzmüller} et al., Artif. Intell. 287, Article ID 103348, 28 p. (2020; Zbl 1493.68286) Full Text: DOI arXiv
Berghammer, Rudolf; Furusawa, Hitoshi; Guttmann, Walter; Höfner, Peter Relational characterisations of paths. (English) Zbl 1462.05198 J. Log. Algebr. Methods Program. 117, Article ID 100590, 19 p. (2020). MSC: 05C38 03B35 03G15 05C85 68V15 PDFBibTeX XMLCite \textit{R. Berghammer} et al., J. Log. Algebr. Methods Program. 117, Article ID 100590, 19 p. (2020; Zbl 1462.05198) Full Text: DOI arXiv
Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; Waldmann, Uwe Formalizing Bachmair and Ganzinger’s ordered resolution prover. (English) Zbl 1468.68307 J. Autom. Reasoning 64, No. 7, 1169-1195 (2020). MSC: 68V15 03B35 68V20 PDFBibTeX XMLCite \textit{A. Schlichtkrull} et al., J. Autom. Reasoning 64, No. 7, 1169--1195 (2020; Zbl 1468.68307) Full Text: DOI Link
Syeda, Hira Taqdees; Klein, Gerwin Formal reasoning under cached address translation. (English) Zbl 1468.68070 J. Autom. Reasoning 64, No. 5, 911-945 (2020). MSC: 68N25 03B70 68N30 68V15 PDFBibTeX XMLCite \textit{H. T. Syeda} and \textit{G. Klein}, J. Autom. Reasoning 64, No. 5, 911--945 (2020; Zbl 1468.68070) Full Text: DOI
Benzmüller, Christoph; Fuenmayor, David Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel’s ontological argument. (English) Zbl 1461.03021 Bull. Sect. Log., Univ. Łódź, Dep. Log. 49, No. 2, 127-148 (2020). MSC: 03B45 03B35 03-08 PDFBibTeX XMLCite \textit{C. Benzmüller} and \textit{D. Fuenmayor}, Bull. Sect. Log., Univ. Łódź, Dep. Log. 49, No. 2, 127--148 (2020; Zbl 1461.03021) Full Text: DOI arXiv
Sternagel, Christian A mechanized proof of Higman’s lemma by open induction. (English) Zbl 1446.68188 Schuster, Peter M. (ed.) et al., Well-quasi orders in computation, logic, language and reasoning. A unifying concept of proof theory, automata theory, formal languages and descriptive set theory. Based on the minisymposium on well-quasi orders: from theory to applications within the Jahrestagung der Deutschen Mathematiker-Vereinigung (DMV), Hamburg, Germany, September 21–25, 2015 and the Dagstuhl seminar 16031 on well quasi-orders in computer science, Schloss Dagstuhl, Germany, January 17–22, 2016. Cham: Springer. Trends Log. Stud. Log. Libr. 53, 339-350 (2020). MSC: 68V20 03B35 03E05 PDFBibTeX XMLCite \textit{C. Sternagel}, Trends Log. Stud. Log. Libr. 53, 339--350 (2020; Zbl 1446.68188) 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 PDFBibTeX XMLCite \textit{O. Abrahamsson}, J. Log. Algebr. Methods Program. 112, Article ID 100530, 19 p. (2020; Zbl 1433.68527) 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 1469.68165 J. Autom. Reasoning 64, No. 4, 699-735 (2020). MSC: 68V15 03B35 12-08 13P05 68V20 PDFBibTeX XMLCite \textit{J. Divasón} et al., J. Autom. Reasoning 64, No. 4, 699--735 (2020; Zbl 1469.68165) Full Text: DOI
Kirchner, Daniel; Benzmüller, Christoph; Zalta, Edward N. Mechanizing Principia logico-metaphysica in functional type-theory. (English) Zbl 1484.03020 Rev. Symb. Log. 13, No. 1, 206-218 (2020). MSC: 03B35 03A05 03B38 03B45 68V15 PDFBibTeX XMLCite \textit{D. Kirchner} et al., Rev. Symb. Log. 13, No. 1, 206--218 (2020; Zbl 1484.03020) Full Text: DOI arXiv
Cristiá, Maximiliano; Rossi, Gianfranco Solving quantifier-free first-order constraints over finite sets and binary relations. (English) Zbl 1468.03009 J. Autom. Reasoning 64, No. 2, 295-330 (2020). MSC: 03B35 68N17 68V15 PDFBibTeX XMLCite \textit{M. Cristiá} and \textit{G. Rossi}, J. Autom. Reasoning 64, No. 2, 295--330 (2020; Zbl 1468.03009) 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 PDFBibTeX XMLCite \textit{C. Benzmüller} and \textit{D. S. Scott}, J. Autom. Reasoning 64, No. 1, 53--72 (2020; Zbl 1434.68639) Full Text: DOI Link
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 PDFBibTeX XMLCite \textit{A. J. Roffé}, J. Appl. Non-Class. Log. 30, No. 1, 68--91 (2020; Zbl 1444.68288) Full Text: DOI
Paulson, Lawrence C. Formalising mathematics in simple type theory. (English) Zbl 1528.03098 Centrone, Stefania (ed.) et al., Reflections on the foundations of mathematics. Univalent foundations, set theory and general thoughts. Based on the conference on foundations of mathematics: univalent foundations and set theory, FOMUS, Bielefeld, Germany, July 18–23, 2016. Cham: Springer. Synth. Libr. 407, 437-453 (2019). MSC: 03B35 03A05 03B38 68V20 PDFBibTeX XMLCite \textit{L. C. Paulson}, Synth. Libr. 407, 437--453 (2019; Zbl 1528.03098) Full Text: DOI arXiv
Ebner, Gabriel Herbrand constructivization for automated intuitionistic theorem proving. (English) Zbl 1435.68364 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, 355-373 (2019). MSC: 68V15 03B20 03B35 PDFBibTeX XMLCite \textit{G. Ebner}, Lect. Notes Comput. Sci. 11714, 355--373 (2019; Zbl 1435.68364) Full Text: DOI
Sternagel, Christian; Winkler, Sarah Certified equational reasoning via ordered completion. (English) Zbl 07178995 Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 508-525 (2019). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{C. Sternagel} and \textit{S. Winkler}, Lect. Notes Comput. Sci. 11716, 508--525 (2019; Zbl 07178995) Full Text: DOI
Popescu, Andrei; Traytel, Dmitriy A formally verified abstract account of Gödel’s incompleteness theorems. (English) Zbl 07178991 Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 442-461 (2019). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{A. Popescu} and \textit{D. Traytel}, Lect. Notes Comput. Sci. 11716, 442--461 (2019; Zbl 07178991) Full Text: DOI Link
Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Zohar, Yoni; Barrett, Clark; Tinelli, Cesare Towards bit-width-independent proofs in SMT solvers. (English) Zbl 07178987 Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 366-384 (2019). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{A. Niemetz} et al., Lect. Notes Comput. Sci. 11716, 366--384 (2019; Zbl 07178987) Full Text: DOI arXiv
Chvalovský, Karel; Jakubův, Jan; Suda, Martin; Urban, Josef ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\). (English) Zbl 07178977 Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 197-215 (2019). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{K. Chvalovský} et al., Lect. Notes Comput. Sci. 11716, 197--215 (2019; Zbl 07178977) Full Text: DOI arXiv
Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef GRUNGE: a grand unified ATP challenge. (English) Zbl 07178973 Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 123-141 (2019). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{C. E. Brown} et al., Lect. Notes Comput. Sci. 11716, 123--141 (2019; Zbl 07178973) Full Text: DOI arXiv
Bohrer, Brandon; Fernández, Manuel; Platzer, André \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic. (English) Zbl 07178971 Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 94-110 (2019). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{B. Bohrer} et al., Lect. Notes Comput. Sci. 11716, 94--110 (2019; Zbl 07178971) Full Text: DOI
Barbosa, Haniel; Reynolds, Andrew; El Ouraoui, Daniel; Tinelli, Cesare; Barrett, Clark Extending SMT solvers to higher-order logic. (English) Zbl 07178968 Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 35-54 (2019). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{H. Barbosa} et al., Lect. Notes Comput. Sci. 11716, 35--54 (2019; Zbl 07178968) Full Text: DOI HAL
Brown, Chad E.; Pąk, Karol A tale of two set theories. (English) Zbl 1428.68348 Kaliszyk, Cezary (ed.) et al., Intelligent computer mathematics. 12th international conference, CICM 2019, Prague, Czech Republic, July 8–12, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11617, 44-60 (2019). MSC: 68V20 03B35 03E70 68V15 PDFBibTeX XMLCite \textit{C. E. Brown} and \textit{K. Pąk}, Lect. Notes Comput. Sci. 11617, 44--60 (2019; Zbl 1428.68348) Full Text: DOI arXiv
Miller, Dale Mechanized metatheory revisited. (English) Zbl 1468.68303 J. Autom. Reasoning 63, No. 3, 625-665 (2019). MSC: 68V15 03B35 PDFBibTeX XMLCite \textit{D. Miller}, J. Autom. Reasoning 63, No. 3, 625--665 (2019; Zbl 1468.68303) Full Text: DOI HAL
Kaliszyk, Cezary; Pąk, Karol Semantics of Mizar as an Isabelle object logic. (English) Zbl 1468.68290 J. Autom. Reasoning 63, No. 3, 557-595 (2019). MSC: 68V15 03B35 PDFBibTeX XMLCite \textit{C. Kaliszyk} and \textit{K. Pąk}, J. Autom. Reasoning 63, No. 3, 557--595 (2019; Zbl 1468.68290) Full Text: DOI
Stojanović-Ðurđević, Sana From informal to formal proofs in Euclidean geometry. (English) Zbl 07055778 Ann. Math. Artif. Intell. 85, No. 2-4, 89-117 (2019). MSC: 03B35 68T15 PDFBibTeX XMLCite \textit{S. Stojanović-Ðurđević}, Ann. Math. Artif. Intell. 85, No. 2--4, 89--117 (2019; Zbl 07055778) Full Text: DOI
Kunčar, Ondřej; Popescu, Andrei A consistent foundation for Isabelle/HOL. (English) Zbl 1465.68289 J. Autom. Reasoning 62, No. 4, 531-555 (2019). MSC: 68V15 03B16 03B35 PDFBibTeX XMLCite \textit{O. Kunčar} and \textit{A. Popescu}, J. Autom. Reasoning 62, No. 4, 531--555 (2019; Zbl 1465.68289) Full Text: DOI Link
Immler, Fabian; Traut, Christoph The flow of ODEs: formalization of variational equation and Poincaré map. (English) Zbl 1468.68325 J. Autom. Reasoning 62, No. 2, 215-236 (2019). MSC: 68V20 03B35 34A12 34A26 37C10 65L05 65P99 PDFBibTeX XMLCite \textit{F. Immler} and \textit{C. Traut}, J. Autom. Reasoning 62, No. 2, 215--236 (2019; Zbl 1468.68325) Full Text: DOI
Michaelis, Julius; Nipkow, Tobias Formalized proof systems for propositional logic. (English) Zbl 1528.03097 Abel, Andreas (ed.) et al., 23rd international conference on types for proofs and programs, TYPES 2017, May 24 – June 1, 2017, Budapest, Hungary. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 104, Article 5, 16 p. (2018). MSC: 03B35 PDFBibTeX XMLCite \textit{J. Michaelis} and \textit{T. Nipkow}, LIPIcs -- Leibniz Int. Proc. Inform. 104, Article 5, 16 p. (2018; Zbl 1528.03097) Full Text: DOI
Gleißner, Tobias; Steen, Alexander The MET: the art of flexible reasoning with modalities. (English) Zbl 1518.68416 Benzmüller, Christoph (ed.) et al., Rules and reasoning. Second international joint conference, RuleML+RR 2018, Luxembourg, Luxembourg, September 18–21, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11092, 274-284 (2018). MSC: 68V15 03B45 PDFBibTeX XMLCite \textit{T. Gleißner} and \textit{A. Steen}, Lect. Notes Comput. Sci. 11092, 274--284 (2018; Zbl 1518.68416) Full Text: DOI
Gengelbach, Arve; Weber, Tjark Model-theoretic conservative extension for definitional theories. (English) Zbl 1434.03028 Alves, Sandra (ed.) et al., Selected papers of the 12th workshop on logical and semantic frameworks, with applications (LSFA 2017), Brasilia, Brazil, September 23–24, 2017. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 338, 133-145 (2018). MSC: 03B35 03B16 03C07 68V15 PDFBibTeX XMLCite \textit{A. Gengelbach} and \textit{T. Weber}, Electron. Notes Theor. Comput. Sci. 338, 133--145 (2018; Zbl 1434.03028) Full Text: DOI
Haslbeck, Maximilian P. L.; Nipkow, Tobias Hoare logics for time bounds. A study in meta theory. (English) Zbl 1423.68098 Beyer, Dirk (ed.) et al., Tools and algorithms for the construction and analysis of systems. 24th international conference, TACAS 2018, held as part of the European joint conferences on theory and practice of software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 10805, 155-171 (2018). MSC: 68N30 03B70 68Q60 68T15 68W40 PDFBibTeX XMLCite \textit{M. P. L. Haslbeck} and \textit{T. Nipkow}, Lect. Notes Comput. Sci. 10805, 155--171 (2018; Zbl 1423.68098) Full Text: DOI
Parent, Xavier; van der Torre, Leendert Introduction to deontic logic and normative systems. (English) Zbl 1431.03034 Texts in Logic and Reasoning 1. London: College Publications (ISBN 978-1-84890-269-5/pbk). viii, 92 p. (2018). Reviewer: David Makinson (London) MSC: 03B45 PDFBibTeX XMLCite \textit{X. Parent} and \textit{L. van der Torre}, Introduction to deontic logic and normative systems. London: College Publications (2018; Zbl 1431.03034)
Benzmüller, Christoph; Farjami, Ali; Parent, Xavier A dyadic deontic logic in HOL. (English) Zbl 1418.03069 Broersen, Jan (ed.) et al., Deontic logic and normative systems. 14th international conference, DEON 2018, Utrecht, Netherlands, July 3–6, 2018. Proceedings. London: College Publications. 33-49 (2018). MSC: 03B45 03B15 03B35 PDFBibTeX XMLCite \textit{C. Benzmüller} et al., in: Deontic logic and normative systems. 14th international conference, DEON 2018, Utrecht, Netherlands, July 3--6, 2018. Proceedings. London: College Publications. 33--49 (2018; Zbl 1418.03069)
Huerta y Munive, Jonathan Julián; Struth, Georg Verifying hybrid systems with modal Kleene algebra. (English) Zbl 1518.68209 Desharnais, Jules (ed.) et al., Relational and algebraic methods in computer science. 17th international conference, RAMiCS 2018, Groningen, The Netherlands, October 29 – November 1, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11194, 225-243 (2018). MSC: 68Q60 03B70 68V20 PDFBibTeX XMLCite \textit{J. J. Huerta y Munive} and \textit{G. Struth}, Lect. Notes Comput. Sci. 11194, 225--243 (2018; Zbl 1518.68209) Full Text: DOI
Avron, Arnon; Cohen, Liron Applicable mathematics in a minimal computational theory of sets. (English) Zbl 1454.03064 Log. Methods Comput. Sci. 14, No. 4, Paper No. 1, 29 p. (2018). MSC: 03E30 03B35 PDFBibTeX XMLCite \textit{A. Avron} and \textit{L. Cohen}, Log. Methods Comput. Sci. 14, No. 4, Paper No. 1, 29 p. (2018; Zbl 1454.03064) Full Text: DOI arXiv
Guttmann, Walter Verifying minimum spanning tree algorithms with Stone relation algebras. (English) Zbl 1401.68247 J. Log. Algebr. Methods Program. 101, 132-150 (2018). MSC: 68R10 03B35 03G15 05C22 68Q60 68T15 PDFBibTeX XMLCite \textit{W. Guttmann}, J. Log. Algebr. Methods Program. 101, 132--150 (2018; Zbl 1401.68247) Full Text: DOI
Schlichtkrull, Anders; Blanchette, Jasmin Christian; Traytel, Dmitriy; Waldmann, Uwe Formalizing Bachmair and Ganzinger’s ordered resolution prover. (English) Zbl 1468.68306 Galmiche, Didier (ed.) et al., Automated reasoning. 9th international joint conference, IJCAR 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14–17, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10900, 89-107 (2018). MSC: 68V15 03B35 68V20 PDFBibTeX XMLCite \textit{A. Schlichtkrull} et al., Lect. Notes Comput. Sci. 10900, 89--107 (2018; Zbl 1468.68306) Full Text: DOI Link
Bentkamp, Alexander; Blanchette, Jasmin Christian; Cruanes, Simon; Waldmann, Uwe Superposition for \(\lambda\)-free higher-order logic. (English) Zbl 1511.68302 Galmiche, Didier (ed.) et al., Automated reasoning. 9th international joint conference, IJCAR 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14–17, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10900, 28-46 (2018). MSC: 68V15 03B16 03B35 PDFBibTeX XMLCite \textit{A. Bentkamp} et al., Lect. Notes Comput. Sci. 10900, 28--46 (2018; Zbl 1511.68302) Full Text: DOI
Endou, Noboru Fubini’s theorem for non-negative or non-positive functions. (English) Zbl 1401.28007 Formaliz. Math. 26, No. 1, 49-67 (2018). MSC: 28A35 03B35 PDFBibTeX XMLCite \textit{N. Endou}, Formaliz. Math. 26, No. 1, 49--67 (2018; Zbl 1401.28007) Full Text: DOI
Coghetto, Roland Klein-Beltrami model. II. (English) Zbl 1401.51002 Formaliz. Math. 26, No. 1, 33-48 (2018). MSC: 51A05 51M10 03B35 PDFBibTeX XMLCite \textit{R. Coghetto}, Formaliz. Math. 26, No. 1, 33--48 (2018; Zbl 1401.51002) Full Text: DOI
Coghetto, Roland Klein-Beltrami model. I. (English) Zbl 1401.51001 Formaliz. Math. 26, No. 1, 21-32 (2018). MSC: 51A05 03B35 PDFBibTeX XMLCite \textit{R. Coghetto}, Formaliz. Math. 26, No. 1, 21--32 (2018; Zbl 1401.51001) Full Text: DOI
Syeda, Hira Taqdees; Klein, Gerwin Program verification in the presence of cached address translation. (English) Zbl 1468.68069 Avigad, Jeremy (ed.) et al., Interactive theorem proving. 9th international conference, ITP 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10895, 542-559 (2018). MSC: 68N25 03B70 68N30 68V15 PDFBibTeX XMLCite \textit{H. T. Syeda} and \textit{G. Klein}, Lect. Notes Comput. Sci. 10895, 542--559 (2018; Zbl 1468.68069) Full Text: DOI
Jantsch, Simon; Norrish, Michael Verifying the LTL to Büchi automata translation via very weak alternating automata. (English) Zbl 1511.68335 Avigad, Jeremy (ed.) et al., Interactive theorem proving. 9th international conference, ITP 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10895, 306-323 (2018). MSC: 68V20 03B44 03D05 68Q45 PDFBibTeX XMLCite \textit{S. Jantsch} and \textit{M. Norrish}, Lect. Notes Comput. Sci. 10895, 306--323 (2018; Zbl 1511.68335) Full Text: DOI
Doczkal, Christian; Combette, Guillaume; Pous, Damien A formal proof of the minor-exclusion property for treewidth-two graphs. (English) Zbl 1468.68319 Avigad, Jeremy (ed.) et al., Interactive theorem proving. 9th international conference, ITP 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10895, 178-195 (2018). MSC: 68V20 03B35 05C05 05C60 05C83 68V15 PDFBibTeX XMLCite \textit{C. Doczkal} et al., Lect. Notes Comput. Sci. 10895, 178--195 (2018; Zbl 1468.68319) Full Text: DOI HAL
Cauderlier, Raphaël Tactics and certificates in Meta Dedukti. (English) Zbl 1482.68266 Avigad, Jeremy (ed.) et al., Interactive theorem proving. 9th international conference, ITP 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10895, 142-159 (2018). MSC: 68V15 03B70 PDFBibTeX XMLCite \textit{R. Cauderlier}, Lect. Notes Comput. Sci. 10895, 142--159 (2018; Zbl 1482.68266) Full Text: DOI
Bannister, Callum; Höfner, Peter; Klein, Gerwin Backwards and forwards with separation logic. (English) Zbl 1511.68067 Avigad, Jeremy (ed.) et al., Interactive theorem proving. 9th international conference, ITP 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10895, 68-87 (2018). MSC: 68N30 03B70 68V15 PDFBibTeX XMLCite \textit{C. Bannister} et al., Lect. Notes Comput. Sci. 10895, 68--87 (2018; Zbl 1511.68067) Full Text: DOI
Balco, Samuel; Frittella, Sabine; Greco, Giuseppe; Kurz, Alexander; Palmigiano, Alessandra Software tool support for modular reasoning in modal logics of actions. (English) Zbl 1511.68301 Avigad, Jeremy (ed.) et al., Interactive theorem proving. 9th international conference, ITP 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10895, 48-67 (2018). MSC: 68V15 03B42 03B45 68V20 PDFBibTeX XMLCite \textit{S. Balco} et al., Lect. Notes Comput. Sci. 10895, 48--67 (2018; Zbl 1511.68301) Full Text: DOI Link
Schwammberger, Maike An abstract model for proving safety of autonomous urban traffic. (English) Zbl 1400.68126 Theor. Comput. Sci. 744, 143-169 (2018). MSC: 68Q60 03B70 68Q45 90B20 PDFBibTeX XMLCite \textit{M. Schwammberger}, Theor. Comput. Sci. 744, 143--169 (2018; Zbl 1400.68126) Full Text: DOI
Benzmüller, Christoph; Parent, Xavier; van der Torre, Leendert A deontic logic reasoning infrastructure. (English) Zbl 1509.68327 Manea, Florin (ed.) et al., Sailing routes in the world of computation. 14th conference on computability in Europe, CiE 2018, Kiel, Germany, July 30 – August 3, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10936, 60-69 (2018). MSC: 68V20 03B16 03B35 03B45 68T27 68T30 PDFBibTeX XMLCite \textit{C. Benzmüller} et al., Lect. Notes Comput. Sci. 10936, 60--69 (2018; Zbl 1509.68327) Full Text: DOI Link
Schlichtkrull, Anders Formalization of the resolution calculus for first-order logic. (English) Zbl 1451.03019 J. Autom. Reasoning 61, No. 1-4, 455-484 (2018). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{A. Schlichtkrull}, J. Autom. Reasoning 61, No. 1--4, 455--484 (2018; Zbl 1451.03019) Full Text: DOI Link
Shankar, Natarajan Combining model checking and deduction. (English) Zbl 1392.68265 Clarke, Edmund M. (ed.) et al., Handbook of model checking. Cham: Springer (ISBN 978-3-319-10574-1/hbk; 978-3-319-10575-8/ebook). 651-684 (2018). MSC: 68Q60 03B70 PDFBibTeX XMLCite \textit{N. Shankar}, in: Handbook of model checking. Cham: Springer. 651--684 (2018; Zbl 1392.68265) Full Text: DOI
Steffen, Bernhard; Rüthing, Oliver; Huth, Michael Mathematical foundations of advanced informatics. Volume 1. Inductive approaches. (English) Zbl 1395.68002 Cham: Springer (ISBN 978-3-319-68396-6/hbk; 978-3-319-68397-3/ebook). xxvii, 228 p. (2018). Reviewer: Éric Martin (Sydney) MSC: 68-01 00A06 03B70 PDFBibTeX XMLCite \textit{B. Steffen} et al., Mathematical foundations of advanced informatics. Volume 1. Inductive approaches. Cham: Springer (2018; Zbl 1395.68002) Full Text: DOI
Struth, Georg Hoare semigroups. (English) Zbl 1390.68440 Math. Struct. Comput. Sci. 28, No. 6, 775-799 (2018). MSC: 68Q60 03B70 20M10 PDFBibTeX XMLCite \textit{G. Struth}, Math. Struct. Comput. Sci. 28, No. 6, 775--799 (2018; Zbl 1390.68440) Full Text: DOI
Blanchette, Jasmin Christian; Meier, Fabian; Popescu, Andrei; Traytel, Dmitriy Foundational nonuniform (co)datatypes for higher-order logic. (English) Zbl 1457.68173 Proceedings of the 2017 32nd annual ACM/IEEE symposium on logic in computer science, LICS 2017, Reykjavík University, Reykjavík, Iceland, June 20–23, 2017. Piscataway, NJ: IEEE Press. Article No. 11, 12 p. (2017). MSC: 68Q65 03B16 PDFBibTeX XMLCite \textit{J. C. Blanchette} et al., in: Proceedings of the 2017 32nd annual ACM/IEEE symposium on logic in computer science, LICS 2017, Reykjavík University, Reykjavík, Iceland, June 20--23, 2017. Piscataway, NJ: IEEE Press. Article No. 11, 12 p. (2017; Zbl 1457.68173) Full Text: Link
Blanchette, Jasmin Christian; Fleury, Mathias; Traytel, Dmitriy Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL. (English) Zbl 1434.03025 Miller, Dale (ed.), 2nd international conference on formal structures for computation and deduction. FSCD 2017, Oxford, UK, September 3–9, 2017. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 84, Article 11, 18 p. (2017). MSC: 03B35 03B25 03F15 PDFBibTeX XMLCite \textit{J. C. Blanchette} et al., LIPIcs -- Leibniz Int. Proc. Inform. 84, Article 11, 18 p. (2017; Zbl 1434.03025) Full Text: DOI
Gleißner, Tobias; Steen, Alexander; Benzmüller, Christoph Theorem provers for every normal modal logic. (English) Zbl 1403.68225 Eiter, Thomas (ed.) et al., LPAR-21. 21st international conference on logic for programming, artificial intelligence and reasoning, Maun, Botswana, May 8–12, 2017. Selected papers. Manchester: EasyChair. EPiC Series in Computing 46, 14-30 (2017). MSC: 68T15 03B35 03B45 PDFBibTeX XMLCite \textit{T. Gleißner} et al., EPiC Ser. Comput. 46, 14--30 (2017; Zbl 1403.68225) Full Text: DOI
Coghetto, Roland; Grabowski, Adam Tarski geometry axioms. III. (English) Zbl 1401.51003 Formaliz. Math. 25, No. 4, 289-313 (2017). MSC: 51A05 03B35 PDFBibTeX XMLCite \textit{R. Coghetto} and \textit{A. Grabowski}, Formaliz. Math. 25, No. 4, 289--313 (2017; Zbl 1401.51003) Full Text: DOI