Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq Dominik KirstMarc Hermes OriginalPaper Open access 12 March 2023 Article: 13
Computer-Aided Constructions of Commafree Codes Aaron A. Windsor OriginalPaper 17 February 2023 Article: 12
Finding Normal Binary Floating-Point Factors Efficiently Mak Andrlon OriginalPaper Open access 06 February 2023 Article: 11
Superposition for Higher-Order Logic Alexander BentkampJasmin BlanchettePetar Vukmirović OriginalPaper 21 January 2023 Article: 10
Correction: Towards Formalising Schutz’ Axioms for Minkowski Spacetime in Isabelle/HOL Richard SchmoettenJake E. PalmerJacques D. Fleuriot Correction Open access 13 January 2023 Article: 9
Efficient Extensional Binary Tries Andrew W. AppelXavier Leroy OriginalPaper 12 January 2023 Article: 8
Optimal Deterministic Controller Synthesis from Steady-State Distributions Alvaro VelasquezIsmail AlkhouriGeorge Atia OriginalPaper 12 January 2023 Article: 7
Semantically-Guided Goal-Sensitive Reasoning: Decision Procedures and the Koala Prover Maria Paola BonacinaSarah Winkler OriginalPaper 11 January 2023 Article: 6
Measuring the Readability of Geometric Proofs: The Area Method Case Pedro QuaresmaPierluigi Graziani OriginalPaper Open access 10 January 2023 Article: 5
A Solver for Arrays with Concatenation Qinshi WangAndrew W. Appel OriginalPaper 07 January 2023 Article: 4
Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic Guido Fiorino OriginalPaper 30 December 2022 Article: 3
Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL Chelsea EdmondsAngeliki Koutsoukou-ArgyrakiLawrence C. Paulson OriginalPaper Open access 19 December 2022 Article: 2
A Formalization and Proof Checker for Isabelle’s Metalogic Simon RoßkopfTobias Nipkow OriginalPaper Open access 12 December 2022 Article: 1
