Basic narrowing revisited

DOI10.1016/S0747-7171(89)80014-8zbMath0682.68094MaRDI QIDQ1824412

Pierre Réty, Gert Smolka, Werner Nutt

Publication date: 1989

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

rewriting systemnarrowinginitial algebraequation solvingrewriting ruleFailure rulesResolution rulessafe blocking ruleSimplification rulesunfolding rule

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Abstract data types; algebraic specification (68Q65) Thue and Post systems, etc. (03D03)

Related Items

A new approach to general E-unification based on conditional rewriting systems ⋮ An optimal narrowing strategy for general canonical systems ⋮ Completeness results for basic narrowing ⋮ Proving ground confluence and inductive validity in constructor based equational specifications ⋮ A Finite Representation of the Narrowing Space ⋮ Detecting redundant narrowing derivations by the LSE-SL reducibility test ⋮ Improving transformation systems for general E-unification ⋮ On narrowing, refutation proofs and constraints ⋮ Incremental constraint satisfaction for equational logic programming ⋮ Combination problems for commutative/monoidal theories or how algebra can help in equational unification ⋮ The disconnection tableau calculus ⋮ Enumerating outer narrowing derivations for constructor-based term rewriting systems ⋮ Equation solving in conditional AC-theories ⋮ On modularity in term rewriting and narrowing ⋮ On completeness of narrowing strategies ⋮ Conditional equational theories and complete sets of transformations ⋮ Theorem proving modulo ⋮ A compositional semantic basis for the analysis of equational Horn programs ⋮ Incremental theory reasoning methods for semantic tableaux ⋮ Unification theory ⋮ Unification in a combination of arbitrary disjoint equational theories ⋮ On the connection between narrowing and proof by consistency ⋮ A completion-based method for mixed universal and rigid E-unification ⋮ Complete sets of transformations for general E-unification

Cites Work

• A class of confluent term rewriting systems and unification
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• A Machine-Oriented Logic Based on the Resolution Principle
• Equality, types, modules, and (why not?) generics for logic programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Basic narrowing revisited