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 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
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
Proof Complexity of Modal Resolution	3
Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow Embedding	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