Accepted Papers

Christoph Benzmüller, Chad E. Brown, and Michael Kohlhase
Cut-Simulation in Impredicative Logics

Sean McLaughlin
An Interpretation of Isabelle/HOL in HOL Light

Robert Constable, Wojciech Moczydlowski
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics

Xiang Xue Jia, Jian Zhang
A Powerful Technique to Eliminate Isomorphism in Finite Model Search

Dexter Kozen, Christoph Kreitz, and Eva Richter
Automating Proofs in Category Theory

Jürgen Zimmer, Serge Autexier
The MathServe Framework for Semantic Web Reasoning Services

Boontawee Suntisrivaraporn, Franz Baader, and Carsten Lutz
CEL---A Practical Reasoner for Life Science Ontologies

Jordi Levy, Manfred Schmidt-Schauss, and Mateu Villaret
Stratified Context Unification is NP-complete

Assia Mahboubi
Proving formally the implementation of an efficient gcd algorithm for polynomials

Volker Sorge, Andreas Meier, Roy McCasland, and Simon Colton
The Automatic Construction of Isotopy Invariants

Roland Zumkeller
Formal Global Optimisation with Taylor Models

Joerg Endrullis, Johannes Waldmann, and Hans Zantema
Matrix Interpretations for Proving Termination of Term Rewriting

Benjamin Werner
On the strength of proof-irrelevant type theories

Amine Chaieb
Verifying mixed real-integer quantifier elimination

Adam Koprowski, Hans Zantema
Recursive Path Ordering for Infinite Labelled Rewrite Systems

Florian Rabe
First-Order Logic with Dependent Types

Dmitry Tsarkov, Ian Horrocks
FaCT++ Description Logic Reasoner: System Description

Maria Paola Bonacina, Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, and Daniele Zucchelli
Decidability and Undecidability Results for Nelson-Oppen and Rewrite-based Decision Procedures

Alexander Krauss
Partial Recursive Functions in Higher-Order Logic

Erik Reeber, Warren A. Hunt, Jr.
A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA)

Tobias Nipkow, Gertrud Bauer
Flyspeck I: Tame Graphs

John Harrison
Towards self-verification of HOL Light

Brigitte Pientka
Eliminating redundancy in higher-order unification:a lightweight approach

Sylvie Boldo
Pitfalls of a full floating-point proof: example on the formal proof of the Veltkamp/Dekker algorithms

Kaustuv Chaudhuri, Frank Pfenning, and Greg Price
A logical characterization of forward and backward chaining in the inverse method

Daria Walukiewicz-Chrząszcz, Jacek Chrząszcz
Consistency and Completeness of Rewriting in the Calculus of Constructions

Anna Zamansky, Arnon Avron
Canonical Gentzen-type calculi with (n,k)-ary quantifiers

Benjamin Grégoire, Laurent Théry
A purely functional library for modular arithmetic and its application to certifying large prime numbers

Andrei Paskevich
Connection Tableaux with Lazy Paramodulation

Chad E. Brown
Combining Type Theory and Untyped Set Theory

Viorica Sofronie-Stokkermans
Interpolation in local theory extensions

Peter Baumgartner, Renate Schmidt
Blocking and Other Enhancements for Bottom-Up Model Generation Methods

Bernhard Beckert, Andre Platzer
Dynamic Logic with Non-rigid Functions

Allen Van Gelder, Geoff Sutcliffe
Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation

Predrag Janicic, Pedro Quaresma
System Description: GCLCprover + GeoThms

Christian Urban, Stefan Berghofer
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL

Stephane Demri, Denis Lugiez
Presburger Modal Logic is Only PSPACE-complete

Florent Jacquemard, Michael Rusinowitch, and Laurent Vigneron
Tree automata with equality constraints modulo equational theories

David Toman, Grant Weddell
On Keys and Functional Dependencies as First-class Citizens in Description Logics

Shuvendu Lahiri, Madanlal Musuvathi
Solving Sparse Linear Constraints

Daniel Dougherty, Kathi Fisler, and Shriram Krishnamurthi
Specifying and Reasoning about Dynamic Access-Control Policies

Juergen Giesl, Peter Schneider-Kamp, and Rene Thiemann
AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework

Olga Grinchtein, Martin Leucker, and Nir Piterman
Inferring Network Invariants Automatically

Hans de Nivelle, Jia Meng
Geometric Resolution: A Proof Procedure Based on Finite Model Search

Roy Dyckhoff, Delia Kesner, and Stephane Lengrand
Strong cut-elimination systems for Hudelmaier's depth-bounded sequent calculus for implicational logic

Geoff Sutcliffe, Stephan Schulz, Koen Claessen, and Allen Van Gelder
Using the TPTP Language for Writing Derivations and Finite Interpretations

Steven Obua, Sebastian Skalberg
Importing HOL into Isabelle/HOL

Joe Hendrix, Jose Meseguer, and Hitoshi Ohsaki
A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms

Yevgeny Kazakov, Boris Motik
A Resolution-Based Decision Procedure for SHOIQ