Automated Deduction CADE-20 自动化演绎－CADE-20/2005年国际会议录

书籍目录

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

作者简介

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.

 Automated Deduction CADE-20 自动化演绎－CADE-20/2005年国际会议录下载