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

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

Handling Transitive Relations in First-Order Automated Reasoning	3
SCL(EQ): SCL for First-Order Logic with Equality	3
Non-termination in Term Rewriting and Logic Programming	3
A Formalization of SQL with Nulls	2
Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic	2
An Automated Approach to the Collatz Conjecture	2
Predicate Transformer Semantics for Hybrid Systems	2
Should Decisions in QCDCL Follow Prefix Order?	2
Cyclic Hypersequent System for Transitive Closure Logic	2
Automata Terms in a Lazy WSkS Decision Procedure	2
Measuring the Readability of Geometric Proofs: The Area Method Case	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 Formalization of Dedekind Domains and Class Groups of Global Fields	2
Constructing the Lie Algebra of Smooth Vector Fields on a Lie Group in Isabelle/HOL	2
Timed Automata Verification and Synthesis Via Finite Automata Learning	2
Set of Support, Demodulation, Paramodulation: A Historical Perspective	2
Schematic Program Proofs with Abstract Execution	2
A Formalization of the CHSH Inequality and Tsirelson’s Upper-bound in Isabelle/HOL	2
A Solver for Arrays with Concatenation	2
Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification	2
Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow Embedding	2
Combining Higher-Order Logic with Set Theory Formalizations	1
A Direct Procedure to Test Entailment in a Separation Logic of Relations	1
Satisfiability of Non-linear Transcendental Arithmetic as a Certificate Search Problem	1
Larry Wos: Visions of Automated Reasoning	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
Finding Normal Binary Floating-Point Factors Efficiently	1
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users	1
Combining Stable Infiniteness and (Strong) Politeness	1
Formally-Verified Round-Off Error Analysis of Runge–Kutta Methods	1
Deciding the Word Problem for Ground and Strongly Shallow Identities w.r.t. Extensional Symbols	1
Theorem Proving as Constraint Solving with Coherent Logic	1
POSIX Lexing with Derivatives of Regular Expressions	1
Experiences from Exporting Major Proof Assistant Libraries	1
Engel’s Theorem in Mathlib	1
Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant	1
Automated reasoning for proving non-orderability of groups	1
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences	1
A Coq Formalization of Lebesgue Integration of Nonnegative Functions	1
From Specification to Testing: Semantics Engineering for Lua 5.2	1
Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version	1
Proof Complexity of Modal Resolution	1
Correction to: Certified First-Order AC-Unification and Applications	1
Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs	1
A Formalization and Proof Checker for Isabelle’s Metalogic	1
An Automatically Verified Prototype of the Android Permissions System	1
Double Auctions: Formalization and Automated Checkers	1