04669nam 22007095 450 99646559160331620230406060557.03-540-36835-310.1007/11805618(CKB)1000000000233062(SSID)ssj0000320335(PQKBManifestationID)11238877(PQKBTitleCode)TC0000320335(PQKBWorkID)10348333(PQKB)10632372(DE-He213)978-3-540-36835-9(MiAaPQ)EBC3068187(PPN)123137039(EXLCZ)99100000000023306220100301d2006 u| 0engurnn|008mamaatxtccrTerm Rewriting and Applications[electronic resource] 17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings /edited by Frank Pfenning1st ed. 2006.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,2006.1 online resource (XIV, 418 p.) Theoretical Computer Science and General Issues,2512-2029 ;4098Bibliographic Level Mode of Issuance: Monograph3-540-36834-5 Includes bibliographical references and index.FLoC Plenary Talk -- Formal Verification of Infinite State Systems Using Boolean Methods -- Session 1. Constraints and Optimization -- Solving Partial Order Constraints for LPO Termination -- Computationally Equivalent Elimination of Conditions -- On the Correctness of Bubbling -- Propositional Tree Automata -- Session 2. Equational Reasoning -- Generalizing Newman’s Lemma for Left-Linear Rewrite Systems -- Unions of Equational Monadic Theories -- Modular Church-Rosser Modulo -- Session 3. System Verification -- Hierarchical Combination of Intruder Theories -- Feasible Trace Reconstruction for Rewriting Approximations -- Invited Talk -- Rewriting Models of Boolean Programs -- Session 4. Lambda Calculus -- Syntactic Descriptions: A Type System for Solving Matching Equations in the Linear ?-Calculus -- A Terminating and Confluent Linear Lambda Calculus -- A Lambda-Calculus with Constructors -- Structural Proof Theory as Rewriting -- Session 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 Induction -- Session 6. System Descriptions -- TPA: Termination Proved Automatically -- RAPT: A Program Transformation System Based on Term Rewriting -- The CL-Atse Protocol Analyser -- Slothrop: Knuth-Bendix Completion with a Modern Termination Checker -- Invited Talk -- Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages -- Session 7. Termination -- Predictive Labeling -- Termination of String Rewriting with Matrix Interpretations -- Decidability of Termination for Semi-constructor TRSs, Left-Linear Shallow TRSs and Related Systems -- Proving Positive Almost Sure Termination Under Strategies -- Session 8. Higher-Order Rewriting and Unification -- A Proof of Finite Family Developments for Higher-Order Rewriting Using a Prefix Property -- Higher-Order Orderings for Normal Rewriting -- Bounded Second-Order Unification Is NP-Complete.Theoretical Computer Science and General Issues,2512-2029 ;4098Compilers (Computer programs)Machine theoryComputer scienceArtificial intelligenceComputer science—MathematicsCompilers and InterpretersFormal Languages and Automata TheoryComputer Science Logic and Foundations of ProgrammingArtificial IntelligenceSymbolic and Algebraic ManipulationCompilers (Computer programs).Machine theory.Computer science.Artificial intelligence.Computer science—Mathematics.Compilers and Interpreters.Formal Languages and Automata Theory.Computer Science Logic and Foundations of Programming.Artificial Intelligence.Symbolic and Algebraic Manipulation.005.131Pfenning Frankedthttp://id.loc.gov/vocabulary/relators/edtInternational Conference on Rewriting Techniques and ApplicationsBOOK996465591603316Term Rewriting and Applications772114UNISA