OOIR: Observatory of International Research

Papers

(The TQCC of Journal of Automated Reasoning is 2. 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-05-01 to 2026-05-01.)

Article	Citations
Unifying Splitting	11
Optimal Deterministic Controller Synthesis from Steady-State Distributions	10
Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL	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
Synthesising Programs with Non-trivial Constants	7
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq	7
Formalized Functional Analysis with Semilinear Maps	7
SAT Meets Tableaux for Linear Temporal Logic Satisfiability	7
Formalization of the Prime Number Theorem with a Remainder Term	6
Certified First-Order AC-Unification and Applications	6
Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic	6
The Rewster: Type Preserving Rewrite Rules for the Rocq Prover	6
Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate	5
Saturation-Based Boolean Conjunctive Query Answering and Rewriting for the Guarded Quantification Fragments	5
Polite Combination of Algebraic Datatypes	5
A Formal Theory of Choreographic Programming	5
Single-Set Cubical Categories and Their Formalisation with a Proof Assistant	4
A Resolution Proof System for Dependency Stochastic Boolean Satisfiability	4
Refinement of Parallel Algorithms Down to LLVM: Applied to Practically Efficient Parallel Sorting	4
Combination of Uniform Interpolants via Beth Definability	3
Non-termination in Term Rewriting and Logic Programming	3
Correction to: Local is Best: Efficient Reductions to Modal Logic K	3
SCL(EQ): SCL for First-Order Logic with Equality	3
Verifying the Generalization of Deep Learning to Out-of-Distribution Domains	3

Measuring the Readability of Geometric Proofs: The Area Method Case	3
The Resolution of Keller’s Conjecture	3
Schematic Program Proofs with Abstract Execution	3
A Formalization of Dedekind Domains and Class Groups of Global Fields	2
Set of Support, Demodulation, Paramodulation: A Historical Perspective	2
An Automated Approach to the Collatz Conjecture	2
Unsatisfiability-based Algorithms for Multi-Objective Combinatorial Optimization	2
Feature Necessity and Relevancy in Machine Learning Explanations	2
Theorem Proving as Constraint Solving with Coherent Logic	2
Deciding the Word Problem for Ground and Strongly Shallow Identities w.r.t. Extensional Symbols	2
Constructing the Lie Algebra of Smooth Vector Fields on a Lie Group in Isabelle/HOL	2
A Solver for Arrays with Concatenation	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
Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow Embedding	2
Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version	2
From Specification to Testing: Semantics Engineering for Lua 5.2	2
Combining Higher-Order Logic with Set Theory Formalizations	2
Should Decisions in QCDCL Follow Prefix Order?	2
A Formalization of SQL with Nulls	2
Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification	2
Cyclic Hypersequent System for Transitive Closure Logic	2
A simple proof of correctness of folding the regular heptagon	2
Satisfiability of Non-linear Transcendental Arithmetic as a Certificate Search Problem	2
Timed Automata Verification and Synthesis Via Finite Automata Learning	2
A Direct Procedure to Test Entailment in a Separation Logic of Relations	2
Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic	2