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

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

The Resolution of Keller’s Conjecture	3
Handling Transitive Relations in First-Order Automated Reasoning	3
Single-Set Cubical Categories and Their Formalisation with a Proof Assistant	3
An Automated Approach to the Collatz Conjecture	2
Predicate Transformer Semantics for Hybrid Systems	2
Human-Centered Automated Proof Search	2
Automata Terms in a Lazy WSkS Decision Procedure	2
Constructing the Lie Algebra of Smooth Vector Fields on a Lie Group in Isabelle/HOL	2
A Formalization of SQL with Nulls	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
Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow Embedding	2
Should Decisions in QCDCL Follow Prefix Order?	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
Cyclic Hypersequent System for Transitive Closure Logic	2
Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification	2
A Solver for Arrays with Concatenation	2
Measuring the Readability of Geometric Proofs: The Area Method Case	2
Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic	2
From Specification to Testing: Semantics Engineering for Lua 5.2	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
POSIX Lexing with Derivatives of Regular Expressions	1
Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant	1
Finding Normal Binary Floating-Point Factors Efficiently	1
A Direct Procedure to Test Entailment in a Separation Logic of Relations	1
Deciding the Word Problem for Ground and Strongly Shallow Identities w.r.t. Extensional Symbols	1
Correction to: Certified First-Order AC-Unification and Applications	1
Timed Automata Verification and Synthesis Via Finite Automata Learning	1
Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version	1
Combining Higher-Order Logic with Set Theory Formalizations	1
Self-evident Automated Geometric Theorem Proving Based on Complex Number Identity	1
An Automatically Verified Prototype of the Android Permissions System	1
Experiences from Exporting Major Proof Assistant Libraries	1
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences	1
A Coq Formalization of Lebesgue Integration of Nonnegative Functions	1
Using Model Theory to Find Decidable and Tractable Description Logics with Concrete Domains	1
Larry Wos: Visions of Automated Reasoning	1
Formally-Verified Round-Off Error Analysis of Runge–Kutta Methods	1
Combining Stable Infiniteness and (Strong) Politeness	1
A Formalization and Proof Checker for Isabelle’s Metalogic	1
Double Auctions: Formalization and Automated Checkers	1
Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs	1