Automated Deduction CADE-20 自动化演绎－CADE-20/2005年国际会议录
|
读过这本书吗？
最近在读
读过
想读
还不熟悉
|
图书城书列：
加入到博客或社交网站：
|
|
我来评论这本书：
内容提要：
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 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 …… Author Index |