scientific article; zbMATH DE number 67451

zbMATH Open0745.68089MaRDI QIDQ4012174FDOQ4012174

Authors: Nachum Dershowitz 

Publication date: 27 September 1992

Title of this publication is not available (Why is that?)

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

zbMATH Keywords

paramodulationequational Horn theories

Mathematics Subject Classification ID

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

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
• Title not available (Why is that?)
• Structures for abstract rewriting
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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)