A goal-type driven method of solving Horn logic with equality

DOI10.1007/BF02945313zbMATH Open0725.68087OpenAlexW2994540178MaRDI QIDQ2277873FDOQ2277873

Authors: Yunfa Hu 

Publication date: 1990

Published in: Journal of Computer Science and Technology (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf02945313

Recommendations

• Efficient deduction in equality Horn logic by Horn-completion
• scientific article; zbMATH DE number 3924139
• On solving the equality problem in theories defined by Horn clauses
• An inference system for horn clause logic with equality
• The homogeneous form of logic programs with equality
• scientific article; zbMATH DE number 4090847
• An equational approach to logic programming
• A theory of complete logic programs with equality
• Goal-oriented conjecturing for Isabelle/HOL
• scientific article; zbMATH DE number 4195157

zbMATH Keywords

resolutionunificationgoal-type driven methodHorn logic with equality

Mathematics Subject Classification ID

Data structures (68P05)

Cited In (2)

• An universal termination condition for solving goals in equational languages
• On solving the equality problem in theories defined by Horn clauses

This page was built for publication: A goal-type driven method of solving Horn logic with equality

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