Conditional narrowing modulo a set of equations
From MaRDI portal
Narrowing is a universal unification procedure for equational theories given by a canonical term rewrite system. We introduce conditional narrowing modulo a set of conditional equations and give a full proof of its correctness and completeness for equational conditional rewrite systems \(R\), \(E\) without extravariables where \(E\) is regular and \(R\), \(E\) is Church-Rosser modulo \(E\) and decreasing modulo \(E\). This result can be seen as the theoretical foundation of a special form of constraint logic and functional programming.
Recommendations
Cites work
- A rationale for conditional equational programming
- Associative-commutative reduction orderings
- Complete Sets of Reductions for Some Equational Theories
- Completeness results for basic narrowing
- Completion of a Set of Rules Modulo a Set of Equations
- Conditional rewrite rules
- Foundations of equational logic programming
- scientific article; zbMATH DE number 3870640 (Why is no real title available?)
- scientific article; zbMATH DE number 4164122 (Why is no real title available?)
- scientific article; zbMATH DE number 3817070 (Why is no real title available?)
- scientific article; zbMATH DE number 3921957 (Why is no real title available?)
- scientific article; zbMATH DE number 3930372 (Why is no real title available?)
- scientific article; zbMATH DE number 3938563 (Why is no real title available?)
- scientific article; zbMATH DE number 3945331 (Why is no real title available?)
- scientific article; zbMATH DE number 3990847 (Why is no real title available?)
- scientific article; zbMATH DE number 4047068 (Why is no real title available?)
- scientific article; zbMATH DE number 4053008 (Why is no real title available?)
- scientific article; zbMATH DE number 4053061 (Why is no real title available?)
- scientific article; zbMATH DE number 3688776 (Why is no real title available?)
- scientific article; zbMATH DE number 3702108 (Why is no real title available?)
- scientific article; zbMATH DE number 18651 (Why is no real title available?)
- scientific article; zbMATH DE number 193539 (Why is no real title available?)
- scientific article; zbMATH DE number 4113971 (Why is no real title available?)
- Proving termination with multiset orderings
- Simplifying conditional term rewriting systems: Unification, termination and confluence
- Termination of rewriting systems by polynomial interpretations and its implementation
- Termination orderings for associative-commutative rewriting systems
Cited in
(12)- Sentence-normalized conditional narrowing modulo in rewriting logic and Maude
- Narrowing and rewriting logic: from foundations to applications
- Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude
- scientific article; zbMATH DE number 3930372 (Why is no real title available?)
- An implementation of narrowing
- On narrowing, refutation proofs and constraints
- Higher order conditional rewriting and narrowing
- Variant narrowing and equational unification
- Strategies in conditional narrowing modulo SMT plus axioms
- Strict coherence of conditional rewriting modulo axioms
- Complete symbolic reachability analysis using back-and-forth narrowing
- Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
This page was built for publication: Conditional narrowing modulo a set of equations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1261194)
