


default search action
16th CADE 1999: Trento, Italy
- Harald Ganzinger:

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 - 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 - Andrew 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 - Ullrich Hustadt

, Renate A. Schmidt
:
Maslov's Class K Revisited. 172-186 - 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 - Alexandre Riazanov, Andrei Voronkov:

Vampire. 292-296 - 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 - Peter Baumgartner, Norbert Eisinger, Ulrich Furbach:

A Confluent Connection Calculus. 329-343 - Marc Fuchs, Dirk Fuchs:

Abstraction-Based Relevancy Testing for Model Elimination. 344-358 - Matthew Bishop:

A Breadth-First Strategy for Mating Search. 359-373 - Dieter Hutter

, Alan Bundy:
The Design of the CADE-16 Inductive Theorem Prover Contest. 374-377 - Christoph Weidenbach:

System Description: Spass Version 1.0.0. 378-382 - Andrei Voronkov:

KK: a theorem prover for K. 383-387 - Jon Whittle, Alan Bundy, Richard J. Boulton, Helen Lowe:

System Description: CyNTHIA. 388-392 - 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

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














