Refutation search for Horn sets by a subgoal-extraction method

DOI10.1016/0743-1066(90)90043-5MaRDI QIDQ3485884zbMATH OpenOpenAlexFDO

Authors

Publication date 1990

Published in The Journal of Logic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0743-1066(90)90043-5

zbMATH Keywords

automated theorem provinglogic programmingHorn setsrefutation searchdeductive-databases management

Mathematics Subject Classification ID

Logic programming (68N17) Logic in artificial intelligence (68T27)

Recommendations

• scientific article; zbMATH DE number 3978440
• Subgoal alternation in model elimination
• A formal grammatical model of the resolution method for the propositional calculus
• scientific article; zbMATH DE number 4047180
• A disjunctive positive refinement of model elimination and its application to subsumption deletion

Cited in

(5)

• The anatomy of vampire. Implementing bottom-up procedures with code trees
• Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
• Strategy of searching of a conclusion in Horn clauses with unitary consideration of sub-target
• Subgoal alternation in model elimination
• Tree-like unit refutations in Horn constraint systems

This page was built for publication: Refutation search for Horn sets by a subgoal-extraction method

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3485884)