Completion of rewrite systems with membership constraints. I: Deduction rules

DOI10.1006/jsco.1997.0185zbMath0983.68091OpenAlexW2087458172MaRDI QIDQ1264438

Hubert Comon

Publication date: 29 April 2002

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

Full work available at URL: https://doi.org/10.1006/jsco.1997.0185

zbMATH Keywords

constrained equational logic

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Logic in artificial intelligence (68T27) Theory of programming languages (68N15) Grammars and rewriting systems (68Q42)

Related Items (14)

Decidability of bounded second order unification ⋮ Simplifying the signature in second-order unification ⋮ Reducing Relative Termination to Dependency Pair Problems ⋮ Sentence-normalized conditional narrowing modulo in rewriting logic and Maude ⋮ On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories ⋮ Decidability of bounded higher-order unification ⋮ Specification and proof in membership equational logic ⋮ Strict coherence of conditional rewriting modulo axioms ⋮ Solving divergence in Knuth--Bendix completion by enriching signatures ⋮ On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs ⋮ Knuth-Bendix Completion for Non-Symmetric Transitive Relations ⋮ Solvability of context equations with two context variables is decidable ⋮ A complete superposition calculus for primal grammars ⋮ On rewrite constraints and context unification

This page was built for publication: Completion of rewrite systems with membership constraints. I: Deduction rules