David A. McAllester
Proceedings of the 17th International Conference on Automated Deduction
CADE, 2000.

@proceedings{CADE-2000,
	address       = "Pittsburgh, Pennsylvania, USA",
	editor        = "David A. McAllester",
	isbn          = "3-540-67664-3",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 17th International Conference on Automated Deduction}",
	volume        = 1831,
	year          = 2000,
}

Contents (44 items)

9 ×#proving
6 ×#logic
6 ×#theorem proving
5 ×#named
4 ×#framework
4 ×#reasoning
4 ×#using
3 ×#automation
3 ×#semantics
3 ×#tutorial

CADE-2000-Harrison #proving #theorem proving #using #verification

High-Level Verification Using Theorem Proving and Formalized Mathematics (JH), pp. 1–6.

CADE-2000-MichaelA #bytecode #higher-order #logic #semantics #syntax

Machine Instruction Syntax and Semantics in Higher Order Logic (NGM, AWA), pp. 7–24.

CADE-2000-NeculaL #generative #proving #theorem proving

Proof Generation in the Touchstone Theorem Prover (GCN, PL), pp. 25–44.

CADE-2000-Slind

Wellfounded Schematic Definitions (KS), pp. 45–63.

CADE-2000-BachmairT #congruence

Abstract Congruence Closure and Specializations (LB, AT), pp. 64–78.

CADE-2000-BarrettDS #framework

A Framework for Cooperating Decision Procedures (CWB, DLD, AS), pp. 79–98.

CADE-2000-Kammuller #composition #reasoning

Modular Reasoning in Isabelle (FK), pp. 99–114.

CADE-2000-Farmer #framework #reasoning

An Infrastructure for Intertheory Reasoning (WMF), pp. 115–131.

CADE-2000-Belinfante #algorithm

Gödel’s Algorithm for Class Formation (JGFB), pp. 132–147.

CADE-2000-BezemHN #automation #proving #type system #using

Automated Proof Construction in Type Theory Using Resolution (MB, DH, HdN), pp. 148–163.

CADE-2000-AndrewsBB #proving #theorem proving #type system

System Description: TPS: A Theorem Proving System for Type Theory (PBA, MB, CEB), pp. 164–169.

CADE-2000-AllenCEKL #logic

The Nuprl Open Logical Environment (SFA, RLC, RE, CK, LL), pp. 170–176.

CADE-2000-Sinz #algebra #automation #proving #theorem proving

System Description: ARA — An Automatic Theorem Prover for Relation Algebras (CS), pp. 177–182.

CADE-2000-Kautz #information management #reasoning #representation #scalability

Scalable Knowledge Representation and Reasoning Systems (HAK), p. 183.

CADE-2000-HasegawaFK #branch #generative #performance #using

Efficient Minimal Model Generation Using Branching Lemmas (RH, HF, MK), pp. 184–199.

CADE-2000-Baumgartner #first-order #named

FDPLL — A First Order Davis-Putnam-Longeman-Loveland Procedure (PB), pp. 200–219.

CADE-2000-TiwariBR #revisited

Rigid E-Unification Revisited (AT, LB, HR), pp. 220–234.

CADE-2000-Seger #float #model checking #proving #theorem proving

Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice (CJHS), p. 235.

CADE-2000-EmersonK #model checking

Reducing Model Checking of the Many to the Few (EAE, VK), pp. 236–254.

CADE-2000-BustanG #simulation

Simulation Based Minimization (DB, OG), pp. 255–270.

CADE-2000-GenetK #encryption #protocol #verification

Rewriting for Cryptographic Protocol Verification (TG, FK), pp. 271–290.

CADE-2000-GiunchigliaT #development #framework #platform

System Description: *SAT: A Platform for the Development of Modal Decision Procedures (EG, AT), pp. 291–296.

CADE-2000-Patel-Schneider

System Description: DLP (PFPS), pp. 297–301.

CADE-2000-AudemardBH #finite

Two Techniques to Improve Finite Model Search (GA, BB, LH), pp. 302–308.

CADE-2000-GieslM

Eliminating Dummy Elimination (JG, AM), pp. 309–323.

CADE-2000-KapurS #induction

Extending Decision Procedures with Induction Schemes (DK, MS), pp. 324–345.

CADE-2000-BorrallerasFR #order #semantics

Complete Monotonic Semantic Path Orderings (CB, MF, AR), pp. 346–364.

CADE-2000-DegtyarevV

Stratified Resolution (AD, AV), pp. 365–384.

CADE-2000-SpencerH #order

Support Ordered Resolution (BS, JDH), pp. 385–400.

CADE-2000-McCuneS

System Description: IVY (WM, OS), pp. 401–405.

CADE-2000-Sutcliffe

System Description: SystemOn TPTP (GS), pp. 406–410.

CADE-2000-BrownS #semantics

System Description: PTTP+GLiDes: Semantically Guided PTTP (MB, GS), pp. 411–416.

CADE-2000-Gillard #calculus #concurrent #formal method

A Formalization of a Concurrent Object Calculus up to alpha-Conversion (GG), pp. 417–432.

CADE-2000-SchmidtH #logic

A Resolution Decision Procedure for Fluted Logic (RAS, UH), pp. 433–448.

CADE-2000-ChatalicS #named

ZRES: The Old Davis-Putman Procedure Meets ZBDD (PC, LS), pp. 449–454.

CADE-2000-FrankeK #knowledge base

System Description: MBASE, an Open Mathematical Knowledge Base (AF, MK), pp. 455–459.

CADE-2000-Meier #proving

System Description: TRAMP: Transformation of Machine-Found Proofs into ND-Proofs at the Assertion Level (AM), pp. 460–464.

CADE-2000-Sofronie-Stokkermans #on the #unification

On Unification for Bonded Distributive Lattices (VSS), pp. 465–481.

CADE-2000-HorrocksST #logic #reasoning

Reasoning with Individuals for the Description Logic SHIQ (IH, US, ST), pp. 482–496.

CADE-2000-CollinsD #verification

System Description: Embedding Verification into Microsoft Excel (GC, LAD), pp. 497–501.

CADE-2000-JacksonL #interactive #proving

System Description: Interactive Proof Critics in XBarnacle (MJ, HL), pp. 502–506.

CADE-2000-Schurmann #framework #logic #named #tutorial

Tutorial: Meta-logical Frameworks (CS), pp. 507–508.

CADE-2000-Pulman #automation #comprehension #deduction #named #natural language #tutorial

Tutorial: Automated Deduction and Natural Language Understanding (SGP), pp. 509–510.

CADE-2000-AndrewsB #education #higher-order #logic #named #proving #theorem proving #tutorial #using

Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic (PBA, CEB), pp. 511–512.