Automated Deduction - CADE-20: 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings / Edition 1

Automated Deduction - CADE-20: 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings / Edition 1

by Robert Nieuwenhuis
     
 

ISBN-10: 3540280057

ISBN-13: 9783540280057

Pub. Date: 09/01/2005

Publisher: Springer Berlin Heidelberg

This book constitutes the refereed proceedings of the 20th International Conference on Automated Deduction, CADE-20, held in Tallinn, Estonia, in July 2005.

The 25 revised full papers and 5 system descriptions presented were carefully reviewed and selected from 78 submissions. All current aspects of automated deduction are addressed, ranging from theoretical and

Overview

This book constitutes the refereed proceedings of the 20th International Conference on Automated Deduction, CADE-20, held in Tallinn, Estonia, in July 2005.

The 25 revised full papers and 5 system descriptions presented were carefully reviewed and selected from 78 submissions. All current aspects of automated deduction are addressed, ranging from theoretical and methodological issues to presentation and evaluation of theorem provers and logical reasoning systems.

Product Details

ISBN-13:
9783540280057
Publisher:
Springer Berlin Heidelberg
Publication date:
09/01/2005
Series:
Lecture Notes in Computer Science / Lecture Notes in Artificial Intelligence Series, #3632
Edition description:
2005
Pages:
466
Product dimensions:
6.10(w) x 9.25(h) x (d)

Table of Contents

What Do We Know When We Know That a Theory Is Consistent?.- Reflecting Proofs in First-Order Logic with Equality.- Reasoning in Extensional Type Theory with Equality.- Nominal Techniques in Isabelle/HOL.- Tabling for Higher-Order Logic Programming.- A Focusing Inverse Method Theorem Prover for First-Order Linear Logic.- The CoRe Calculus.- Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures.- Privacy-Sensitive Information Flow with JML.- The Decidability of the First-Order Theory of Knuth-Bendix Order.- Well-Nested Context Unification.- Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules.- The OWL Instance Store: System Description.- Temporal Logics over Transitive States.- Deciding Monodic Fragments by Temporal Resolution.- Hierarchic Reasoning in Local Theory Extensions.- Proof Planning for First-Order Temporal Logic.- System Description: Multi A Multi-strategy Proof Planner.- Decision Procedures Customized for Formal Verification.- An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic.- Connecting Many-Sorted Theories.- A Proof-Producing Decision Procedure for Real Arithmetic.- The MathSAT 3 System.- Deduction with XOR Constraints in Security API Modelling.- On the Complexity of Equational Horn Clauses.- A Combination Method for Generating Interpolants.- sKizzo: A Suite to Evaluate and Certify QBFs.- Regular Protocols and Attacks with Regular Knowledge.- The Model Evolution Calculus with Equality.- Model Representation via Contexts and Implicit Generalizations.- Proving Properties of Incremental Merkle Trees.- Computer Search for Counterexamples to Wilkie’s Identity.- KRHyper – In Your Pocket.

Customer Reviews

Average Review:

Write a Review

and post it to your social network

     

Most Helpful Customer Reviews

See all customer reviews >