Automated Deduction CADE-20 自動化演繹－CADE-20/2005年國際會議錄

內(nèi)容概要

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.

書籍目錄

What Do We Know When We Know That a Theory Is Consistent?Reflecting Proofs in First-Order Logic with EqualityReasoning in Extensional Type Theory with EqualityNominal Techniques in Isabelle/HOLTabling for Higher-Order Logic ProgrammingA Focusing Inverse Method Theorem Prover for First-Order Linear LogicThe CoRE CalculusSimulating Reachability Using First-Order Logic with Applications to Verification of Linked Data StructuresPrivacy-Sensitive Information Flow with JMLThe Decidability of the First-Order Theory of Knuth-Bendix OrderWell-Nested Context UnificationTermination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground RulesThe OWL Instance Store: System DescriptionTemporal Logics over Transitive StatesDeciding Monodic Fragments by Temporal ResolutionHierarchic Reasoning in Local Theory ExtensionsProof Planning for First-Order Temporal LogicSystem Description: MULTI A Multi-strategy Proof PlannerDecision Procedures Customized for Formal VerificationAn Algorithm for Deciding BAPA: Boolean Algebra with Presburger ArithmeticConnecting Many-Sorted TheoriesA Proof-Producing Decision Procedure for Real ArithmeticThe MathSAT 3 SystemDeduction with XOR Constraints in Security API ModellingOn the Complexity of Equational Horn ClausesA Combination Method for Generating InterpolantssKizzo: A Suite to Evaluate and Certify QBFs……Author Index

圖書封面

評論、評分、閱讀與下載

---

    Automated Deduction CADE-20 自動化演繹－CADE-20/2005年國際會議錄 PDF格式下載

---