CADE 2013 - LNAI 7898

Author Index

A B C D E F G H I J K L M N O P Q R S T U V W X Y Z

Ábrahám, Erika

A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition
U. Loup, K. Scheibler, F. Corzilius, E. Ábrahám, and B. Becker
LNAI 7898, p. 193 ff.
Abstract | Full article in PDF | BibTeX

Azmy, Noran

Computing Tiny Clause Normal Forms
N. Azmy and C. Weidenbach
LNAI 7898, p. 109 ff.
Abstract | Full article in PDF | BibTeX

Baader, Franz

Temporalizing Ontology-Based Data Access
F. Baader, S. Borgwardt, and M. Lippmann
LNAI 7898, p. 330 ff.
Abstract | Full article in PDF | BibTeX

Barrett, Clark

Quantifier Instantiation Techniques for Finite Model Finding in SMT
A. Reynolds, C. Tinelli, A. Goel, S. Krsti $\'{c}$ , M. Deters, and C. Barrett
LNAI 7898, p. 377 ff.
Abstract | Full article in PDF | BibTeX

Baumgartner, Peter

Hierarchic Superposition with Weak Abstraction
P. Baumgartner and U. Waldmann
LNAI 7898, p. 39 ff.
Abstract | Full article in PDF | BibTeX

Becker, Bernd

Beckert, Bernhard

Analysing Vote Counting Algorithms via Logic
B. Beckert, R. Goré, and C. Schürmann
LNAI 7898, p. 135 ff.
Abstract | Full article in PDF | BibTeX

Dynamic Logic with Trace Semantics
B. Beckert and D. Bruns
LNAI 7898, p. 315 ff.
Abstract | Full article in PDF | BibTeX

Bender, Markus

System Description: E-KRHyper 1.4
M. Bender, B. Pelzer, and C. Schon
LNAI 7898, p. 126 ff.
Abstract | Full article in PDF | BibTeX

Biere, Armin

$\hbox{\sc bv2epr}$ : A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into $\hbox{\sc EPR}$
G. Kovásznai, A. Fröhlich, and A. Biere
LNAI 7898, p. 443 ff.
Abstract | Full article in PDF | BibTeX

Blanchette, Jasmin Christian

TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
J.C. Blanchette and A. Paskevich
LNAI 7898, p. 414 ff.
Abstract | Full article in PDF | BibTeX

Borgwardt, Stefan

Temporalizing Ontology-Based Data Access
F. Baader, S. Borgwardt, and M. Lippmann
LNAI 7898, p. 330 ff.
Abstract | Full article in PDF | BibTeX

Bruns, Daniel

Dynamic Logic with Trace Semantics
B. Beckert and D. Bruns
LNAI 7898, p. 315 ff.
Abstract | Full article in PDF | BibTeX

Bubel, Richard

Reuse in Software Verification by Abstract Method Calls
R. Hähnle, I. Schaefer, and R. Bubel
LNAI 7898, p. 300 ff.
Abstract | Full article in PDF | BibTeX

Chihani, Zakaria

Foundational Proof Certificates in First-Order Logic
Z. Chihani, D. Miller, and F. Renaud
LNAI 7898, p. 162 ff.
Abstract | Full article in PDF | BibTeX

Cialdea Mayer, Marta

A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies
M. Cialdea Mayer
LNAI 7898, p. 76 ff.
Abstract | Full article in PDF | BibTeX

Claessen, Koen

Automating Inductive Proofs Using Theory Exploration
K. Claessen, M. Johansson, D. Rosén, and N. Smallbone
LNAI 7898, p. 392 ff.
Abstract | Full article in PDF | BibTeX

Clarke, Edmund M.

dReal: An SMT Solver for Nonlinear Theories over the Reals
S. Gao, S. Kong, and E.M. Clarke
LNAI 7898, p. 208 ff.
Abstract | Full article in PDF | BibTeX

Comon-Lundh, Hubert

Tractable Inference Systems: An Extension with a Deducibility Predicate
H. Comon-Lundh, V. Cortier, and G. Scerri
LNAI 7898, p. 91 ff.
Abstract | Full article in PDF | BibTeX

Cortier, Véronique

Tractable Inference Systems: An Extension with a Deducibility Predicate
H. Comon-Lundh, V. Cortier, and G. Scerri
LNAI 7898, p. 91 ff.
Abstract | Full article in PDF | BibTeX

Corzilius, Florian

de Moura, Leonardo

Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals
L. de Moura and G.O. Passmore
LNAI 7898, p. 178 ff.
Abstract | Full article in PDF | BibTeX

Deters, Morgan

Erbatur, Serdar

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis
S. Erbatur, S. Escobar, D. Kapur, Z. Liu, C.A. Lynch, C. Meadows, J. Meseguer, P. Narendran, S. Santiago, and R. Sasse
LNAI 7898, p. 231 ff.
Abstract | Full article in PDF | BibTeX

Hierarchical Combination
S. Erbatur, D. Kapur, A.M. Marshall, P. Narendran, and C. Ringeissen
LNAI 7898, p. 249 ff.
Abstract | Full article in PDF | BibTeX

Escobar, Santiago

Filliâtre, Jean-Christophe

One Logic to Use Them All
J.-C. Filliâtre
LNAI 7898, p. 1 ff.
Abstract | Full article in PDF | BibTeX

Fröhlich, Andreas

Gange, Graeme

Solving Difference Constraints over Modular Arithmetic
G. Gange, H. Søndergaard, P.J. Stuckey, and P. Schachte
LNAI 7898, p. 215 ff.
Abstract | Full article in PDF | BibTeX

Gao, Sicun

dReal: An SMT Solver for Nonlinear Theories over the Reals
S. Gao, S. Kong, and E.M. Clarke
LNAI 7898, p. 208 ff.
Abstract | Full article in PDF | BibTeX

Goel, Amit

Goré, Rajeev

Analysing Vote Counting Algorithms via Logic
B. Beckert, R. Goré, and C. Schürmann
LNAI 7898, p. 135 ff.
Abstract | Full article in PDF | BibTeX

An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System Description
R. Goré and J. Thomson
LNAI 7898, p. 275 ff.
Abstract | Full article in PDF | BibTeX

Hähnle, Reiner

Reuse in Software Verification by Abstract Method Calls
R. Hähnle, I. Schaefer, and R. Bubel
LNAI 7898, p. 300 ff.
Abstract | Full article in PDF | BibTeX

Hawblitzel, Chris

Towards Modularly Comparing Programs Using Automated Theorem Provers
C. Hawblitzel, M. Kawaguchi, S.K. Lahiri, and H. Rebêlo
LNAI 7898, p. 282 ff.
Abstract | Full article in PDF | BibTeX

Heule, Marijn J.H.

Verifying Refutations with Extended Resolution
M.J.H. Heule, W.A. Hunt Jr., and N. Wetzler
LNAI 7898, p. 345 ff.
Abstract | Full article in PDF | BibTeX

Hoder, Kryštof

The 481 Ways to Split a Clause and Deal with Propositional Variables
K. Hoder and A. Voronkov
LNAI 7898, p. 450 ff.
Abstract | Full article in PDF | BibTeX

Hunt Jr., Warren A.

Verifying Refutations with Extended Resolution
M.J.H. Heule, W.A. Hunt Jr., and N. Wetzler
LNAI 7898, p. 345 ff.
Abstract | Full article in PDF | BibTeX

Iosif, Radu

The Tree Width of Separation Logic with Recursive Definitions
R. Iosif, A. Rogalewicz, and J. Simacek
LNAI 7898, p. 21 ff.
Abstract | Full article in PDF | BibTeX

Johansson, Moa

Automating Inductive Proofs Using Theory Exploration
K. Claessen, M. Johansson, D. Rosén, and N. Smallbone
LNAI 7898, p. 392 ff.
Abstract | Full article in PDF | BibTeX

Kaliszyk, Cezary

PRocH: Proof Reconstruction for HOL Light
C. Kaliszyk and J. Urban
LNAI 7898, p. 267 ff.
Abstract | Full article in PDF | BibTeX

Kaminski, Mark

InKreSAT: Modal Reasoning via Incremental Reduction to SAT
M. Kaminski and T. Tebbi
LNAI 7898, p. 436 ff.
Abstract | Full article in PDF | BibTeX

Kapur, Deepak

Hierarchical Combination
S. Erbatur, D. Kapur, A.M. Marshall, P. Narendran, and C. Ringeissen
LNAI 7898, p. 249 ff.
Abstract | Full article in PDF | BibTeX

Kawaguchi, Ming

Towards Modularly Comparing Programs Using Automated Theorem Provers
C. Hawblitzel, M. Kawaguchi, S.K. Lahiri, and H. Rebêlo
LNAI 7898, p. 282 ff.
Abstract | Full article in PDF | BibTeX

Kersani, Abdelkader

Completeness and Decidability Results for First-Order Clauses with Indices
A. Kersani and N. Peltier
LNAI 7898, p. 58 ff.
Abstract | Full article in PDF | BibTeX

Konev, Boris

Propositional Temporal Proving with Reductions to a SAT Problem
R. Williams and B. Konev
LNAI 7898, p. 421 ff.
Abstract | Full article in PDF | BibTeX

Kong, Soonho

dReal: An SMT Solver for Nonlinear Theories over the Reals
S. Gao, S. Kong, and E.M. Clarke
LNAI 7898, p. 208 ff.
Abstract | Full article in PDF | BibTeX

Kovásznai, Gergely

Krsti $\'{c}$ , Sava

Kühlwein, Daniel

E-MaLeS 1.1
D. Kühlwein, S. Schulz, and J. Urban
LNAI 7898, p. 407 ff.
Abstract | Full article in PDF | BibTeX

Lahiri, Shuvendu K.

Towards Modularly Comparing Programs Using Automated Theorem Provers
C. Hawblitzel, M. Kawaguchi, S.K. Lahiri, and H. Rebêlo
LNAI 7898, p. 282 ff.
Abstract | Full article in PDF | BibTeX

Lippmann, Marcel

Temporalizing Ontology-Based Data Access
F. Baader, S. Borgwardt, and M. Lippmann
LNAI 7898, p. 330 ff.
Abstract | Full article in PDF | BibTeX

Liu, Zhiqiang

Loup, Ulrich

Lynch, Christopher A.

Marshall, Andrew M.

Hierarchical Combination
S. Erbatur, D. Kapur, A.M. Marshall, P. Narendran, and C. Ringeissen
LNAI 7898, p. 249 ff.
Abstract | Full article in PDF | BibTeX

Meadows, Catherine

Meseguer, José

Miller, Dale

Foundational Proof Certificates in First-Order Logic
Z. Chihani, D. Miller, and F. Renaud
LNAI 7898, p. 162 ff.
Abstract | Full article in PDF | BibTeX

Narendran, Paliath

Hierarchical Combination
S. Erbatur, D. Kapur, A.M. Marshall, P. Narendran, and C. Ringeissen
LNAI 7898, p. 249 ff.
Abstract | Full article in PDF | BibTeX

Paskevich, Andrei

TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
J.C. Blanchette and A. Paskevich
LNAI 7898, p. 414 ff.
Abstract | Full article in PDF | BibTeX

Passmore, Grant Olney

Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals
L. de Moura and G.O. Passmore
LNAI 7898, p. 178 ff.
Abstract | Full article in PDF | BibTeX

Peltier, Nicolas

Completeness and Decidability Results for First-Order Clauses with Indices
A. Kersani and N. Peltier
LNAI 7898, p. 58 ff.
Abstract | Full article in PDF | BibTeX

Pelzer, Björn

System Description: E-KRHyper 1.4
M. Bender, B. Pelzer, and C. Schon
LNAI 7898, p. 126 ff.
Abstract | Full article in PDF | BibTeX

Rebêlo, Henrique

Towards Modularly Comparing Programs Using Automated Theorem Provers
C. Hawblitzel, M. Kawaguchi, S.K. Lahiri, and H. Rebêlo
LNAI 7898, p. 282 ff.
Abstract | Full article in PDF | BibTeX

Renaud, Fabien

Foundational Proof Certificates in First-Order Logic
Z. Chihani, D. Miller, and F. Renaud
LNAI 7898, p. 162 ff.
Abstract | Full article in PDF | BibTeX

Reynolds, Andrew

Ringeissen, Christophe

Hierarchical Combination
S. Erbatur, D. Kapur, A.M. Marshall, P. Narendran, and C. Ringeissen
LNAI 7898, p. 249 ff.
Abstract | Full article in PDF | BibTeX

Rogalewicz, Adam

The Tree Width of Separation Logic with Recursive Definitions
R. Iosif, A. Rogalewicz, and J. Simacek
LNAI 7898, p. 21 ff.
Abstract | Full article in PDF | BibTeX

Rosén, Dan

Automating Inductive Proofs Using Theory Exploration
K. Claessen, M. Johansson, D. Rosén, and N. Smallbone
LNAI 7898, p. 392 ff.
Abstract | Full article in PDF | BibTeX

Santiago, Sonia

Sasse, Ralf

Scerri, Guillaume

Tractable Inference Systems: An Extension with a Deducibility Predicate
H. Comon-Lundh, V. Cortier, and G. Scerri
LNAI 7898, p. 91 ff.
Abstract | Full article in PDF | BibTeX

Schachte, Peter

Solving Difference Constraints over Modular Arithmetic
G. Gange, H. Søndergaard, P.J. Stuckey, and P. Schachte
LNAI 7898, p. 215 ff.
Abstract | Full article in PDF | BibTeX

Schaefer, Ina

Reuse in Software Verification by Abstract Method Calls
R. Hähnle, I. Schaefer, and R. Bubel
LNAI 7898, p. 300 ff.
Abstract | Full article in PDF | BibTeX

Scheibler, Karsten

Schon, Claudia

System Description: E-KRHyper 1.4
M. Bender, B. Pelzer, and C. Schon
LNAI 7898, p. 126 ff.
Abstract | Full article in PDF | BibTeX

Schulz, Stephan

E-MaLeS 1.1
D. Kühlwein, S. Schulz, and J. Urban
LNAI 7898, p. 407 ff.
Abstract | Full article in PDF | BibTeX

Schürmann, Carsten

Analysing Vote Counting Algorithms via Logic
B. Beckert, R. Goré, and C. Schürmann
LNAI 7898, p. 135 ff.
Abstract | Full article in PDF | BibTeX

Shankar, Natarajan

Automated Reasoning, Fast and Slow
N. Shankar
LNAI 7898, p. 145 ff.
Abstract | Full article in PDF | BibTeX

Simacek, Jiri

The Tree Width of Separation Logic with Recursive Definitions
R. Iosif, A. Rogalewicz, and J. Simacek
LNAI 7898, p. 21 ff.
Abstract | Full article in PDF | BibTeX

Smallbone, Nicholas

Automating Inductive Proofs Using Theory Exploration
K. Claessen, M. Johansson, D. Rosén, and N. Smallbone
LNAI 7898, p. 392 ff.
Abstract | Full article in PDF | BibTeX

Sofronie-Stokkermans, Viorica

Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems
V. Sofronie-Stokkermans
LNAI 7898, p. 360 ff.
Abstract | Full article in PDF | BibTeX

Søndergaard, Harald

Solving Difference Constraints over Modular Arithmetic
G. Gange, H. Søndergaard, P.J. Stuckey, and P. Schachte
LNAI 7898, p. 215 ff.
Abstract | Full article in PDF | BibTeX

Stuckey, Peter J.

Solving Difference Constraints over Modular Arithmetic
G. Gange, H. Søndergaard, P.J. Stuckey, and P. Schachte
LNAI 7898, p. 215 ff.
Abstract | Full article in PDF | BibTeX

Tebbi, Tobias

InKreSAT: Modal Reasoning via Incremental Reduction to SAT
M. Kaminski and T. Tebbi
LNAI 7898, p. 436 ff.
Abstract | Full article in PDF | BibTeX

Thomson, Jimmy

An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System Description
R. Goré and J. Thomson
LNAI 7898, p. 275 ff.
Abstract | Full article in PDF | BibTeX

Tinelli, Cesare

Urban, Josef

PRocH: Proof Reconstruction for HOL Light
C. Kaliszyk and J. Urban
LNAI 7898, p. 267 ff.
Abstract | Full article in PDF | BibTeX

E-MaLeS 1.1
D. Kühlwein, S. Schulz, and J. Urban
LNAI 7898, p. 407 ff.
Abstract | Full article in PDF | BibTeX

Voronkov, Andrei

The 481 Ways to Split a Clause and Deal with Propositional Variables
K. Hoder and A. Voronkov
LNAI 7898, p. 450 ff.
Abstract | Full article in PDF | BibTeX

Waldmann, Uwe

Hierarchic Superposition with Weak Abstraction
P. Baumgartner and U. Waldmann
LNAI 7898, p. 39 ff.
Abstract | Full article in PDF | BibTeX

Weidenbach, Christoph

Computing Tiny Clause Normal Forms
N. Azmy and C. Weidenbach
LNAI 7898, p. 109 ff.
Abstract | Full article in PDF | BibTeX

Wetzler, Nathan

Verifying Refutations with Extended Resolution
M.J.H. Heule, W.A. Hunt Jr., and N. Wetzler
LNAI 7898, p. 345 ff.
Abstract | Full article in PDF | BibTeX

Williams, Richard

Propositional Temporal Proving with Reductions to a SAT Problem
R. Williams and B. Konev
LNAI 7898, p. 421 ff.
Abstract | Full article in PDF | BibTeX