OOIR: Observatory of International Research

Papers

(The TQCC of Journal of Automated Reasoning is 3. 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
Certified Quantum Computation in Isabelle/HOL	9
Integrating Owicki–Gries for C11-Style Memory Models into Isabelle/HOL	9
Multi-cost Bounded Tradeoff Analysis in MDP	8
Superposition with Lambdas	8
Automated Proof of Bell–LaPadula Security Properties	6
Probably Partially True: Satisfiability for Łukasiewicz Infinitely-Valued Probabilistic Logic and Related Topics	6
An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory Model	5
A Coq Formalization of Lebesgue Integration of Nonnegative Functions	5
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
An Automatically Verified Prototype of the Tokeneer ID Station Specification	4
Building Strategies into QBF Proofs	4
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
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