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-01-01 to 2026-01-01.)

Article	Citations
Unifying Splitting	10
SAT Meets Tableaux for Linear Temporal Logic Satisfiability	9
Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL	8
Use and Abuse of Instance Parameters in the Lean Mathematical Library	8
Optimal Deterministic Controller Synthesis from Steady-State Distributions	8
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq	7
Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic	6
A Wos Challenge Met	6
Synthesising Programs with Non-trivial Constants	6
Formalized Functional Analysis with Semilinear Maps	6
Certified First-Order AC-Unification and Applications	6
Theorem Proving as Constraint Solving for Coherent Logic with Function Symbols	6
Formalization of the Prime Number Theorem with a Remainder Term	6
Saturation-Based Boolean Conjunctive Query Answering and Rewriting for the Guarded Quantification Fragments	5
Polite Combination of Algebraic Datatypes	4
A Resolution Proof System for Dependency Stochastic Boolean Satisfiability	4
Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate	4
A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column	4
A Formal Theory of Choreographic Programming	4
Refinement of Parallel Algorithms Down to LLVM: Applied to Practically Efficient Parallel Sorting	3
Combination of Uniform Interpolants via Beth Definability	3
Non-termination in Term Rewriting and Logic Programming	3
Single-Set Cubical Categories and Their Formalisation with a Proof Assistant	3
Formalization of the Computational Theory of a Turing Complete Functional Language Model	3
Measuring the Readability of Geometric Proofs: The Area Method Case	3

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