16. CADE 1999: Trento, Italy

@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