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