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

Article	Citations
Measuring the Readability of Geometric Proofs: The Area Method Case	15
Fast Left Kan Extensions Using the Chase	12
Experiences from Exporting Major Proof Assistant Libraries	8
Optimal Deterministic Controller Synthesis from Steady-State Distributions	7
Derivational Complexity and Context-Sensitive Rewriting	6
Human-Centered Automated Proof Search	6
Combining Stable Infiniteness and (Strong) Politeness	6
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences	5
Cyclic Hypersequent System for Transitive Closure Logic	5
Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL	5
Synthesising Programs with Non-trivial Constants	5
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq	4
Investigations into Proof Structures	4
Predicate Transformer Semantics for Hybrid Systems	4
Unifying Splitting	4
SAT Meets Tableaux for Linear Temporal Logic Satisfiability	4
A Proof Procedure for Separation Logic with Inductive Definitions and Data	4
Proof Complexity of Modal Resolution	3
Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow Embedding	3
Superposition for Higher-Order Logic	3
Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant	3
Automated Reasoning with Restricted Intensional Sets	3
Use and Abuse of Instance Parameters in the Lean Mathematical Library	3
An Automated Approach to the Collatz Conjecture	3
A Formalization and Proof Checker for Isabelle’s Metalogic	3

Correction to: A Unifying View on SMT-Based Software Verification	3
Formalized Functional Analysis with Semilinear Maps	3
Preface: Special Issue of Selected Extended Papers of CADE 2019	3
Linear Resources in Isabelle/HOL	3
Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic	2
First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification	2
Formalization of Ring Theory in PVS	2
Set of Support, Demodulation, Paramodulation: A Historical Perspective	2
An Automatically Verified Prototype of the Android Permissions System	2
Bisequent Calculus for Four-Valued Quasi-Relevant Logics: Cut Elimination and Interpolation	2
Mechanising Gödel–Löb Provability Logic in HOL Light	2
Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version	2
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq	2
Schematic Program Proofs with Abstract Execution	2
Larry Wos: Visions of Automated Reasoning	2
Formal Verification of Termination Criteria for First-Order Recursive Functions	2
Finding Normal Binary Floating-Point Factors Efficiently	2
Superposition with Lambdas	2
A Comprehensive Framework for Saturation Theorem Proving	2
Certified First-Order AC-Unification and Applications	2
A Formalization of the Smith Normal Form in Higher-Order Logic	1
A Formalization of the CHSH Inequality and Tsirelson’s Upper-bound in Isabelle/HOL	1
Binary Codes that do not Preserve Primitivity	1
Integrating Owicki–Gries for C11-Style Memory Models into Isabelle/HOL	1
Towards Formalising Schutz’ Axioms for Minkowski Spacetime in Isabelle/HOL	1
Model Completeness, Uniform Interpolants and Superposition Calculus	1
An Automatically Verified Prototype of the Tokeneer ID Station Specification	1
IsaVODEs: Interactive Verification of Cyber-Physical Systems at Scale	1
Correction to: Local is Best: Efficient Reductions to Modal Logic K	1
Finitary Type Theories With and Without Contexts	1
On the Importance of Domain Model Configuration for Automated Planning Engines	1
Computer-Assisted Proofs for Lyapunov Stability via Sums of Squares Certificates and Constructive Analysis	1
Theorem Proving as Constraint Solving with Coherent Logic	1
A Formalization of SQL with Nulls	1
Pardinus: A Temporal Relational Model Finder	1
A Wos Challenge Met	1
Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic	1
Automata Terms in a Lazy WSkS Decision Procedure	1
Analyzing Read-Once Cutting Plane Proofs in Horn Systems	1
Satisfiability of Non-linear Transcendental Arithmetic as a Certificate Search Problem	1
A Coq Formalization of Lebesgue Integration of Nonnegative Functions	1
Automated Generation of Geometry Proof Problems Based on Point Geometry Identity	1
General Clauses for SAT-Based Proof Search in Intuitionistic Propositional Logic	1
Correction to: Differential Dynamic Logic for Hybrid Systems	1