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

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

Handling Transitive Relations in First-Order Automated Reasoning	3
A Resolution Proof System for Dependency Stochastic Boolean Satisfiability	3
Predicate Transformer Semantics for Hybrid Systems	3
Combination of Uniform Interpolants via Beth Definability	3
Automata Terms in a Lazy WSkS Decision Procedure	2
Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic	2
An Automated Approach to the Collatz Conjecture	2
A Formalization of Dedekind Domains and Class Groups of Global Fields	2
Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification	2
Cyclic Hypersequent System for Transitive Closure Logic	2
Measuring the Readability of Geometric Proofs: The Area Method Case	2
Correction to: Local is Best: Efficient Reductions to Modal Logic K	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 Formalization of SQL with Nulls	2
Set of Support, Demodulation, Paramodulation: A Historical Perspective	2
Schematic Program Proofs with Abstract Execution	2
Model Completeness, Uniform Interpolants and Superposition Calculus	2
Should Decisions in QCDCL Follow Prefix Order?	2
Human-Centered Automated Proof Search	2
Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version	1
From Specification to Testing: Semantics Engineering for Lua 5.2	1
Finding Normal Binary Floating-Point Factors Efficiently	1
Experiences from Exporting Major Proof Assistant Libraries	1
Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs	1
A Coq Formalization of Lebesgue Integration of Nonnegative Functions	1
Correction to: Certified First-Order AC-Unification and Applications	1
Larry Wos: Visions of Automated Reasoning	1
Using Model Theory to Find Decidable and Tractable Description Logics with Concrete Domains	1
Combining Stable Infiniteness and (Strong) Politeness	1
Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant	1
A Formalization and Proof Checker for Isabelle’s Metalogic	1
Self-evident Automated Geometric Theorem Proving Based on Complex Number Identity	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
Proof Complexity of Modal Resolution	1
Satisfiability of Non-linear Transcendental Arithmetic as a Certificate Search Problem	1
Combining Higher-Order Logic with Set Theory Formalizations	1
An Automatically Verified Prototype of the Android Permissions System	1
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences	1
Formally-Verified Round-Off Error Analysis of Runge–Kutta Methods	1
POSIX Lexing with Derivatives of Regular Expressions	1
Formalization of Ring Theory in PVS	1