Redundancy criteria for constrained completion

DOI10.1016/0304-3975(94)00274-6MaRDI QIDQ673620zbMATH OpenOpenAlexFDO

Authors Juan-Miguel Gracia

Publication date 28 February 1997

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

Copyright license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International

Full work available at URL https://doi.org/10.1016/0304-3975(94)00274-6

zbMATH Keywords

inference systems

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Recommendations

• Redundancy criteria for constrained completion
• Critical pair criteria for completion
• Completion for constrained term rewriting systems
• Complete sets of reductions with constraints
• scientific article; zbMATH DE number 44069

Cites work

• scientific article; zbMATH DE number 4164128 (Why is no real title available?)
• scientific article; zbMATH DE number 3928345 (Why is no real title available?)
• scientific article; zbMATH DE number 3928346 (Why is no real title available?)
• scientific article; zbMATH DE number 3981150 (Why is no real title available?)
• scientific article; zbMATH DE number 50648 (Why is no real title available?)
• scientific article; zbMATH DE number 176755 (Why is no real title available?)
• scientific article; zbMATH DE number 1348468 (Why is no real title available?)
• scientific article; zbMATH DE number 1348470 (Why is no real title available?)
• A proof theory for general unification
• Complete sets of reductions with constraints
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Consider only general superpositions in completion procedures
• Critical pair criteria for completion
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Proving refutational completeness of theorem-proving strategies
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• SOLVING SYMBOLIC ORDERING CONSTRAINTS
• Unnecessary inferences in associative-commutative completion procedures
• Using forcing to prove completeness of resolution and paramodulation

Cited in

(7)

• Complete sets of reductions with constraints
• On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs
• Rewrite semantics for production rule systems: theory and applications
• Local simplification
• Redundancy criteria for constrained completion
• Harald Ganzinger's legacy: contributions to logics and programming
• Local simplification

This page was built for publication: Redundancy criteria for constrained completion

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q673620)