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 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
Pardinus: A Temporal Relational Model Finder	6
Automated Reasoning with Restricted Intensional Sets	6
An Automatically Verified Prototype of the Tokeneer ID Station Specification	6
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
Superposition for Higher-Order Logic	5
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
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
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

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
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
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