Front matter
677
A Dynamic Programming Approach to Categorial Deduction
Philippe de Groote
676
Tractable Transformations from Modal Provability Logics into First-Order Logic
Stéephane Demri and Rajeev Goré
675
Decision Procedures for Guarded Logics
Erich Grädel
674
A PSpace Algorithm for Graded Modal Logic
Stephan Tobies
675
Solvability of Context Equations with Two Context Variables Is Decidable
Manfred Schmidt-Schauß and Klaus U. Schulz
673
Complexity of the Higher Order Matching
ToMasz Wierzbicki
677
Solving Equational Problems Efficiently
Reinhard Pichler
677
VSDITLU: A Verifiable Symbolic Definite Integral Table Look-Up
A. A. Adams, H. Gottliebsen, S. A. Linton and U. Martin
679
A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers
Predrag Janičić, Alan Bundy and Ian Green
70
Presenting Proofs in a Human-Oriented Way
Helmut Horacek
70
On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results
Viorica Sofronie-Stokkermans
678
Maslov’s Class K Revisited
Ullrich Hustadt and Renate A. Schmidt
677
Prefixed Resolution: A Resolution Method for Modal and Description Logics
Carlos Areces, Hans de Nivelle and Maarten de Rijke
679
System Description: Twelf — A Meta-Logical Framework for Deductive Systems
Frank Pfenning and Carsten Schürmann
676
System Description: inka 5.0 - A Logic Voyager
Serge Autexier, Dieter Hutter, Heiko Mantel and Axel Schairer
678
System Description: CutRes 0.1: Cut Elimination by Resolution
Matthias Baaz, Alexander Leitsch and Georg Moser
676
System Description: MathWeb
, an Agent-Based Communication Layer for Distributed Automated Theorem Proving
Andreas Franke and Michael Kohlhase
70
System Description Using OBDD’s for the Validationof Skolem Verification Conditions
E. Pascal Gribomont and Nachaat Salloum
675
Fault-Tolerant Distributed Theorem Proving
Jason Hickey
680
System Description: Waldmeister — Improvements in Performance and Ease of Use
Thomas Hillenbrand, Andreas Jaeger and Bernd Löchner
674
Formal Metatheory Using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems
Amy P. Felty, Douglas J. Howe and Abhik Roychoudhury
674
A Formalization of Static Analyses in System
F
Frédéric Prost
678
On Explicit Reflection in Theorem Proving and Formal Verification
Sergei N. Artemov
677
System Description: Kimba, A Model Generator for Many-Valued First-Order Logics
Karsten Konrad and D. A. Wolfram
679
System Description: Teyjus—A Compiler and Abstract Machine Based Implementation of λProlog
Gopalan Nadathur and Dustin J. Mitchell
674
Vampire
Alexandre Riazanov and Andrei Voronkov
676
System Abstract: E 0.3
Stephan Schulz
676
Invited Talk: Rewrite-Based Deduction and Symbolic Constraints
Robert Nieuwenhuis
70
Towards an Automatic Analysis of Security Protocols in First-Order Logic
Christoph Weidenbach
680
A Confluent Connection Calculus
Peter Baumgartner, Norbert Eisinger and Ulrich Furbach
675
Abstraction-Based Relevancy Testing for Model Elimination
Marc Fuchs and Dirk Fuchs
679
A Breadth-First Strategy for Mating Search
Matthew Bishop
676
The Design of the CADE-16 Inductive Theorem Prover Contest
Dieter Hutter and Alan Bundy
680
System Description: Spass
Version 1.0.0
Christoph Weidenbach, Bijan Afshordel, Uwe Brahm, Christian Cohrs and Thorsten Engel, et al.
678
K
: A Theorem Prover for K
Andrei Voronkov
674
System Description:
CYNTHIA
Jon Whittle, Alan Bundy, Richard Boulton and Helen Lowe
676-677
System Description: MCS: Model-Based Conjecture Searching
Jian Zhang
678
Embedding Programming Languages in Theorem Provers
Tobias Nipkow
678
Extensional Higher-Order Paramodulation and RUE-Resolution
Christoph Benzmüller
680
Automatic Generation of Proof Search Strategies for Second-Order Logic
Raul H. C. Lopes
Back matter