Journal of Automated Reasoning

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-05-01 to 2024-05-01.)
ArticleCitations
TacticToe: Learning to Prove with Tactics15
ICE-Based Refinement Type Discovery for Higher-Order Functional Programs15
Extensional Higher-Order Paramodulation in Leo-III13
Certified Quantum Computation in Isabelle/HOL12
Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover11
Multi-cost Bounded Tradeoff Analysis in MDP9
Integrating Owicki–Gries for C11-Style Memory Models into Isabelle/HOL9
Superposition with Lambdas8
Automated Proof of Bell–LaPadula Security Properties7
Probably Partially True: Satisfiability for Łukasiewicz Infinitely-Valued Probabilistic Logic and Related Topics6
A Coq Formalization of Lebesgue Integration of Nonnegative Functions5
An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory Model5
Pardinus: A Temporal Relational Model Finder5
Automated Reasoning with Restricted Intensional Sets5
An Automatically Verified Prototype of the Tokeneer ID Station Specification5
Predicate Transformer Semantics for Hybrid Systems5
Model Completeness, Uniform Interpolants and Superposition Calculus4
Machine Learning Guidance for Connection Tableaux4
Chain Reduction for Binary and Zero-Suppressed Decision Diagrams4
Building Strategies into QBF Proofs4
Making Higher-Order Superposition Work3
Towards Satisfiability Modulo Parametric Bit-vectors3
A Formal Theory of Choreographic Programming3
A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines3
Experiences from Exporting Major Proof Assistant Libraries3
The Resolution of Keller’s Conjecture3
Simulating Strong Practical Proof Systems with Extended Resolution3
A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks with Applications to Probability Theory3
Proof-Producing Synthesis of CakeML from Monadic HOL Functions3
Synthesizing Precise and Useful Commutativity Conditions3
Fine-Grained Complexity of Safety Verification3
Automated Discovery of Geometric Theorems Based on Vector Equations3
Formalising $$\varSigma $$-Protocols and Commitment Schemes Using CryptHOL3
A Formalization of Dedekind Domains and Class Groups of Global Fields3
On the Importance of Domain Model Configuration for Automated Planning Engines3
A Comprehensive Framework for Saturation Theorem Proving3
0.01909613609314