Termination of narrowing revisited

DOI10.1016/j.tcs.2009.07.037zbMath1187.68271OpenAlexW2000232009WikidataQ57978189 ScholiaQ57978189MaRDI QIDQ1035697

Santiago Escobar, María Alpuente, José Iborra

Publication date: 4 November 2009

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2009.07.037

zbMATH Keywords

terminationnarrowingreachability problemsequational unification

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (10)

Symbolic Specialization of Rewriting Logic Theories with Presto ⋮ Optimizing Maude programs via program specialization ⋮ Modular Termination of Basic Narrowing ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A compact fixpoint semantics for term rewriting systems ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ Constant runtime complexity of term rewriting is semi-decidable ⋮ Termination of Narrowing Using Dependency Pairs ⋮ A Non-Deterministic Multiset Query Language

Uses Software

• Haskell
• Maude

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties
• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Termination of rewriting
• Counterexamples to termination for the direct sum of term rewriting systems
• Unification theory
• Syntacticness, cycle-syntacticness and shallow theories
• Completeness results for basic narrowing
• Incremental constraint satisfaction for equational logic programming
• Foundations of equational logic programming
• Termination of term rewriting using dependency pairs
• Declarative Debugging of Functional Logic Programs1 1This work has been partially supported by CICYT under grant TIC2001-2705-C03-01, by Accóon Integrada Hispano-Italiana HI2000-0161 and by Generalitat Valenciana under grant GV01-424.
• Modular termination of basic narrowing and equational unification
• Abstract Diagnosis of Functional Programs
• The integration of functions into logic programming: From theory to practice
• Analyses of unsatisfiability for equational logic programming
• Narrowing directed by a graph of terms
• On modularity in term rewriting and narrowing
• Foundations of Software Science and Computation Structures
• Symbolic Model Checking of Infinite-State Systems Using Narrowing

This page was built for publication: Termination of narrowing revisited