OOIR: Observatory of International Research

Papers

(The median citation count of Journal of Automated Reasoning is 1. The table below lists those papers that are above that threshold based on CrossRef citation counts [max. 250 papers]. The publications cover those that have been published in the past four years, i.e., from 2022-08-01 to 2026-08-01.)

Article	Citations
Unifying Splitting	12
Optimal Deterministic Controller Synthesis from Steady-State Distributions	11
Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL	8
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq	7
Use and Abuse of Instance Parameters in the Lean Mathematical Library	7
Theorem Proving as Constraint Solving for Coherent Logic with Function Symbols	6
Synthesising Programs with Non-trivial Constants	6
Formalized Functional Analysis with Semilinear Maps	6
SAT Meets Tableaux for Linear Temporal Logic Satisfiability	6
Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic	5
Certified First-Order AC-Unification and Applications	5
The Rewster: Type Preserving Rewrite Rules for the Rocq Prover	5
Saturation-Based Boolean Conjunctive Query Answering and Rewriting for the Guarded Quantification Fragments	4
Refinement of Parallel Algorithms Down to LLVM: Applied to Practically Efficient Parallel Sorting	4
Formalization of the Prime Number Theorem with a Remainder Term	4
Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate	4
A Resolution Proof System for Dependency Stochastic Boolean Satisfiability	4
A Formal Theory of Choreographic Programming	4
Single-Set Cubical Categories and Their Formalisation with a Proof Assistant	4
Schematic Program Proofs with Abstract Execution	3
SCL(EQ): SCL for First-Order Logic with Equality	3
Measuring the Readability of Geometric Proofs: The Area Method Case	3
YALLA: Yet Another Deep Embedding of Linear Logic in Rocq	3
Non-termination in Term Rewriting and Logic Programming	3
Verifying the Generalization of Deep Learning to Out-of-Distribution Domains	3

Constructing the Lie Algebra of Smooth Vector Fields on a Lie Group in Isabelle/HOL	2
A Formalization of Dedekind Domains and Class Groups of Global Fields	2
An Automated Approach to the Collatz Conjecture	2
Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic	2
Correction to: Local is Best: Efficient Reductions to Modal Logic K	2
Formally-Verified Round-Off Error Analysis of Runge–Kutta Methods	2
Correction to: Certified First-Order AC-Unification and Applications	2
Feature Necessity and Relevancy in Machine Learning Explanations	2
Should Decisions in QCDCL Follow Prefix Order?	2
A Formalization of the CHSH Inequality and Tsirelson’s Upper-bound in Isabelle/HOL	2
Unsatisfiability-based Algorithms for Multi-Objective Combinatorial Optimization	2
Producing Proofs of Unsatisfiability with Distributed Clause-Sharing SAT Solvers	2
A simple proof of correctness of folding the regular heptagon	2
Self-evident Automated Geometric Theorem Proving Based on Complex Number Identity	2
A Direct Procedure to Test Entailment in a Separation Logic of Relations	2
Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow Embedding	2
A Solver for Arrays with Concatenation	2
Verified Tableaux: from Modal Logics to Modal Fixpoint Logics	2
Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification	2
Cyclic Hypersequent System for Transitive Closure Logic	2
Timed Automata Verification and Synthesis Via Finite Automata Learning	2
Combining Higher-Order Logic with Set Theory Formalizations	2
Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version	2
Satisfiability of Non-linear Transcendental Arithmetic as a Certificate Search Problem	2
POSIX Lexing with Derivatives of Regular Expressions	1
Solving a problem with GeoGebra current possibilities and limits of CAS tools	1
Automated reasoning for proving non-orderability of groups	1
Finding Normal Binary Floating-Point Factors Efficiently	1
A Formalization and Proof Checker for Isabelle’s Metalogic	1
Engel’s Theorem in Mathlib	1
Relative Security: (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities in Isabelle/HOL	1
A Formal Correctness Proof of Edmonds’ Blossom Shrinking Algorithm	1
Combining Stable Infiniteness and (Strong) Politeness	1
LTL Reactive Synthesis with a Few Hints	1
The Relative Strength of #SAT Proof Systems	1
A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry	1
Double Auctions: Formalization and Automated Checkers	1
From Specification to Testing: Semantics Engineering for Lua 5.2	1
Typed Compositional Quantum Computation with Lenses	1
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences	1
An Automatically Verified Prototype of the Android Permissions System	1
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users	1