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

Article	Citations
Combining Stable Infiniteness and (Strong) Politeness	14
Optimal Deterministic Controller Synthesis from Steady-State Distributions	8
Investigations into Proof Structures	8
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences	8
Automated Reasoning with Restricted Intensional Sets	7
Human-Centered Automated Proof Search	7
Predicate Transformer Semantics for Hybrid Systems	6
A Proof Procedure for Separation Logic with Inductive Definitions and Data	5
Experiences from Exporting Major Proof Assistant Libraries	5
Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow Embedding	5
Synthesising Programs with Non-trivial Constants	5
Derivational Complexity and Context-Sensitive Rewriting	5
Unifying Splitting	4
SAT Meets Tableaux for Linear Temporal Logic Satisfiability	4
Cyclic Hypersequent System for Transitive Closure Logic	4
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq	4
Preface: Special Issue of Selected Extended Papers of CADE 2019	3
Fast Left Kan Extensions Using the Chase	3
Bisequent Calculus for Four-Valued Quasi-Relevant Logics: Cut Elimination and Interpolation	3
Mechanising Gödel–Löb Provability Logic in HOL Light	3
A Comprehensive Framework for Saturation Theorem Proving	3
Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL	3
Use and Abuse of Instance Parameters in the Lean Mathematical Library	3
Certified First-Order AC-Unification and Applications	3
Linear Resources in Isabelle/HOL	3

Measuring the Readability of Geometric Proofs: The Area Method Case	3
Formalized Functional Analysis with Semilinear Maps	3
Proof Complexity of Modal Resolution	3
Formal Verification of Termination Criteria for First-Order Recursive Functions	3
First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification	2
Formalization of Ring Theory in PVS	2
Schematic Program Proofs with Abstract Execution	2
Superposition with Lambdas	2
Set of Support, Demodulation, Paramodulation: A Historical Perspective	2
Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic	2
Larry Wos: Visions of Automated Reasoning	2
Finding Normal Binary Floating-Point Factors Efficiently	2
Correction to: Local is Best: Efficient Reductions to Modal Logic K	2
A Formalization of the Smith Normal Form in Higher-Order Logic	2
A Formalization and Proof Checker for Isabelle’s Metalogic	2
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq	2
Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant	2
Superposition for Higher-Order Logic	2
Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version	2
Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic	2
An Automated Approach to the Collatz Conjecture	2