


default search action
Journal of Automated Reasoning, Volume 51
Volume 51, Number 1, June 2013
- Nikolaj S. Bjørner, Viorica Sofronie-Stokkermans:

Preface: Special Issue of Selected Extended Papers of CADE-23. 1-2 - Didier Galmiche, Daniel Méry:

A Connection-based Characterization of Bi-intuitionistic Validity. 3-26 - Lars Noschinski, Fabian Emmes, Jürgen Giesl

:
Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs. 27-56 - Chad E. Brown:

Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems. 57-77 - Dejan Jovanovic, Leonardo Mendonça de Moura:

Cutting to the Chase - Solving Linear Integer Arithmetic. 79-108 - Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson

:
Extending Sledgehammer with SMT Solvers. 109-128
Volume 51, Number 2, August 2013
- Mauro Ferrari

, Camillo Fiorentini
, Guido Fiorino:
Contraction-Free Linear Depth Sequent Calculi for Intuitionistic Propositional Logic with the Subformula Property and Minimal Depth Counter-Models. 129-149 - César A. Muñoz, Anthony Narkawicz:

Formalization of Bernstein Polynomials and Applications to Global Optimization. 151-196 - Serenella Cerrito, Marta Cialdea Mayer

:
A Tableau Based Decision Procedure for an Expressive Fragment of Hybrid Logic with Binders, Converse and Global Modalities. 197-239
Volume 51, Number 3, October 2013
- Sandip Ray, Rob Sumners:

Specification and Verification of Concurrent Programs Through Refinements. 241-280 - Carles Creus, Guillem Godoy, Francesc Massanes, Ashish Tiwari:

Non-Linear Rewrite Closure and Weak Normalization. 281-324 - Christopher Lynch

, Quang-Trung Ta, Duc-Khanh Tran:
SMELS: Satisfiability Modulo Equality with Lazy Superposition. 325-356
Volume 51, Number 4, December 2013
- Christian Sternagel:

Proof Pearl - A Mechanized Proof of GHC's Mergesort. 357-370 - Carles Creus, Adrià Gascón, Guillem Godoy:

Emptiness and Finiteness for Tree Automata with Global Reflexive Disequality Constraints. 371-400 - Matthias Baaz

, Ori Lahav
, Anna Zamansky:
Finite-valued Semantics for Canonical Labelled Calculi. 401-430 - Alexei Lisitsa:

Finite Reasons for Safety - Parameterized Verification by Finite Model Finding. 431-451 - Clark W. Barrett

:
"Decision Procedures: An Algorithmic Point of View, " by Daniel Kroening and Ofer Strichman, Springer-Verlag, 2008. 453-456

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.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














