Top

Journal

Journal of Automated Reasoning

Issue 3/2020

Special Issue: Automated Reasoning Systems / Guest Editors: Armin Biere, Cesare Tinelli, Christoph Weidenbach & Special Issue: Selected Extended Papers of CADE 2017 / Guest Editor: Leonardo de Moura

Table of Contents ( 12 Articles )

13-08-2019 | Issue 3/2020

Preface to the Special Issue on Automated Reasoning Systems

Armin Biere, Cesare Tinelli, Christoph Weidenbach

09-12-2018 | Issue 3/2020 Open Access

A Verified Implementation of Algebraic Numbers in Isabelle/HOL

Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada

Download PDF-version View full text

17-12-2018 | Issue 3/2020

Limited Second-Order Functionality in a First-Order Setting

Matt Kaufmann, J Strother Moore

15-12-2018 | Issue 3/2020

OptiMathSAT: A Tool for Optimization Modulo Theories

Roberto Sebastiani, Patrick Trentin

17-12-2018 | Issue 3/2020 Open Access

A Resolution-Based Theorem Prover for : Architecture, Refinements, Strategies and Experiments

Cláudia Nalon, Ullrich Hustadt, Clare Dixon

Download PDF-version View full text

04-01-2019 | Issue 3/2020

Scalable Fine-Grained Proofs for Formula Processing

Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine

17-02-2020 | Issue 3/2020

Preface: Selected Extended Papers of CADE 2017

Leonardo de Moura

04-06-2019 | Issue 3/2020 Open Access

Efficient Verified (UN)SAT Certificate Checking

Peter Lammich

Download PDF-version View full text

22-02-2019 | Issue 3/2020 Open Access

Strong Extension-Free Proof Systems

Marijn J. H. Heule, Benjamin Kiesl, Armin Biere

Download PDF-version View full text

09-08-2019 | Issue 3/2020 Open Access

Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof

Gadi Tellez, James Brotherston

Download PDF-version View full text

04-01-2019 | Issue 3/2020

Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness

Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar

25-02-2020 | Issue 3/2020

SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment

Andreas Teucke, Christoph Weidenbach

Current Publications

Issue 1/2021

Issue 8/2020

Issue 7/2020

Issue 6/2020

Issue 5/2020

Issue 4/2020

Issue 3/2020

Issue 2/2020

Issue 1/2020

Issue 4/2019

Premium Partner

Image Credits

Springer Professional

Table of Contents ( 12 Articles )

Preface to the Special Issue on Automated Reasoning Systems

A Verified Implementation of Algebraic Numbers in Isabelle/HOL

Limited Second-Order Functionality in a First-Order Setting

OptiMathSAT: A Tool for Optimization Modulo Theories

A Resolution-Based Theorem Prover for : Architecture, Refinements, Strategies and Experiments

Scalable Fine-Grained Proofs for Formula Processing

Preface: Selected Extended Papers of CADE 2017

Efficient Verified (UN)SAT Certificate Checking

Strong Extension-Free Proof Systems

Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof

Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness

SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment

Current Publications

Issue 1/2021

Issue 8/2020

Issue 7/2020

Issue 6/2020

Issue 5/2020

Issue 4/2020

Issue 3/2020

Issue 2/2020

Issue 1/2020

Issue 4/2019

Premium Partner