scientific article; zbMATH DE number 3856444

MaRDI QIDQ3325075zbMATH OpenFDO

Authors Wolfgang Küchlin

Publication date 1982

zbMATH Keywords

computational logicKnuth-Bendix algorithmresolution theorem-provingalgebraic abstract data type completion

Mathematics Subject Classification ID

Data structures (68P05)

Recommendations

• scientific article; zbMATH DE number 4076598
• scientific article; zbMATH DE number 44069
• scientific article; zbMATH DE number 3928345
• Knuth-bendix completion of horn clause programs for restricted linear resolution and paramodulation
• Some experiments with a completion theorem prover

Cited in

(15)

• Abstract reduction systems and idea of Knuth-Bendix completion algorithm
• Citius altius fortius: lessons learned from the theorem prover Waldmeister
• scientific article; zbMATH DE number 4022667 (Why is no real title available?)
• scientific article; zbMATH DE number 3928345 (Why is no real title available?)
• scientific article; zbMATH DE number 782043 (Why is no real title available?)
• scientific article; zbMATH DE number 915924 (Why is no real title available?)
• Relational Methods in Computer Science
• Buchberger's algorithm: The term rewriter's point of view
• On pot, pans and pudding or how to discover generalised critical pairs
• Solving divergence in Knuth--Bendix completion by enriching signatures
• KBCV – Knuth-Bendix Completion Visualizer
• scientific article; zbMATH DE number 3913723 (Why is no real title available?)
• Knuth-Bendix completion for non-symmetric transitive relations
• History and basic features of the critical-pair/completion procedure
• A strategy to deal with divergent rewrite systems

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 Q3325075)