16. CADE 1999:
Trento,
Italy
Harald Ganzinger (Ed.):
Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings.
Lecture Notes in Computer Science 1632 Springer 1999, ISBN 3-540-66222-7 BibTeX
@proceedings{DBLP:conf/cade/1999,
editor = {Harald Ganzinger},
title = {Automated Deduction - CADE-16, 16th International Conference
on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings},
booktitle = {CADE},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {1632},
year = {1999},
isbn = {3-540-66222-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
- Philippe de Groote:
A dynamic programming approach to categorial deduction.
1-15
Electronic Edition (Springer LINK) BibTeX
- Stéphane Demri, Rajeev Goré:
Tractable Transformations from Modal Provability Logics into First-Order Logic.
16-30
Electronic Edition (Springer LINK) BibTeX
- Erich Grädel:
Invited Talk: Decision procedures for guarded logics.
31-51
Electronic Edition (Springer LINK) BibTeX
- Stephan Tobies:
A PSpace Algorithm for Graded Modal Logic.
52-66
Electronic Edition (Springer LINK) BibTeX
- Manfred Schmidt-Schauß, Klaus U. Schulz:
Solvability of Context Equations with Two Context Variables is Decidable.
67-81
Electronic Edition (Springer LINK) BibTeX
- Tomasz Wierzbicki:
Complexity of the higher order matching.
82-96
Electronic Edition (Springer LINK) BibTeX
- Reinhard Pichler:
Solving Equational Problems Efficiently.
97-111
Electronic Edition (Springer LINK) BibTeX
- A. A. Adams, Hanne Gottliebsen, Steve Linton, Ursula Martin:
VSDITLU: a verifiable symbolic definite integral table look-up.
112-126
Electronic Edition (Springer LINK) BibTeX
- Predrag Janicic, Alan Bundy, Ian Green:
A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers.
127-141
Electronic Edition (Springer LINK) BibTeX
- Helmut Horacek:
Presenting Proofs in a Human-Oriented Way.
142-156
Electronic Edition (Springer LINK) BibTeX
- Viorica Sofronie-Stokkermans:
On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results.
157-171
Electronic Edition (Springer LINK) BibTeX
- Ullrich Hustadt, Renate A. Schmidt:
Maslov's Class K Revisited.
172-186
Electronic Edition (Springer LINK) BibTeX
- Carlos Areces, Hans de Nivelle, Maarten de Rijke:
Prefixed Resolution: A Resolution Method for Modal and Description Logics.
187-201
Electronic Edition (Springer LINK) BibTeX
- Frank Pfenning, Carsten Schürmann:
System Description: Twelf - A Meta-Logical Framework for Deductive Systems.
202-206
Electronic Edition (Springer LINK) BibTeX
- Serge Autexier, Dieter Hutter, Heiko Mantel, Axel Schairer:
System Description: inka 5.0 - A Logic Voyager.
207-211
Electronic Edition (Springer LINK) BibTeX
- Matthias Baaz, Alexander Leitsch, Georg Moser:
System Description: CutRes 0.1: Cut Elimination by Resolution.
212-216
Electronic Edition (Springer LINK) BibTeX
- Andreas Franke, Michael Kohlhase:
System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving.
217-221
Electronic Edition (Springer LINK) BibTeX
- E. Pascal Gribomont, Nachaat Salloum:
System Description: Using OBDD's for the validation of Skolem verification conditions.
222-226
Electronic Edition (Springer LINK) BibTeX
- Jason Hickey:
Fault-Tolerant Distributed Theorem Proving.
227-231
Electronic Edition (Springer LINK) BibTeX
- Thomas Hillenbrand, Andreas Jaeger, Bernd Löchner:
System Description: Waldmeister - Improvements in Performance and Ease of Use.
232-236
Electronic Edition (Springer LINK) BibTeX
- Amy P. Felty, Douglas J. Howe, Abhik Roychoudhury:
Formal Metatheory using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems.
237-251
Electronic Edition (Springer LINK) BibTeX
- Frédéric Prost:
A formalization of Static Analyses in System F.
252-266
Electronic Edition (Springer LINK) BibTeX
- Sergei N. Artëmov:
On Explicit Reflection in Theorem Proving and Formal Verification.
267-281
Electronic Edition (Springer LINK) BibTeX
- Karsten Konrad, David A. Wolfram:
System Description: Kimba, A Model Generator for Many-Valued First-Order Logics.
282-286
Electronic Edition (Springer LINK) BibTeX
- Gopalan Nadathur, Dustin J. Mitchell:
System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of lambda-Prolog.
287-291
Electronic Edition (Springer LINK) BibTeX
- Alexandre Riazanov, Andrei Voronkov:
Vampire.
292-296
Electronic Edition (Springer LINK) BibTeX
- Stephan Schulz:
System Abstract: E 0.3.
297-301
Electronic Edition (Springer LINK) BibTeX
- Robert Nieuwenhuis:
Invited Talk: Rewrite-based Deduction and Symbolic Constraints.
302-313
Electronic Edition (Springer LINK) BibTeX
- Christoph Weidenbach:
Towards an Automatic Analysis of Security Protocols in First-Order Logic.
314-328
Electronic Edition (Springer LINK) BibTeX
- Peter Baumgartner, Norbert Eisinger, Ulrich Furbach:
A Confluent Connection Calculus.
329-343
Electronic Edition (Springer LINK) BibTeX
- Marc Fuchs, Dirk Fuchs:
Abstraction-Based Relevancy Testing for Model Elimination.
344-358
Electronic Edition (Springer LINK) BibTeX
- Matthew Bishop:
A Breadth-First Strategy for Mating Search.
359-373
Electronic Edition (Springer LINK) BibTeX
- Dieter Hutter, Alan Bundy:
The Design of the CADE-16 Inductive Theorem Prover Contest.
374-377
Electronic Edition (Springer LINK) BibTeX
- Christoph Weidenbach:
System Description: Spass Version 1.0.0.
378-382
Electronic Edition (Springer LINK) BibTeX
- Andrei Voronkov:
KK: a theorem prover for K.
383-387
Electronic Edition (Springer LINK) BibTeX
- Jon Whittle, Alan Bundy, Richard J. Boulton, Helen Lowe:
System Description: CyNTHIA.
388-392
Electronic Edition (Springer LINK) BibTeX
- Jian Zhang:
System Description: MCS: Model-based Conjecture Searching.
393-397
Electronic Edition (Springer LINK) BibTeX
- Tobias Nipkow:
Invited Talk: Embedding Programming Languages in Theorem Provers (Abstract).
398
Electronic Edition (Springer LINK) BibTeX
- Christoph Benzmüller:
Extensional Higher-Order Paramodulation and RUE-Resolution.
399-413
Electronic Edition (Springer LINK) BibTeX
- Raul H. C. Lopes:
Automatic Generation of Proof Search Strategies for Second-order Logic.
414-428
Electronic Edition (Springer LINK) BibTeX
Acknowledgement:
the information on this page was provided by Uwe Waldmann
Copyright © Sat May 16 23:00:05 2009
by Michael Ley (ley@uni-trier.de)