scientific article; zbMATH DE number 4090851

MaRDI QIDQ3817656zbMATH OpenFDO

Authors Harald Ganzinger

Publication date 1988

zbMATH Keywords

completionproof treesnonreductive critical pairs

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Recommendations

• A completion procedure for conditional equations
• scientific article; zbMATH DE number 4090770
• Critical pair criteria for completion
• scientific article; zbMATH DE number 3956434
• scientific article; zbMATH DE number 44069

Cited in

(20)

• On restrictions of ordered paramodulation with simplification
• Implementing contextual rewriting
• Conditional semi-Thue systems for presenting monoids
• Consider only general superpositions in completion procedures
• scientific article; zbMATH DE number 4049134 (Why is no real title available?)
• scientific article; zbMATH DE number 4078788 (Why is no real title available?)
• Completion-time optimization of rewrite-time goal solving
• Proving group isomorphism theorems
• scientific article; zbMATH DE number 4090770 (Why is no real title available?)
• Involutive Completion to Avoid LBB Condition
• A maximal-literal unit strategy for horn clauses
• Harald Ganzinger's legacy: contributions to logics and programming
• Critical pair criteria for completion
• Proof normalization for resolution and paramodulation
• scientific article; zbMATH DE number 3990847 (Why is no real title available?)
• Completion of first-order clauses with equality by strict superposition
• Knuth-bendix completion of horn clause programs for restricted linear resolution and paramodulation
• From search to computation: redundancy criteria and simplification at work
• Conditional rewriting logic: Deduction, models and concurrency
• Equation solving in conditional AC-theories

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