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

Article	Citations
ICE-Based Refinement Type Discovery for Higher-Order Functional Programs	15
TacticToe: Learning to Prove with Tactics	14
Extensional Higher-Order Paramodulation in Leo-III	13
Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover	11
Integrating Owicki–Gries for C11-Style Memory Models into Isabelle/HOL	9
Certified Quantum Computation in Isabelle/HOL	9
Multi-cost Bounded Tradeoff Analysis in MDP	8
Superposition with Lambdas	8
Probably Partially True: Satisfiability for Łukasiewicz Infinitely-Valued Probabilistic Logic and Related Topics	6
Automated Proof of Bell–LaPadula Security Properties	6
A Coq Formalization of Lebesgue Integration of Nonnegative Functions	5
An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory Model	5
An Automatically Verified Prototype of the Tokeneer ID Station Specification	4
Building Strategies into QBF Proofs	4
Model Completeness, Uniform Interpolants and Superposition Calculus	4
Predicate Transformer Semantics for Hybrid Systems	4
Machine Learning Guidance for Connection Tableaux	4
Automated Reasoning with Restricted Intensional Sets	4
A Comprehensive Framework for Saturation Theorem Proving	3
Simulating Strong Practical Proof Systems with Extended Resolution	3
A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks with Applications to Probability Theory	3
Proof-Producing Synthesis of CakeML from Monadic HOL Functions	3
A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines	3
Fine-Grained Complexity of Safety Verification	3
Automated Discovery of Geometric Theorems Based on Vector Equations	3

Formalising $$\varSigma $$-Protocols and Commitment Schemes Using CryptHOL	3
A Formalization of Dedekind Domains and Class Groups of Global Fields	3
On the Importance of Domain Model Configuration for Automated Planning Engines	3
Synthesizing Precise and Useful Commutativity Conditions	3
Experiences from Exporting Major Proof Assistant Libraries	3
Making Higher-Order Superposition Work	3
Towards Satisfiability Modulo Parametric Bit-vectors	3
Chain Reduction for Binary and Zero-Suppressed Decision Diagrams	3
Pardinus: A Temporal Relational Model Finder	3
Constructive Decision via Redundancy-Free Proof-Search	2
Parameterized Model Checking on the TSO Weak Memory Model	2
Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs	2
Using Model Theory to Find Decidable and Tractable Description Logics with Concrete Domains	2
Larry Wos: Visions of Automated Reasoning	2
Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL	2
Formalization of the Poincaré Disc Model of Hyperbolic Geometry	2
Combination of Uniform Interpolants via Beth Definability	2
Verifying Whiley Programs with Boogie	2
A Formal Theory of Choreographic Programming	2
Theorem Proving as Constraint Solving with Coherent Logic	2
Superposition for Higher-Order Logic	2
A Bi-Directional Extensible Interface Between Lean and Mathematica	2
The Resolution of Keller’s Conjecture	2
Formalization of the Computational Theory of a Turing Complete Functional Language Model	2
A Solver for Arrays with Concatenation	2
A Decidable Class of Security Protocols for Both Reachability and Equivalence Properties	2
Unbounded-Time Safety Verification of Guarded LTI Models with Inputs by Abstract Acceleration	2
Schematic Refutations of Formula Schemata	1
Local is Best: Efficient Reductions to Modal Logic K	1
Measure Construction by Extension in Dependent Type Theory with Application to Integration	1
A Resolution Proof System for Dependency Stochastic Boolean Satisfiability	1
Binary Codes that do not Preserve Primitivity	1
Decidable $${\exists }^{\forall }^$$ First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates	1
Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version	1
HO$$\pi $$ in Coq	1
A Formalization of the Smith Normal Form in Higher-Order Logic	1
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq	1
Human-Centered Automated Proof Search	1
Optimization Modulo the Theories of Signed Bit-Vectors and Floating-Point Numbers	1
Efficient Extensional Binary Tries	1
Polite Combination of Algebraic Datatypes	1
POSIX Lexing with Derivatives of Regular Expressions	1
A Wos Challenge Met	1
Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic	1
Correction to: Differential Dynamic Logic for Hybrid Systems	1
Formalization of Ring Theory in PVS	1
Cyclic Hypersequent System for Transitive Closure Logic	1
Measuring the Readability of Geometric Proofs: The Area Method Case	1
Tuple Interpretations for Termination of Term Rewriting	1
CoCon: A Conference Management System with Formally Verified Document Confidentiality	1

Craig Interpolation with Clausal First-Order Tableaux	1
From Specification to Testing: Semantics Engineering for Lua 5.2	1
A Formalization of SQL with Nulls	1
Analyzing Read-Once Cutting Plane Proofs in Horn Systems	1
A Formalization and Proof Checker for Isabelle’s Metalogic	1
Formalization of Euler–Lagrange Equation Set Based on Variational Calculus in HOL Light	1
Set of Support, Demodulation, Paramodulation: A Historical Perspective	1
Derivational Complexity and Context-Sensitive Rewriting	1