This book constitutes the refereed proceedings of the 16th International Conference on Automated Deduction, CADE-16, held in Trento, Italy in July 1999 as part of FLoC'99. The 21 revised full papers presented were carefully reviewed and selected from a total of 83 submissions. Also included are 15 system descriptions and two invited full papers. The book addresses all current issues in automated deduction and theorem proving, ranging from logical foundations to deduction systems design and evaluation
Author(s): Harald Ganzinger (auth.)
Series: Lecture Notes in Computer Science 1632 : Lecture Notes in Artificial Intelligence
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1999
Language: English
Pages: 438
Tags: Artificial Intelligence (incl. Robotics); Mathematical Logic and Formal Languages; Logics and Meanings of Programs
A Dynamic Programming Approach to Categorial Deduction....Pages 1-15
Tractable Transformations from Modal Provability Logics into First-Order Logic....Pages 16-30
Decision Procedures for Guarded Logics....Pages 31-51
A PSpace Algorithm for Graded Modal Logic....Pages 52-66
Solvability of Context Equations with Two Context Variables Is Decidable....Pages 67-81
Complexity of the Higher Order Matching....Pages 82-96
Solving Equational Problems Efficiently....Pages 97-111
VSDITLU: A Verifiable Symbolic Definite Integral Table Look-Up....Pages 112-126
A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers....Pages 127-141
Presenting Proofs in a Human-Oriented Way....Pages 142-156
On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results....Pages 157-171
Maslov’s Class K Revisited....Pages 172-186
Prefixed Resolution: A Resolution Method for Modal and Description Logics....Pages 187-201
System Description: Twelf — A Meta-Logical Framework for Deductive Systems....Pages 202-206
System Description: inka 5.0 - A Logic Voyager....Pages 207-211
System Description: CutRes 0.1: Cut Elimination by Resolution....Pages 212-216
System Description: MathWeb , an Agent-Based Communication Layer for Distributed Automated Theorem Proving....Pages 217-221
System Description Using OBDD’s for the Validationof Skolem Verification Conditions....Pages 222-226
Fault-Tolerant Distributed Theorem Proving....Pages 227-231
System Description: Waldmeister — Improvements in Performance and Ease of Use....Pages 232-236
Formal Metatheory Using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems....Pages 237-251
A Formalization of Static Analyses in System F ....Pages 252-266
On Explicit Reflection in Theorem Proving and Formal Verification....Pages 267-281
System Description: Kimba, A Model Generator for Many-Valued First-Order Logics....Pages 282-286
System Description: Teyjus—A Compiler and Abstract Machine Based Implementation of λProlog....Pages 287-291
Vampire....Pages 292-296
System Abstract: E 0.3....Pages 297-301
Invited Talk: Rewrite-Based Deduction and Symbolic Constraints....Pages 302-313
Towards an Automatic Analysis of Security Protocols in First-Order Logic....Pages 314-328
A Confluent Connection Calculus....Pages 329-343
Abstraction-Based Relevancy Testing for Model Elimination....Pages 344-358
A Breadth-First Strategy for Mating Search....Pages 359-373
The Design of the CADE-16 Inductive Theorem Prover Contest....Pages 374-377
System Description: Spass Version 1.0.0....Pages 378-382
K : A Theorem Prover for K....Pages 383-387
System Description: CYNTHIA ....Pages 388-392
System Description: MCS: Model-Based Conjecture Searching....Pages 393-397
Embedding Programming Languages in Theorem Provers....Pages 398-398
Extensional Higher-Order Paramodulation and RUE-Resolution....Pages 399-413
Automatic Generation of Proof Search Strategies for Second-Order Logic....Pages 414-428
