Automated Deduction - CADE-20: 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedin by Robert NieuwenhuisAutomated Deduction - CADE-20: 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedin by Robert Nieuwenhuis

Automated Deduction - CADE-20: 20th International Conference on Automated Deduction, Tallinn…

byRobert Nieuwenhuis

Paperback | July 14, 2005

Pricing and Purchase Info

$148.02 online 
$178.50 list price save 17%
Earn 740 plum® points

Prices and offers may vary in store

Quantity:

In stock online

Ships free on orders over $25

Not available in stores

about

authors. The merits of the submissions were d- cussed by the programcommittee for ten days through the Internet by means of the EasyChair system. Finally, the program committee selected for publication 25 regular research papers and 5 system descriptions.
Title:Automated Deduction - CADE-20: 20th International Conference on Automated Deduction, Tallinn…Format:PaperbackDimensions:466 pages, 23.5 × 15.5 × 0.07 inPublished:July 14, 2005Publisher:Springer-Verlag/Sci-Tech/TradeLanguage:English

The following ISBNs are associated with this title:

ISBN - 10:3540280057

ISBN - 13:9783540280057

Look for similar items by category:

Reviews

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.