[DL] Accepted papers to CADE-19

[Christopher Lynch]

Accepted Papers to CADE-19 in Miami
July 28 - August 2
http://www.cade-19.info/
Stay tuned for registration information

--------------------------------------------------------------------------------

Research Papers 

Unification modulo ACUI plus Homomorphisms/Distributivity
Siva Anantharaman, Paliath Narendran, Michael Rusinowitch 

Superposition with Equivalence Reasoning and Delayed Clause Normal Form
Transformation
Harald Ganzinger, J|rgen Stuber 

A Principle for Incorporating Axioms into the First-Order Translation of
Modal Formulae
Renate A. Schmidt, Ullrich Hustadt 

Matching in a Class of Combined Non-Disjoint Theories
Christophe Ringeissen 

Reasoning about iteration in Goedel's class theory
Johan G. F. Belinfante 

Optimizing a BDD-based Modal Solver
Guoqiang Pan, Moshe Y. Vardi 

Efficient instance retrieval with standard and relational path indexing
Alexandre Riazanov, Andrei Voronkov 

AC-compatible Knuth-Bendix Orderings
Konstantin Korovin, Andrei Voronkov 

Canonization for disjoint unions of theories
Sava Krstic, Sylvain Conchon 

Optimizing higher-order pattern unification
Brigitte Pientka, Frank Pfenning 

Automating the Dependency Pair Method
Nao Hirokawa, Aart Middeldorp 

Proving Pointer Programs in Higher-Order Logic
Farhad Mehta, Tobias Nipkow 

The Complexity of Finite Model Reasoning in Description Logics
Carsten Lutz, Ulrike Sattler, Lidia Tendera 

Deciding Inductive Validity of Equations
J|rgen Giesl, Deepak Kapur 

Extraction of Short Natural Deduction Proofs from Resolution without Using
Choice Axioms
Hans de Nivelle 

Certifying solutions to permutation group problems
Arjeh Cohen, Scott Murray, Martin Pollet, Volker Sorge 

Monodic Temporal Resolution
Anatoly Degtyarev, Michael Fisher, Boris Konev 

A Translation of Alternating Automata to Description Logics
Jan Hladik, Ulrike Sattler 

Decidability of Arity-Bounded Higher-Order Matching
Manfred Schmidt-Schau_ 

A Metalogical Approach to Foundational Certified Code
Karl Crary, Susmit Sarkar 

Equational Abstractions
Jose Meseguer, Miguel Palomino, Narciso Marti-Oliet 

Adbmal
Dimitri Hendriks, Vincent van Oostrom 

Algorithms for Ordinal Arithmetic
Panagiotis Manolios, Daron Vroon 

The Model Evolution Calculus
Peter Baumgartner, Cesare Tinelli 

Superposition modulo a Shostak Theory
Harald Ganzinger, Thomas Hillenbrand, Uwe Waldmann 

Source-tracking Unification
Venkatesh Choppella, Christopher T. Haynes 

A Randomized Satisfiability Procedure for Arithmetic and Uninterpreted
Function Symbols
Sumit Gulwani, George C. Necula 

Subset types and partial functions
Aaron Stump 

Saturation Decision Procedures
Christopher Lynch 



System Descriptions 


The HOMER System
Simon Colton, Sophie Huczynska 

How to prove inductive theorems? Quodlibet!
J|rgen Avenhaus, Ulrich Kuehler, Tobias Schmidt-Samoa, Claus-Peter Wirth 

TRP 2.0: A temporal resolution prover
Ullrich Hustadt, Boris Konev 

IsaPlanner: A Prototype Proof Planner in Isabelle
Lucas Dixon, Jacques Fleuriot 

`Living Book` :- `Deduction`, `Slicing`, `Interaction`.
Peter Baumgartner, Ulrich Furbach, Margret Gross-Hardt, Alex Sinner 

About VeriFun
Christoph Walther, Stephan Schweitzer 

The New Waldmeister Loop at Work
Jean-Marie Gaillourdet, Thomas Hillenbrand, Bernd Lvchner, Hendrik Spies