LEADER 05061nam 2200625 450 001 996466085803316 005 20220113145520.0 010 $a3-662-21551-9 024 7 $a10.1007/978-3-662-21551-7 035 $a(CKB)1000000000233978 035 $a(SSID)ssj0000326347 035 $a(PQKBManifestationID)11268655 035 $a(PQKBTitleCode)TC0000326347 035 $a(PQKBWorkID)10265663 035 $a(PQKB)10727523 035 $a(DE-He213)978-3-662-21551-7 035 $a(MiAaPQ)EBC6593074 035 $a(Au-PeEL)EBL6593074 035 $a(OCoLC)1250084194 035 $a(EXLCZ)991000000000233978 100 $a20220113d1993 uy 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 00$aRewriting techniques and applications $e5th international conference, RTA-93, Montreal, Canada, June 16-18, 1993 : proceedings /$fClaude Kirchner, editor 205 $a1st ed. 1993. 210 1$aBerlin, Germany ;$aNew York, New York :$cSpringer-Verlag,$d[1993] 210 4$d©1993 215 $a1 online resource (XI, 492 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v690 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-56868-9 320 $aIncludes bibliographical references and index. 327 $aRewrite techniques in theorem proving -- Redundancy criteria for constrained completion -- Bi-rewriting, a term rewriting technique for monotonic order relations -- A case study of completion modulo distributivity and Abelian groups -- A semantic approach to order-sorted rewriting -- Distributing equational theorem proving -- On the correctness of a distributed memory Gröbner basis algorithm -- Improving transformation systems for general E-unification -- Equational and membership constraints for infinite trees -- Regular path expressions in feature logic -- Proving properties of typed lambda terms: Realizability, covers, and sheaves -- Some lambda calculi with categorical sums and products -- Paths, computations and labels in the ?-calculus -- Confluence and superdevelopments -- Relating graph and term rewriting via Böhm models -- Topics in termination -- Total termination of term rewriting -- Simple termination is difficult -- Optimal normalization in orthogonal term rewriting systems -- A graph reduction approach to incremental term rewriting -- Generating tables for bottom-up matching -- On some algorithmic problems for groups and monoids -- Combination techniques and decision problems for disunification -- The negation elimination from syntactic equational formula is decidable -- Encompassment properties and automata with constraints -- Recursively defined tree transductions -- AC complement problems: Satisfiability and negation elimination -- A precedence-based total AC-compatible ordering -- Extension of the associative path ordering to a chain of associative commutative symbols -- Polynomial time termination and constraint satisfaction tests -- Linear interpretations by counting patterns -- Some undecidable termination problems for semi-Thue systems -- Saturation of first-order (constrained) clauses with the Saturate system -- MERILL: An equational reasoning system in standard ML -- Reduce the redex ? ReDuX -- Agg ? An implementation of algebraic graph rewriting -- Smaran: A congruence-closure based system for equational computations -- LAMBDALG: Higher order algebraic specification language -- More problems in rewriting. 330 $aThis volume contains the proceedings of RTA-93, the fifth International Conference on Rewriting Techniques and Applications, held in Montreal, Canada, in June 1993. The volume includes three invited lectures, "Rewrite techniques in theorem proving" (L. Bachmair), "Proving properties of typed lambda terms: realizability, covers, and sheaves" (J. Gallier), and "On some algorithmic problems for groups and monoids" (S.J. Adian), together with 29 selected papers, 6 system descriptions, and a list of open problems in the field. The papers covermany topics: term rewriting; termination; graph rewriting; constraint solving; semantic unification, disunification and combination; higher-order logics; and theorem proving, with several papers on distributed theorem proving, theorem proving with constraints and completion. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v690 606 $aRewriting systems (Computer science)$vCongresses 606 $aComputer programming$vCongresses 606 $aAlgorithms$vCongresses 608 $aElectronic books. 615 0$aRewriting systems (Computer science) 615 0$aComputer programming 615 0$aAlgorithms 676 $a005.13/1 702 $aKirchner$b Claude 712 12$aInternational Conference on Rewriting Techniques and Applications 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996466085803316 996 $aRewriting Techniques and Applications$9774195 997 $aUNISA