Journal of automated reasoning

Keyphrases

Publications

volume 67, number 2, 2023

Aart Middeldorp, Alexander Lochmann, Fabian Mitterwallner
First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification. Journal of automated reasoning 67 (2) (2023)
Gabriel Ebner, Jasmin Blanchette, Sophie Tourret
Unifying Splitting. Journal of automated reasoning 67 (2) (2023)
Gabriel Ebner, Jasmin Blanchette, Sophie Tourret
Unifying Splitting. Journal of automated reasoning 67 (2) (2023)
Alessandro Abate, Haniel Barbosa, Clark Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, Cesare Tinelli
Synthesising Programs with Non-trivial Constants. Journal of automated reasoning 67 (2) (2023)
Cezary Kaliszyk, Karol Pąk
Combining Higher-Order Logic with Set Theory Formalizations. Journal of automated reasoning 67 (2) (2023)

volume 66, number 3, 2022

Nicolas Peltier, Viorica Sofronie-Stokkermans
Special Issue of Selected Extended Papers of IJCAR 2020. Journal of automated reasoning 66 (3) (2022)

volume 66, number 4, 2022

Jose Divasón, René Thiemann
A Formalization of the Smith Normal Form in Higher-Order Logic. Journal of automated reasoning 66 (4) (2022)
Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette
A Comprehensive Framework for Saturation Theorem Proving. Journal of automated reasoning 66 (4) (2022)
Wilmer Ricciotti, James Cheney
A Formalization of SQL with Nulls. Journal of automated reasoning 66 (4) (2022)

2021

Pascal Fontaine
Preface: Special Issue of Selected Extended Papers of CADE 2019. Journal of automated reasoning (2021)

volume 66, number 1, 2021

Sarah Sigley, Olaf Beyersdorff
Proof Complexity of Modal Resolution. Journal of automated reasoning 66 (1) (2021)

volume 65, number 1, 2020

Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan
Building Strategies into QBF Proofs. Journal of automated reasoning 65 (1) (2020)

volume 65, number 2, 2020

Dario Cattaruzza, Alessandro Abate, Peter Schrammel, Daniel Kroening
Unbounded-Time Safety Verification of Guarded LTI Models with Inputs by Abstract Acceleration. Journal of automated reasoning 65 (2) (2020)
Michael Färber, Cezary Kaliszyk, Josef Urban
Machine Learning Guidance for Connection Tableaux. Journal of automated reasoning 65 (2) (2020)

volume 65, number 5, 2020

Anthony Bordg, Hanna Lachnitt, Yijun He
Certified Quantum Computation in Isabelle/HOL. Journal of automated reasoning 65 (5) (2020)

volume 64, number 5, 2020

René Thiemann, Ralph Bottesch, Jose Divasón, Max W Haslbeck, Sebastiaan J C Joosten, Akihisa Yamada
Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL. Journal of automated reasoning 64 (5) (2020)

volume 64, number 2, 2019

Wenda Li, Lawrence C Paulson
Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL. Journal of automated reasoning 64 (2) (2019)

volume 64, number 3, 2019

Marijn J H Heule, Benjamin Kiesl, Armin Biere
Strong Extension-Free Proof Systems. Journal of automated reasoning 64 (3) (2019)

volume 64, number 4, 2019

Jose Divasón, Sebastiaan J C Joosten, René Thiemann, Akihisa Yamada
A Verified Implementation of the Berlekamp-Zassenhaus Factorization Algorithm. Journal of automated reasoning 64 (4) (2019)

volume 64, number 3, 2018

Sebastiaan J C Joosten, René Thiemann, Akihisa Yamada
A Verified Implementation of Algebraic Numbers in Isabelle/HOL. Journal of automated reasoning 64 (3) (2018)

volume 63, number 1, 2018

Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider
Long-Distance Q-Resolution with Dependency Schemes. Journal of automated reasoning 63 (1) (2018)

volume 63, number 3, 2018

Olaf Beyersdorff, Joshua Blinkhorn, Leroy Chew, Renate Schmidt, Martin Suda
Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF. Journal of automated reasoning 63 (3) (2018)

volume 62, number 3, 2018

Alexander Leitsch, Anela Lolic
Extraction of Expansion Trees. Journal of automated reasoning 62 (3) (2018)

volume 61, number 1, 2018

Fabian Immler
A Verified ODE Solver and the Lorenz Attractor. Journal of automated reasoning 61 (1) (2018)
Cornelius Diekmann, Lars Hupel, Julius Michaelis, Maximilian Haslbeck, Georg Carle
Verified iptables Firewall Analysis and Verification. Journal of automated reasoning 61 (1) (2018)
Łukasz Czajka, Cezary Kaliszyk
Hammer for Coq: Automation for Dependent Type Theory. Journal of automated reasoning 61 (1) (2018)
Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, Christoph Weidenbach
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. Journal of automated reasoning 61 (1) (2018)

volume 62, number 1, 2017

Stijn de Gouw, Frank S de Boer, Richard Bubel, Reiner Hähnle, Jurriaan Rot, Dominic Steinhöfel
Verifying OpenJDK's Sort Method for Generic Collections. Journal of automated reasoning 62 (1) (2017)

volume 61, number 1, 2017

Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk
The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar. Journal of automated reasoning 61 (1) (2017)

volume 60, number 2, 2017

Zoltan A Kocsis, Jerry Swan
Genetic Programming + Proof Search = Automatic Improvement. Journal of automated reasoning 60 (2) (2017)

volume 60, number 4, 2017

Nicolas A Matentzoglu, Bijan Parsia, Uli Sattler
OWL Reasoning: Subsumption Test Hardness and Modularity. Journal of automated reasoning 60 (4) (2017)

volume 59, number 1, 2017

Moritz Sinn, Florian Zuleger, Helmut Veith
Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints. Journal of automated reasoning 59 (1) (2017)

volume 59, number 4, 2017

Bijan Parsia, Nicolas A Matentzoglu, Rafael S Gonçalves, Birte Glimm, Andreas Steigmiller
The OWL Reasoner Evaluation (ORE) 2015 Competition Report. Journal of automated reasoning 59 (4) (2017)

volume 58, number 1, 2016

Aleksandar Zeljić, Christoph M Wintersteiger, Philipp Rümmer
An Approximation Framework for Solvers and Decision Procedures. Journal of automated reasoning 58 (1) (2016)

volume 58, number 2, 2016

Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret
Higher-Order Pattern Anti-Unification in Linear Time. Journal of automated reasoning 58 (2) (2016)
M Ganesalingam, W T Gowers
A Fully Automatic Theorem Prover with Human-Style Output. Journal of automated reasoning 58 (2) (2016)

volume 58, number 3, 2016

José Iborra, Naoki Nishida, Germán Vidal, Akihisa Yamada
Relative Termination via Dependency Pairs. Journal of automated reasoning 58 (3) (2016)

volume 57, number 1, 2016

Matthias Schlaipfer, Georg Weissenbacher
Labelled Interpolation Systems for Hyper-Resolution, Clausal, and Local Proofs. Journal of automated reasoning 57 (1) (2016)

volume 57, number 4, 2016

Robbert Krebbers
A Formal C Memory Model for Separation Logic. Journal of automated reasoning 57 (4) (2016)

volume 56, number 3, 2016

Rob Arthan
On Definitions of Constants and Types in HOL. Journal of automated reasoning 56 (3) (2016)

volume 55, number 4, 2015

Christoph Benzmüller, Nik Sultana, Lawrence C Paulson, Frank Theiß
The Higher-Order Prover Leo-II. Journal of automated reasoning 55 (4) (2015)