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. Springer 1999 Lecture Notes in Computer Science ISBN 3-540-66222-7- Philippe de Groote: A dynamic programming approach to categorial deduction. 1-15
- Stéphane Demri, Rajeev Goré: Tractable Transformations from Modal Provability Logics into First-Order Logic. 16-30
- Erich Grädel: Invited Talk: Decision procedures for guarded logics. 31-51
- Stephan Tobies: A PSpace Algorithm for Graded Modal Logic. 52-66
- Manfred Schmidt-Schauß, Klaus U. Schulz: Solvability of Context Equations with Two Context Variables is Decidable. 67-81
- Tomasz Wierzbicki: Complexity of the higher order matching. 82-96
- Reinhard Pichler: Solving Equational Problems Efficiently. 97-111
- A. A. Adams, Hanne Gottliebsen, Steve Linton, Ursula Martin: VSDITLU: a verifiable symbolic definite integral table look-up. 112-126
- Predrag Janicic, Alan Bundy, Ian Green: A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers. 127-141
- Helmut Horacek: Presenting Proofs in a Human-Oriented Way. 142-156
- Viorica Sofronie-Stokkermans: On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results. 157-171
- Carlos Areces, Hans de Nivelle, Maarten de Rijke: Prefixed Resolution: A Resolution Method for Modal and Description Logics. 187-201
- Frank Pfenning, Carsten Schürmann: System Description: Twelf - A Meta-Logical Framework for Deductive Systems. 202-206
- Serge Autexier, Dieter Hutter, Heiko Mantel, Axel Schairer: System Description: inka 5.0 - A Logic Voyager. 207-211
- Matthias Baaz, Alexander Leitsch, Georg Moser: System Description: CutRes 0.1: Cut Elimination by Resolution. 212-216
- Andreas Franke, Michael Kohlhase: System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving. 217-221
- E. Pascal Gribomont, Nachaat Salloum: System Description: Using OBDD's for the validation of Skolem verification conditions. 222-226
- Jason Hickey: Fault-Tolerant Distributed Theorem Proving. 227-231
- Thomas Hillenbrand, Andreas Jaeger, Bernd Löchner: System Description: Waldmeister - Improvements in Performance and Ease of Use. 232-236
- Amy P. Felty, Douglas J. Howe, Abhik Roychoudhury: Formal Metatheory using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems. 237-251
- Frédéric Prost: A formalization of Static Analyses in System F. 252-266
- Sergei N. Artëmov: On Explicit Reflection in Theorem Proving and Formal Verification. 267-281
- Karsten Konrad, David A. Wolfram: System Description: Kimba, A Model Generator for Many-Valued First-Order Logics. 282-286
- Gopalan Nadathur, Dustin J. Mitchell: System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of lambda-Prolog. 287-291
- Stephan Schulz: System Abstract: E 0.3. 297-301
- Robert Nieuwenhuis: Invited Talk: Rewrite-based Deduction and Symbolic Constraints. 302-313
- Christoph Weidenbach: Towards an Automatic Analysis of Security Protocols in First-Order Logic. 314-328
- Matthew Bishop: A Breadth-First Strategy for Mating Search. 359-373
- Christoph Weidenbach: System Description: Spass Version 1.0.0. 378-382
- Andrei Voronkov: KK: a theorem prover for K. 383-387
- Jian Zhang: System Description: MCS: Model-based Conjecture Searching. 393-397
- Tobias Nipkow: Invited Talk: Embedding Programming Languages in Theorem Provers (Abstract). 398
- Christoph Benzmüller: Extensional Higher-Order Paramodulation and RUE-Resolution. 399-413
- Raul H. C. Lopes: Automatic Generation of Proof Search Strategies for Second-order Logic. 414-428
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-17T203403 by the dblp team