scientific article; zbMATH DE number 67451

MaRDI QIDQ4012174zbMATH OpenFDO

Authors Nachum Dershowitz

Publication date 27 September 1992

zbMATH Keywords

equational Horn theoriesparamodulation

Mathematics Subject Classification ID

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

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)

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

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)