Negative Hyper-Resolution for Proving Statements Containing Transitive Relations
Abstract
A modified version of PHR~- resolution comprising negative hyper-resolution and paramodulation is introduced to reduce the search of statements that contain transitive relations. Let R be a symbol of transitive relation and let a nucleus contain the literal tRp, and let a factor of an electron be of the form C V nt,Rt2.Moreover let us suppose that tU = t,U, where U is a simultaneous most general unifier for the corresponding clash. Then the resolvent of this clash contains the subclause (C V pRt2)U. This rule of deduction is said to Be TPHR- rule. It is shown that TPHR"- resolution is complete. More precisely, it is shown that the empty clause a can be deduced from a set G of clauses which contains the axiom of transitivity Tr for the relation R by using PHR""- resolution iff can be deduced from the set G-Trby using TPHR"- resolution. The efficiency of the use of TPHR~rule is illustrated by examples.
Cite
Text
Gergely and Vershinin. "Negative Hyper-Resolution for Proving Statements Containing Transitive Relations." International Joint Conference on Artificial Intelligence, 1983.Markdown
[Gergely and Vershinin. "Negative Hyper-Resolution for Proving Statements Containing Transitive Relations." International Joint Conference on Artificial Intelligence, 1983.](https://mlanthology.org/ijcai/1983/gergely1983ijcai-negative/)BibTeX
@inproceedings{gergely1983ijcai-negative,
title = {{Negative Hyper-Resolution for Proving Statements Containing Transitive Relations}},
author = {Gergely, Tamás and Vershinin, Konstantin},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1983},
pages = {877-881},
url = {https://mlanthology.org/ijcai/1983/gergely1983ijcai-negative/}
}