scientific article; zbMATH DE number 3926235

MaRDI QIDQ3700828zbMATH OpenFDO

Authors Hassan Aït-Kaci

Publication date 1985

Full work available at URL https://eudml.org/doc/92240

zbMATH Keywords

automatic inference methodcomplete automation of the Knuth- Bendix methodfunction symbolsminimal partial orderingProlog programterm-rewriting rulestermination-proving program

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Recommendations

• Automating the Knuth Bendix ordering
• scientific article; zbMATH DE number 3905845
• On the complexity of recursive path orderings
• Extensions and comparison of simplification orderings
• Automatic termination proofs with transformation orderings

Cites work

• A complete proof of correctness of the Knuth-Bendix completion algorithm
• Complete Sets of Reductions for Some Equational Theories
• Computing in systems described by equations
• Computing with rewrite systems
• scientific article; zbMATH DE number 3810909 (Why is no real title available?)
• scientific article; zbMATH DE number 3821100 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• On multiset orderings
• Orderings for term-rewriting systems
• Programming with Equations
• Proving termination with multiset orderings
• Tree-Manipulating Systems and Church-Rosser Theorems

Cited in

(5)

• Termination of rewriting
• Fuzzy lattice operations on first-order terms over signatures with similar constructors: a constraint-based approach
• Recursive Path Orderings Can Also Be Incremental
• Combinatorial Algorithms for Listing Paths in Minimal Change Order
• Automating the Knuth Bendix ordering

Describes a project that uses

Uses Software

• REVE

This page was built for publication:

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