Proceedings of the 16th International Conference on Automated Deduction
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter

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

TEST
DBLP
Scholar
Full names Links ISxN
@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)

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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.