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 2020-11-01 to 2024-11-01.)

Article	Citations
Extensional Higher-Order Paramodulation in Leo-III	15
Certified Quantum Computation in Isabelle/HOL	13
Integrating Owicki–Gries for C11-Style Memory Models into Isabelle/HOL	12
Superposition with Lambdas	8
The Resolution of Keller’s Conjecture	7
An Automatically Verified Prototype of the Tokeneer ID Station Specification	6
Pardinus: A Temporal Relational Model Finder	6
Automated Reasoning with Restricted Intensional Sets	6
Superposition for Higher-Order Logic	5
A Comprehensive Framework for Saturation Theorem Proving	5
A Coq Formalization of Lebesgue Integration of Nonnegative Functions	5
Predicate Transformer Semantics for Hybrid Systems	5
Towards Satisfiability Modulo Parametric Bit-vectors	4
Model Completeness, Uniform Interpolants and Superposition Calculus	4
A Formalization of Dedekind Domains and Class Groups of Global Fields	4
Experiences from Exporting Major Proof Assistant Libraries	4
Automated Discovery of Geometric Theorems Based on Vector Equations	4
On the Importance of Domain Model Configuration for Automated Planning Engines	4
A Bi-Directional Extensible Interface Between Lean and Mathematica	3
Efficient Extensional Binary Tries	3
A Solver for Arrays with Concatenation	3
Larry Wos: Visions of Automated Reasoning	3
Combination of Uniform Interpolants via Beth Definability	3
A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks with Applications to Probability Theory	3
A Formal Theory of Choreographic Programming	3

Making Higher-Order Superposition Work	3
Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs	3
Using Model Theory to Find Decidable and Tractable Description Logics with Concrete Domains	3
A Formalization of SQL with Nulls	3
Measure Construction by Extension in Dependent Type Theory with Application to Integration	2
Polite Combination of Algebraic Datatypes	2
Analyzing Read-Once Cutting Plane Proofs in Horn Systems	2
Formalization of Ring Theory in PVS	2
A Proof Procedure for Separation Logic with Inductive Definitions and Data	2
Optimization Modulo the Theories of Signed Bit-Vectors and Floating-Point Numbers	2
Formalization of the Computational Theory of a Turing Complete Functional Language Model	2
POSIX Lexing with Derivatives of Regular Expressions	2
Theorem Proving as Constraint Solving with Coherent Logic	2
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq	2
Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL	2
Verifying Whiley Programs with Boogie	2
Craig Interpolation with Clausal First-Order Tableaux	2
A Wos Challenge Met	2
Set of Support, Demodulation, Paramodulation: A Historical Perspective	2
Cyclic Hypersequent System for Transitive Closure Logic	2
Derivational Complexity and Context-Sensitive Rewriting	1
Schematic Refutations of Formula Schemata	1
Tuple Interpretations for Termination of Term Rewriting	1
Gale-Shapley Verified	1
Formally-Verified Round-Off Error Analysis of Runge–Kutta Methods	1
Binary Codes that do not Preserve Primitivity	1
Schematic Program Proofs with Abstract Execution	1
Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version	1
SAT Meets Tableaux for Linear Temporal Logic Satisfiability	1
Measuring the Readability of Geometric Proofs: The Area Method Case	1
Local is Best: Efficient Reductions to Modal Logic K	1
Verifying the Generalization of Deep Learning to Out-of-Distribution Domains	1
A Resolution Proof System for Dependency Stochastic Boolean Satisfiability	1
Faster Linear Unification Algorithm	1
A Formalization and Proof Checker for Isabelle’s Metalogic	1
Correction to: Differential Dynamic Logic for Hybrid Systems	1
Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic	1
Synthesising Programs with Non-trivial Constants	1
Human-Centered Automated Proof Search	1
Lower Bounds for QCDCL via Formula Gauge	1
Should Decisions in QCDCL Follow Prefix Order?	1
Engel’s Theorem in Mathlib	1
From Specification to Testing: Semantics Engineering for Lua 5.2	1
An Automatically Verified Prototype of the Android Permissions System	1
A Formalization of the Smith Normal Form in Higher-Order Logic	1
An Automated Approach to the Collatz Conjecture	1