scientific article; zbMATH DE number 4090847

MaRDI QIDQ3817652zbMATH OpenFDO

Authors Nachum Dershowitz, G. Sivakumar

Publication date 1988

zbMATH Keywords

conditional rewrite rulesconditional term rewriting systemsequation solving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Equational classes, universal algebra in model theory (03C05)

Recommendations

• Equation solving in conditional AC-theories
• An universal termination condition for solving goals in equational languages
• Publication:3490956
• A rationale for conditional equational programming
• Combining Logic Programming and Equation Solving

Cited in

(12)

• Equation solving in conditional AC-theories
• Extracting Higher-Order Goals from the Mizar Mathematical Library
• Termination of narrowing via termination of rewriting
• A goal-type driven method of solving Horn logic with equality
• scientific article; zbMATH DE number 4035205 (Why is no real title available?)
• An universal termination condition for solving goals in equational languages
• scientific article; zbMATH DE number 4110161 (Why is no real title available?)
• Specification and proof in membership equational logic
• Completion-time optimization of rewrite-time goal solving
• scientific article; zbMATH DE number 4045106 (Why is no real title available?)
• Goal-directed completion using SOUR graphs
• Narrowing directed by a graph of terms

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