Automated Deduction - CADE-16 : 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings / edited by Harald Ganzinger.

Format:

Book

Contributor:

Ganzinger, H. (Harald), 1950- editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

Lecture notes in computer science. Lecture notes in artificial intelligence ; 1632.

Lecture Notes in Artificial Intelligence ; 1632

Language:

English

Subjects (All):

Artificial intelligence.

Software engineering.

Logic, Symbolic and mathematical.

Computer logic.

Artificial Intelligence.

Software Engineering/Programming and Operating Systems.

Mathematical Logic and Formal Languages.

Logics and Meanings of Programs.

Local Subjects:

Artificial Intelligence.

Software Engineering/Programming and Operating Systems.

Mathematical Logic and Formal Languages.

Logics and Meanings of Programs.

Physical Description:

1 online resource (XIV, 438 pages).

Edition:

First edition 1999.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1999.

System Details:

text file PDF

Contents:

Session 1

A Dynamic Programming Approach to Categorial Deduction

Tractable Transformations from Modal Provability Logics into First-Order Logic

Session 2

Decision Procedures for Guarded Logics

A PSpace Algorithm for Graded Modal Logic

Session 3

Solvability of Context Equations with Two Context Variables Is Decidable

Complexity of the Higher Order Matching

Solving Equational Problems Efficiently

Session 4

VSDITLU: A Verifiable Symbolic Definite Integral Table Look-Up

A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers

Presenting Proofs in a Human-Oriented Way

Session 5

On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results

Maslov's Class K Revisited

Prefixed Resolution: A Resolution Method for Modal and Description Logics

Session 6: System Descriptions

System Description: Twelf - A Meta-Logical Framework for Deductive Systems

System Description: inka 5.0 - A Logic Voyager

System Description: CutRes 0.1: Cut Elimination by Resolution

System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving

System Description Using OBDD's for the Validationof Skolem Verification Conditions

Fault-Tolerant Distributed Theorem Proving

System Description: Waldmeister - Improvements in Performance and Ease of Use

Session 7

Formal Metatheory Using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems

A Formalization of Static Analyses in System F

On Explicit Reflection in Theorem Proving and Formal Verification

Session 8: System Descriptions

System Description: Kimba, A Model Generator for Many-Valued First-Order Logics

System Description: Teyjus-A Compiler and Abstract Machine Based Implementation of ?Prolog

Vampire

System Abstract: E 0.3

Session 9

Invited Talk: Rewrite-Based Deduction and Symbolic Constraints

Towards an Automatic Analysis of Security Protocols in First-Order Logic

Session 10

A Confluent Connection Calculus

Abstraction-Based Relevancy Testing for Model Elimination

A Breadth-First Strategy for Mating Search

Session 11: System Competitions

The Design of the CADE-16 Inductive Theorem Prover Contest

Session 12: System Descriptions

System Description: Spass Version 1.0.0

K : A Theorem Prover for K

System Description: CYNTHIA

System Description: MCS: Model-Based Conjecture Searching

Session 13

Embedding Programming Languages in Theorem Provers

Extensional Higher-Order Paramodulation and RUE-Resolution

Automatic Generation of Proof Search Strategies for Second-Order Logic.

Other Format:

Printed edition:

ISBN:

978-3-540-48660-2

9783540486602

Access Restriction:

Restricted for use by site license.