scientific article; zbMATH DE number 67451

MaRDI QIDQ4012174zbMATH OpenFDO

Authors Nachum Dershowitz

Publication date 27 September 1992

zbMATH Keywords

paramodulationequational Horn theories

Mathematics Subject Classification ID

Artificial intelligence (68T99) Logic programming (68N17) Mechanization of proofs and logical operations (03B35)

Recommendations

• A maximal-literal unit strategy for horn clauses
• scientific article; zbMATH DE number 176740
• Efficient deduction in equality Horn logic by Horn-completion
• Horn equational theories and paramodulation
• Theorem proving with ordering and equality constrained clauses

Cited in

(11)

• Theorem proving with ordering and equality constrained clauses
• On theorem-proving in Horn theories with built-in algebras
• Canonical ground Horn theories
• Horn equational theories and paramodulation
• A maximal-literal unit strategy for horn clauses
• Strategy of searching of a conclusion in Horn clauses with unitary consideration of sub-target
• scientific article; zbMATH DE number 3924139 (Why is no real title available?)
• Structures for abstract rewriting
• scientific article; zbMATH DE number 1754647 (Why is no real title available?)
• scientific article; zbMATH DE number 176740 (Why is no real title available?)
• Linear and unit-resulting refutations for Horn 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 Q4012174)