CADE A

41 papers

YearTitle / Authors
1999A Breadth-First Strategy for Mating Search.
Matthew Bishop
1999A Confluent Connection Calculus.
Peter Baumgartner, Norbert Eisinger, Ulrich Furbach
1999A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers.
Predrag Janicic, Alan Bundy, Ian Green
1999A PSpace Algorithm for Graded Modal Logic.
Stephan Tobies
1999A dynamic programming approach to categorial deduction.
Philippe de Groote
1999A formalization of Static Analyses in System F.
Frédéric Prost
1999Abstraction-Based Relevancy Testing for Model Elimination.
Marc Fuchs, Dirk Fuchs
1999Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings
Harald Ganzinger
1999Automatic Generation of Proof Search Strategies for Second-order Logic.
Raul H. C. Lopes
1999Complexity of the higher order matching.
Tomasz Wierzbicki
1999Extensional Higher-Order Paramodulation and RUE-Resolution.
Christoph Benzmüller
1999Fault-Tolerant Distributed Theorem Proving.
Jason Hickey
1999Formal Metatheory using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems.
Amy P. Felty, Douglas J. Howe, Abhik Roychoudhury
1999Invited Talk: Decision procedures for guarded logics.
Erich Grädel
1999Invited Talk: Embedding Programming Languages in Theorem Provers (Abstract).
Tobias Nipkow
1999Invited Talk: Rewrite-based Deduction and Symbolic Constraints.
Robert Nieuwenhuis
1999KK: a theorem prover for K.
Andrei Voronkov
1999Maslov's Class K Revisited.
Ullrich Hustadt, Renate A. Schmidt
1999On Explicit Reflection in Theorem Proving and Formal Verification.
Sergei N. Artëmov
1999On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results.
Viorica Sofronie-Stokkermans
1999Prefixed Resolution: A Resolution Method for Modal and Description Logics.
Carlos Areces, Hans de Nivelle, Maarten de Rijke
1999Presenting Proofs in a Human-Oriented Way.
Helmut Horacek
1999Solvability of Context Equations with Two Context Variables is Decidable.
Manfred Schmidt-Schauß, Klaus U. Schulz
1999Solving Equational Problems Efficiently.
Reinhard Pichler
1999System Abstract: E 0.3.
Stephan Schulz
1999System Description: CutRes 0.1: Cut Elimination by Resolution.
Matthias Baaz, Alexander Leitsch, Georg Moser
1999System Description: CyNTHIA.
Jon Whittle, Alan Bundy, Richard J. Boulton, Helen Lowe
1999System Description: Kimba, A Model Generator for Many-Valued First-Order Logics.
Karsten Konrad, David A. Wolfram
1999System Description: MCS: Model-based Conjecture Searching.
Jian Zhang
1999System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving.
Andreas Franke, Michael Kohlhase
1999System Description: Spass Version 1.0.0.
Christoph Weidenbach
1999System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of lambda-Prolog.
Gopalan Nadathur, Dustin J. Mitchell
1999System Description: Twelf - A Meta-Logical Framework for Deductive Systems.
Frank Pfenning, Carsten Schürmann
1999System Description: Using OBDD's for the validation of Skolem verification conditions.
E. Pascal Gribomont, Nachaat Salloum
1999System Description: Waldmeister - Improvements in Performance and Ease of Use.
Thomas Hillenbrand, Andreas Jaeger, Bernd Löchner
1999System Description: inka 5.0 - A Logic Voyager.
Serge Autexier, Dieter Hutter, Heiko Mantel, Axel Schairer
1999The Design of the CADE-16 Inductive Theorem Prover Contest.
Dieter Hutter, Alan Bundy
1999Towards an Automatic Analysis of Security Protocols in First-Order Logic.
Christoph Weidenbach
1999Tractable Transformations from Modal Provability Logics into First-Order Logic.
Stéphane Demri, Rajeev Goré
1999VSDITLU: a verifiable symbolic definite integral table look-up.
Andrew A. Adams, Hanne Gottliebsen, Steve Linton, Ursula Martin
1999Vampire.
Alexandre Riazanov, Andrei Voronkov