Automated Deduction â CADE-20: 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings (Lecture Notes in Computer Science, 3632)

Nieuwenhuis, Robert

ISBN 10: 3540280057 / ISBN 13: 9783540280057

Editore: Springer (edition 2005), 2005

Riguardo questo articolo

It's a preowned item in good condition and includes all the pages. It may have some general signs of wear and tear, such as markings, highlighting, slight damage to the cover, minimal wear to the binding, etc., but they will not affect the overall reading experience.

Codice articolo 3540280057-11-1

Dati bibliografici

• Titolo: Automated Deduction â CADE-20: 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings (Lecture Notes in Computer Science, 3632)
• Editore: Springer (edition 2005)
• Data di pubblicazione: 2005
• Lingua: Inglese
• ISBN 10: 3540280057
• ISBN 13: 9783540280057
• Rilegatura: Paperback
• Edizione: 2005.
• Condizione: Good

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.