Single-Set Cubical Categories and Their Formalisation with a Proof Assistant Philippe MalbosTanguy MassacrierGeorg Struth OriginalPaper 12 September 2024 Article: 20
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq Jason GrossAndres ErbsenAdam Chlipala OriginalPaper Open access 14 August 2024 Article: 19
Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow Embedding Zhongye WangQinxiang CaoYichen Tao OriginalPaper 10 August 2024 Article: 18
Verifying the Generalization of Deep Learning to Out-of-Distribution Domains Guy AmirOsher MaayanMichael Schapira OriginalPaper Open access 03 August 2024 Article: 17
Dependency Schemes in CDCL-Based QBF Solving: A Proof-Theoretic Study Abhimanyu ChoudhuryMeena Mahajan OriginalPaper Open access 24 July 2024 Article: 16
Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL Asta Halkjær FromFrederik Krogsdal Jacobsen OriginalPaper Open access 27 June 2024 Article: 15
Refinement of Parallel Algorithms Down to LLVM: Applied to Practically Efficient Parallel Sorting Peter Lammich OriginalPaper Open access 19 June 2024 Article: 14
General Clauses for SAT-Based Proof Search in Intuitionistic Propositional Logic Camillo FiorentiniMauro Ferrari OriginalPaper 16 June 2024 Article: 13
Automated Generation of Geometry Proof Problems Based on Point Geometry Identity Lei LiZongkai YangSannyuya Liu OriginalPaper 05 June 2024 Article: 11
Formalized Functional Analysis with Semilinear Maps Frédéric DupuisRobert Y. LewisHeather Macbeth OriginalPaper 04 June 2024 Article: 10
Linear Resources in Isabelle/HOL Filip SmolaJacques D. Fleuriot OriginalPaper Open access 18 May 2024 Article: 9
Sequent Calculi for Choice Logics Michael BernreiterAnela LolicStefan Woltran OriginalPaper Open access 03 April 2024 Article: 8
Schematic Program Proofs with Abstract Execution Dominic SteinhöfelReiner Hähnle OriginalPaper Open access 26 March 2024 Article: 7
SAT Meets Tableaux for Linear Temporal Logic Satisfiability Luca GeattiNicola GiganteGabriele Venturato OriginalPaper Open access 15 March 2024 Article: 6
Should Decisions in QCDCL Follow Prefix Order? Benjamin BöhmTomáš PeitlOlaf Beyersdorff OriginalPaper Open access 09 February 2024 Article: 5
Non-termination in Term Rewriting and Logic Programming Étienne Payet OriginalPaper 02 February 2024 Article: 4
A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry David BraunNicolas MagaudPascal Schreck OriginalPaper 18 January 2024 Article: 3
A Formalization of the CHSH Inequality and Tsirelson’s Upper-bound in Isabelle/HOL Mnacho EchenimMehdi Mhalla OriginalPaper 19 December 2023 Article: 2
Formally-Verified Round-Off Error Analysis of Runge–Kutta Methods Florian Faissole OriginalPaper 06 December 2023 Article: 1
Formal Verification of Termination Criteria for First-Order Recursive Functions Cesar A. MuñozMauricio Ayala-RincónThiago M. Ferreira Ramos OriginalPaper 29 November 2023 Article: 40
Saturation-Based Boolean Conjunctive Query Answering and Rewriting for the Guarded Quantification Fragments Sen ZhengRenate A. Schmidt OriginalPaper Open access 23 November 2023 Article: 39
Self-evident Automated Geometric Theorem Proving Based on Complex Number Identity Xicheng PengJingzhong ZhangSannyuya Liu OriginalPaper 20 November 2023 Article: 38
Bisequent Calculus for Four-Valued Quasi-Relevant Logics: Cut Elimination and Interpolation Andrzej Indrzejczak OriginalPaper Open access 16 November 2023 Article: 37
Finitary Type Theories With and Without Contexts Philipp G. HaselwarterAndrej Bauer OriginalPaper Open access 07 October 2023 Article: 36
Lower Bounds for QCDCL via Formula Gauge Benjamin BöhmOlaf Beyersdorff OriginalPaper Open access 27 September 2023 Article: 35
Combining Stable Infiniteness and (Strong) Politeness Ying ShengYoni ZoharCesare Tinelli Research 27 September 2023 Article: 34
Enabling Floating-Point Arithmetic in the Coq Proof Assistant Érik Martin-DorelGuillaume MelquiondPierre Roux OriginalPaper 16 September 2023 Article: 33
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences Ying ShengAndres NötzliCesare Tinelli OriginalPaper 15 September 2023 Article: 32
Preprocessing of Propagation Redundant Clauses Joseph E. ReevesMarijn J. H. HeuleRandal E. Bryant OriginalPaper Open access 14 September 2023 Article: 31
A Proof Procedure for Separation Logic with Inductive Definitions and Data Mnacho EchenimNicolas Peltier OriginalPaper 09 September 2023 Article: 30
Mechanising Gödel–Löb Provability Logic in HOL Light Marco MaggesiCosimo Perini Brogi OriginalPaper Open access 29 August 2023 Article: 29
Measure Construction by Extension in Dependent Type Theory with Application to Integration Reynald AffeldtCyril Cohen OriginalPaper 18 August 2023 Article: 28
Cyclic Hypersequent System for Transitive Closure Logic Anupam DasMarianna Girlando OriginalPaper Open access 16 August 2023 Article: 27
A Resolution Proof System for Dependency Stochastic Boolean Satisfiability Yun-Rong LuoChe ChengJie-Hong R. Jiang OriginalPaper 03 August 2023 Article: 26
Binary Codes that do not Preserve Primitivity Štěpán HolubMartin RaškaŠtěpán Starosta OriginalPaper Open access 18 July 2023 Article: 25
POSIX Lexing with Derivatives of Regular Expressions Christian Urban OriginalPaper Open access 08 July 2023 Article: 24
Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version Andrei Popescu OriginalPaper Open access 05 July 2023 Article: 23
SCL(EQ): SCL for First-Order Logic with Equality Hendrik LeidingerChristoph Weidenbach OriginalPaper Open access 30 June 2023 Article: 22
A Formal Theory of Choreographic Programming Luís Cruz-FilipeFabrizio MontesiMarco Peressotti OriginalPaper Open access 27 May 2023 Article: 21
Combining Higher-Order Logic with Set Theory Formalizations Cezary KaliszykKarol Pąk OriginalPaper Open access 25 May 2023 Article: 20
Synthesising Programs with Non-trivial Constants Alessandro AbateHaniel BarbosaCesare Tinelli OriginalPaper Open access 13 May 2023 Article: 19
An Automatically Verified Prototype of the Android Permissions System Maximiliano CristiáGuido De LucaCarlos Luna OriginalPaper 12 May 2023 Article: 17
Unifying Splitting Gabriel EbnerJasmin BlanchetteSophie Tourret OriginalPaper Open access 28 April 2023 Article: 16
An Automated Approach to the Collatz Conjecture Emre YolcuScott AaronsonMarijn J. H. Heule OriginalPaper Open access 25 April 2023 Article: 15
First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification Aart MiddeldorpAlexander LochmannFabian Mitterwallner Research Open access 06 April 2023 Article: 14
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