Theorem Proving as Constraint Solving for Coherent Logic with Function Symbols Predrag Janičić OriginalPaper 16 October 2025 Article: 29
Formalization of Convergence Rates of Four First-order Algorithms for Convex Optimization Chenyi LiZiyu WangZaiwen Wen OriginalPaper 15 October 2025 Article: 28
A simple proof of correctness of folding the regular heptagon Zoltán Kovács OriginalPaper 13 October 2025 Article: 27
First-order Hybrid Separation Logic Frank S. de BoerHans-Dieter A. Hiep OriginalPaper Open access 29 September 2025 Article: 26
Reasoning About Incompletely Defined Programs Christoph Walther OriginalPaper Open access 25 August 2025 Article: 25
LTL Reactive Synthesis with a Few Hints Mrudula BalachanderEmmanuel FiliotJean-François Raskin OriginalPaper 21 August 2025 Article: 24
Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate Hannah MertensJoost-Pieter KatoenTobias Winkler OriginalPaper Open access 19 August 2025 Article: 23
Structured Monads for Generic First-Order Syntax Metatheory Lawrence DunnVal TannenSteve Zdancewic OriginalPaper Open access 11 August 2025 Article: 22
Formally Verified Suffix Array Construction Louis CheungAlistair MoffatChristine Rizkallah OriginalPaper Open access 21 July 2025 Article: 21
Solving a problem with GeoGebra current possibilities and limits of CAS tools Jiří BlažekPavel Pech OriginalPaper Open access 18 July 2025 Article: 20
Automated reasoning for proving non-orderability of groups Alexei LisitsaZipei NieAlexei Vernitski OriginalPaper Open access 11 July 2025 Article: 19
Constructing the Lie Algebra of Smooth Vector Fields on a Lie Group in Isabelle/HOL Richard SchmoettenJacques D. Fleuriot OriginalPaper Open access 26 June 2025 Article: 18
Double Auctions: Formalization and Automated Checkers Mohit GargN. RajaAbhishek Kr Singh OriginalPaper 24 June 2025 Article: 17
Active Learning for SAT Solver Benchmarking Tobias FuchsJakob BachMarkus Iser OriginalPaper Open access 23 June 2025 Article: 16
Timed Automata Verification and Synthesis Via Finite Automata Learning Ocan Sankur OriginalPaper 13 June 2025 Article: 15
A Sound and Complete Projection for Global Types Dawit TiroreJesper BengtsonMarco Carbone OriginalPaper Open access 28 May 2025 Article: 14
The QSMA Algorithm for Quantifiers in SMT Maria Paola BonacinaStéphane Graham-LengrandChristophe Vauthier OriginalPaper Open access 27 May 2025 Article: 13
Producing Proofs of Unsatisfiability with Distributed Clause-Sharing SAT Solvers Dawn MichaelsonDominik SchreiberMichael W. Whalen OriginalPaper Open access 27 May 2025 Article: 12
A Mechanically Verified Garbage Collector for OCaml Sheera ShamsuDipesh KafleKC Sivaramakrishnan OriginalPaper Open access 14 May 2025 Article: 11
A Direct Procedure to Test Entailment in a Separation Logic of Relations Mnacho EchenimNicolas Peltier OriginalPaper 03 May 2025 Article: 10
A Proof-Producing Compiler for Blockchain Applications Jeremy AvigadLior GoldbergAlon Titelman OriginalPaper Open access 11 April 2025 Article: 9
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users Ana de Almeida BorgesAnnalí Casanueva ArtísThéo Zimmermann OriginalPaper Open access 20 February 2025 Article: 8
Fast, Verified Computation for HOL ITPs Oskar AbrahamssonMagnus O. MyreenJohannes Åman Pohjola OriginalPaper Open access 18 February 2025 Article: 7
Correction to: Certified First-Order AC-Unification and Applications Mauricio Ayala-RincónMaribel FernándezDaniele Nantes-Sobrinho Correction 18 February 2025 Article: 6
Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification Dirk BeyerNian-Ze LeePhilipp Wendler OriginalPaper Open access 05 February 2025 Article: 5
Formalization of the Prime Number Theorem with a Remainder Term Shuhao SongBowen Yao OriginalPaper 04 February 2025 Article: 4
Satisfiability of Non-linear Transcendental Arithmetic as a Certificate Search Problem Enrico LippariniStefan Ratschan OriginalPaper 25 January 2025 Article: 3
Computer-Assisted Proofs for Lyapunov Stability via Sums of Squares Certificates and Constructive Analysis Grigory DevadzeVictor MagronStefan Streif OriginalPaper Open access 25 January 2025 Article: 2
Use and Abuse of Instance Parameters in the Lean Mathematical Library Anne Baanen OriginalPaper Open access 12 December 2024 Article: 1
Certified First-Order AC-Unification and Applications Mauricio Ayala-RincónMaribel FernándezDaniele Nantes-Sobrinho OriginalPaper 14 November 2024 Article: 25
Investigations into Proof Structures Christoph WernhardWolfgang Bibel OriginalPaper Open access 29 October 2024 Article: 24
A Practical Decision Procedure for Quantifier-Free, Decidable Languages Extended with Restricted Quantifiers Maximiliano CristiáGianfranco Rossi OriginalPaper 24 October 2024 Article: 23
Windmills of the Minds: A Hopping Algorithm for Fermat’s Two Squares Theorem Hing Lun Chan OriginalPaper Open access 21 October 2024 Article: 22
IsaVODEs: Interactive Verification of Cyber-Physical Systems at Scale Jonathan Julián Huerta y MuniveSimon FosterThomas Hickman OriginalPaper Open access 19 October 2024 Article: 21
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
