Automated Deduction - Cade-20: 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings

Robert Nieuwenhuis

ISBN 10: 3540280057 / ISBN 13: 9783540280057

Editore: Springer Verlag, 2005

Riguardo questo articolo

1st edition. 472 pages. 9.25x6.25x1.00 inches. In Stock.

Codice articolo x-3540280057

Dati bibliografici

• Titolo: Automated Deduction - Cade-20: 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings
• Editore: Springer Verlag
• Data di pubblicazione: 2005
• Lingua: Inglese
• ISBN 10: 3540280057
• ISBN 13: 9783540280057
• Rilegatura: Paperback
• Condizione: Brand New
• Peso: 0,66 chilogrammi

Descrizione articolo

Riassunto

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.

Contenuti

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.