项重写与应用

出版时间：2006-12  出版社：湖北辞书出版社  作者：Pfenning, Frank  页数：414  

内容概要

This book constitutes the refereed proceedings of the 17th International Conference on Rewriting Techniques and Applications, RTA 2006, held in Seattle, WA, USA in August 2006 within the scope of FLoC 2006, the 2006 Federated Logic Conference.    The 23 revised full papers and 4 systems description papers carefully reviewed and selected from 52 initial submissions are presented together with 2 invited talks and a plenary talk of the hosting FLoC conference. The papers are organized in topical sections on constraints and optimization, equational reasoning, system verification, lambda calculus, theorem proving, system descriptions, termination, and higher-order rewriting and unification.

书籍目录

FLoC Plenary Talk  Formal Verification of Infinite State Systems Using Boolean MethodsSession 1. Constraints and Optimization  Solving Partial Order Constraints for LPO Termination  Computationally Equivalent Elimination of Conditions  On the Correctness of Bubbling  Propositional Tree AutomataSession 2. Equational Reasoning  Generalizing Newman's Lemma for Left-Linear Rewrite Systems  Unions of Equational Monadic Theories  Modular Church-Rosser ModuloSession 3. System Verification  Hierarchical Combination of Intruder Theories  Feasible Trace Reconstruction for Rewriting ApproximationsInvited Talk  Javier Esparza Rewriting Models of Boolean ProgramsSession 4. Lambda Calculus  Syntactic Descriptions: A Type System for Solving Matching Equations in the Linear A-Calculus  A Terminating and Confluent Linear Lambda Calculus  A Lambda-Calculus with Constructors  Structural Proof Theory as RewritingSession 5. Theorem Proving  Checking Conservativity of Overloaded Definitions in Higher-Order Logic  Certified Higher-Order Recursive Path Ordering  Dealing with Non-orientable Equations in Rewriting InductionSession 6. System Descriptions  TPA: Termination Proved Automatically  RAPT: A Program Transformation System Based on Term Rewriting  The CL-Atse Protocol Analyser  ……Invited TalkSeesion 7. TerminationSeesion 8. Higher-Order Rewriting and UnificationAuthor Index