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 2021-11-01 to 2025-11-01.)

Article	Citations
Unifying Splitting	14
Synthesising Programs with Non-trivial Constants	10
Optimal Deterministic Controller Synthesis from Steady-State Distributions	9
Theorem Proving as Constraint Solving for Coherent Logic with Function Symbols	8
Use and Abuse of Instance Parameters in the Lean Mathematical Library	8
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq	7
Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL	7
Correction to: Differential Dynamic Logic for Hybrid Systems	6
SAT Meets Tableaux for Linear Temporal Logic Satisfiability	6
Formalization of the Prime Number Theorem with a Remainder Term	6
Formalized Functional Analysis with Semilinear Maps	6
Certified First-Order AC-Unification and Applications	6
Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic	6
A Wos Challenge Met	5
Polite Combination of Algebraic Datatypes	5
Refinement of Parallel Algorithms Down to LLVM: Applied to Practically Efficient Parallel Sorting	4
Saturation-Based Boolean Conjunctive Query Answering and Rewriting for the Guarded Quantification Fragments	4
A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column	4
Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate	4
A Formal Theory of Choreographic Programming	4
SCL(EQ): SCL for First-Order Logic with Equality	3
Verifying Whiley Programs with Boogie	3
Verifying the Generalization of Deep Learning to Out-of-Distribution Domains	3
Formalization of the Computational Theory of a Turing Complete Functional Language Model	3
A Resolution Proof System for Dependency Stochastic Boolean Satisfiability	3

Single-Set Cubical Categories and Their Formalisation with a Proof Assistant	3
The Resolution of Keller’s Conjecture	2
Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic	2
An Automated Approach to the Collatz Conjecture	2
Measuring the Readability of Geometric Proofs: The Area Method Case	2
A simple proof of correctness of folding the regular heptagon	2
Larry Wos: Visions of Automated Reasoning	2
Should Decisions in QCDCL Follow Prefix Order?	2
Non-termination in Term Rewriting and Logic Programming	2
Combination of Uniform Interpolants via Beth Definability	2
Correction to: Local is Best: Efficient Reductions to Modal Logic K	2
Producing Proofs of Unsatisfiability with Distributed Clause-Sharing SAT Solvers	2
A Solver for Arrays with Concatenation	2
Cyclic Hypersequent System for Transitive Closure Logic	2
Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification	2
Timed Automata Verification and Synthesis Via Finite Automata Learning	2
A Formalization of the CHSH Inequality and Tsirelson’s Upper-bound in Isabelle/HOL	2
Schematic Program Proofs with Abstract Execution	2
Set of Support, Demodulation, Paramodulation: A Historical Perspective	2
A Formalization of SQL with Nulls	2
A Formalization of Dedekind Domains and Class Groups of Global Fields	2
Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow Embedding	2
Constructing the Lie Algebra of Smooth Vector Fields on a Lie Group in Isabelle/HOL	2
An Automatically Verified Prototype of the Android Permissions System	1
From Specification to Testing: Semantics Engineering for Lua 5.2	1
Formally-Verified Round-Off Error Analysis of Runge–Kutta Methods	1
Correction to: Certified First-Order AC-Unification and Applications	1
Self-evident Automated Geometric Theorem Proving Based on Complex Number Identity	1
Automated reasoning for proving non-orderability of groups	1
A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry	1
LTL Reactive Synthesis with a Few Hints	1
Double Auctions: Formalization and Automated Checkers	1
Combining Higher-Order Logic with Set Theory Formalizations	1
A Direct Procedure to Test Entailment in a Separation Logic of Relations	1
Theorem Proving as Constraint Solving with Coherent Logic	1
A Coq Formalization of Lebesgue Integration of Nonnegative Functions	1
Combining Stable Infiniteness and (Strong) Politeness	1
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users	1
Engel’s Theorem in Mathlib	1
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences	1
Using Model Theory to Find Decidable and Tractable Description Logics with Concrete Domains	1
Deciding the Word Problem for Ground and Strongly Shallow Identities w.r.t. Extensional Symbols	1
Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version	1
Satisfiability of Non-linear Transcendental Arithmetic as a Certificate Search Problem	1
POSIX Lexing with Derivatives of Regular Expressions	1
Solving a problem with GeoGebra current possibilities and limits of CAS tools	1
A Formalization and Proof Checker for Isabelle’s Metalogic	1
Finding Normal Binary Floating-Point Factors Efficiently	1