Harald Ganzinger
Proceedings of the 16th International Conference on Automated Deduction
CADE, 1999.

@proceedings{CADE-1999,
	address       = "Trento, Italy",
	editor        = "Harald Ganzinger",
	isbn          = "3-540-66222-7",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 16th International Conference on Automated Deduction}",
	volume        = 1632,
	year          = 1999,
}

Contents (40 items)

9 ×#logic
9 ×#proving
7 ×#theorem proving
3 ×#automation
3 ×#deduction
3 ×#first-order
3 ×#higher-order
2 ×#analysis
2 ×#complexity
2 ×#decidability

CADE-1999-Groote #approach #deduction #programming

A dynamic programming approach to categorial deduction (PdG), pp. 1–15.

CADE-1999-DemriG #first-order #logic

Tractable Transformations from Modal Provability Logics into First-Order Logic (SD, RG), pp. 16–30.

CADE-1999-Gradel #logic

Invited Talk: Decision procedures for guarded logics (EG), pp. 31–51.

CADE-1999-Tobies #algorithm #logic

A PSpace Algorithm for Graded Modal Logic (ST), pp. 52–66.

CADE-1999-Schmidt-SchaussS #decidability #equation

Solvability of Context Equations with Two Context Variables is Decidable (MSS, KUS), pp. 67–81.

CADE-1999-Wierzbicki #complexity #higher-order

Complexity of the higher order matching (TW), pp. 82–96.

CADE-1999-Pichler #equation #problem

Solving Equational Problems Efficiently (RP), pp. 97–111.

CADE-1999-AdamsGLM #named

VSDITLU: a verifiable symbolic definite integral table look-up (AAA, HG, SL, UM), pp. 112–126.

CADE-1999-JanicicBG #flexibility #framework #integration #proving #theorem proving

A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers (PJ, AB, IG), pp. 127–141.

CADE-1999-Horacek #proving

Presenting Proofs in a Human-Oriented Way (HH), pp. 142–156.

CADE-1999-Sofronie-Stokkermans #complexity #decidability #on the

On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results (VSS), pp. 157–171.

CADE-1999-HustadtS #revisited

Maslov’s Class K Revisited (UH, RAS), pp. 172–186.

CADE-1999-ArecesNR #logic

Prefixed Resolution: A Resolution Method for Modal and Description Logics (CA, HdN, MdR), pp. 187–201.

CADE-1999-PfenningS #deduction #framework #logic

System Description: Twelf — A Meta-Logical Framework for Deductive Systems (FP, CS), pp. 202–206.

CADE-1999-AutexierHMS #logic

System Description: inka 5.0 — A Logic Voyager (SA, DH, HM, AS), pp. 207–211.

CADE-1999-BaazLM

System Description: CutRes 0.1: Cut Elimination by Resolution (MB, AL, GM), pp. 212–216.

CADE-1999-FrankeK #automation #communication #distributed #proving #theorem proving

System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving (AF, MK), pp. 217–221.

CADE-1999-GribomontS #using #validation #verification

System Description: Using OBDD’s for the validation of Skolem verification conditions (EPG, NS), pp. 222–226.

CADE-1999-Hickey #distributed #fault tolerance #proving #theorem proving

Fault-Tolerant Distributed Theorem Proving (JH), pp. 227–231.

CADE-1999-HillenbrandJL #performance

System Description: Waldmeister — Improvements in Performance and Ease of Use (TH, AJ, BL), pp. 232–236.

CADE-1999-FeltyHR #abstraction #syntax #using

Formal Metatheory using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems (APF, DJH, AR), pp. 237–251.

CADE-1999-Prost #analysis #formal method #system f

A formalization of Static Analyses in System F (FP), pp. 252–266.

CADE-1999-Artemov #on the #proving #theorem proving #verification

On Explicit Reflection in Theorem Proving and Formal Verification (SNA), pp. 267–281.

CADE-1999-KonradW #first-order #generative #logic

System Description: Kimba, A Model Generator for Many-Valued First-Order Logics (KK, DAW), pp. 282–286.

CADE-1999-NadathurM #automaton #compilation #implementation #prolog #λ-calculus

System Description: Teyjus — A Compiler and Abstract Machine Based Implementation of lambda-Prolog (GN, DJM), pp. 287–291.

CADE-1999-RiazanovV

Vampire (AR, AV), pp. 292–296.

CADE-1999-Schulz

System Abstract: E 0.3 (SS), pp. 297–301.

CADE-1999-Nieuwenhuis #constraints #deduction

Invited Talk: Rewrite-based Deduction and Symbolic Constraints (RN), pp. 302–313.

CADE-1999-Weidenbach #analysis #automation #first-order #logic #protocol #security #towards

Towards an Automatic Analysis of Security Protocols in First-Order Logic (CW), pp. 314–328.

CADE-1999-BaumgartnerEF #calculus #confluence

A Confluent Connection Calculus (PB, NE, UF), pp. 329–343.

CADE-1999-FuchsF #testing

Abstraction-Based Relevancy Testing for Model Elimination (MF, DF), pp. 344–358.

CADE-1999-Bishop

A Breadth-First Strategy for Mating Search (MB), pp. 359–373.

CADE-1999-HutterB #contest #design #induction #proving #theorem proving

The Design of the CADE-16 Inductive Theorem Prover Contest (DH, AB), pp. 374–377.

CADE-1999-Weidenbach99a

System Description: Spass Version 1.0.0 (CW), pp. 378–382.

CADE-1999-Voronkov #named #proving #theorem proving

KK: a theorem prover for K (AV), pp. 383–387.

CADE-1999-WhittleBBL

System Description: CyNTHIA (JW, AB, RJB, HL), pp. 388–392.

CADE-1999-ZhangJ #modelling

System Description: MCS: Model-based Conjecture Searching (JZ0), pp. 393–397.

CADE-1999-Nipkow #programming language #proving #theorem proving

Invited Talk: Embedding Programming Languages in Theorem Provers (TN), p. 398.

CADE-1999-Benzmuller #higher-order

Extensional Higher-Order Paramodulation and RUE-Resolution (CB), pp. 399–413.

CADE-1999-Lopes #automation #generative #higher-order #logic #proving

Automatic Generation of Proof Search Strategies for Second-order Logic (RHCL), pp. 414–428.