


Остановите войну!
for scientists:


default search action
Journal of Automated Reasoning, Volume 58
Volume 58, Number 1, January 2017
- Stéphane Demri, Deepak Kapur, Christoph Weidenbach
:
Preface - Special Issue of Selected Extended Papers of IJCAR 2014. 1-2 - Jürgen Giesl
, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn
, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp
, Thomas Ströder, Stephanie Swiderski, René Thiemann
:
Analyzing Program Termination and Complexity Automatically with AProVE. 3-31 - Thomas Ströder, Jürgen Giesl
, Marc Brockschmidt, Florian Frohn
, Carsten Fuhs, Jera Hensel, Peter Schneider-Kamp
, Cornelius Aschermann:
Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic. 33-65 - Ismail Ilkan Ceylan, Rafael Peñaloza
:
The Bayesian Ontology Language $$\mathcal {BEL}$$ BEL. 67-95 - Marijn J. H. Heule
, Martina Seidl, Armin Biere
:
Solution Validation and Extraction for QBF Preprocessing. 97-125 - Aleksandar Zeljic
, Christoph M. Wintersteiger
, Philipp Rümmer:
An Approximation Framework for Solvers and Decision Procedures. 127-147 - Jasmin Christian Blanchette
, Andrei Popescu, Dmitriy Traytel
:
Soundness and Completeness Proofs by Coinductive Methods. 149-179 - Michael Beeson
, Larry Wos:
Finding Proofs in Tarskian Geometry. 181-207
Volume 58, Number 2, February 2017
- Gabriel Braun, Julien Narboux
:
A Synthetic Proof of Pappus' Theorem in Tarski's Geometry. 209-230 - Ana Cristina Rocha Oliveira, André Luiz Galdino, Mauricio Ayala-Rincón
:
Confluence of Orthogonal Term Rewriting Systems in the Prototype Verification System. 231-251 - M. Ganesalingam, W. T. Gowers:
A Fully Automatic Theorem Prover with Human-Style Output. 253-291 - Alexander Baumgartner, Temur Kutsia
, Jordi Levy
, Mateu Villaret
:
Higher-Order Pattern Anti-Unification in Linear Time. 293-310
Volume 58, Number 3, March 2017
- Amy P. Felty
, Aart Middeldorp
:
Preface: Selected Extended Papers of CADE 2015. 311-312 - Edward Zulkoski
, Curtis Bright
, Albert Heinle, Ilias S. Kotsireas, Krzysztof Czarnecki, Vijay Ganesh
:
Combining SAT Solvers with Computer Algebra Systems to Verify Combinatorial Conjectures. 313-339 - Andrew Reynolds, Jasmin Christian Blanchette
:
A Decision Procedure for (Co)datatypes in SMT Solvers. 341-362 - Vijay D'Silva, Caterina Urban:
Abstract Interpretation as Automated Deduction. 363-390 - José Iborra, Naoki Nishida, Germán Vidal
, Akihisa Yamada
:
Relative Termination via Dependency Pairs. 391-411
Volume 58, Number 4, April 2017
- Jean-Marie Lagniez, Pierre Marquis:
On Preprocessing Techniques and Their Impact on Propositional Model Counting. 413-481 - Manuel Eberl
:
Proving Divide and Conquer Complexities in Isabelle/HOL. 483-508 - Jesús Aransay
, Jose Divasón
:
A Formalisation in HOL of the Fundamental Theorem of Linear Algebra and Its Application to the Solution of the Least Squares Problem. 509-535

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.