Negative Hyper-Resolution for Proving Statements Containing Transitive Relations

Gergely, Tamás; Vershinin, Konstantin

Negative Hyper-Resolution for Proving Statements Containing Transitive Relations

Download BibTeX Cite

Proceedings of the Eighth International Joint Conference on Artificial Intelligence. Theorem Proving. Pages 877-880.

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 r t 1 Rt 2 .Moreover let us suppose that tU = t u, where U is a simultaneous most general Onifier for the corresponding clash. Then the resolvent of this clash contains the subclause (C V pRt 2 )U. Th~s rule of deduction is said to oe TPHR - rule. It is shown that TPHR-- resolution is complete. More precisely, it is shown that the empty clause o can be deduced from a set G of clauses which contains the axiom of transitivity TrR for the relation R by using PHR-- resolution iff o can be deduced from the set G- {TrR} by using TPHR-- resolution. . The efficiency of the use of TPHR-rule is illustrated by examples.

Tamás Gergely, and Konstantin Vershinin. 1983. Negative Hyper-Resolution for Proving Statements Containing Transitive Relations. In Proceedings of the Eighth International Joint Conference on Artificial Intelligence, IJCAI-83. IJCAI, 877–880. https://ijcai.org/proceedings/1983/210

@inproceedings{ijcai1983p210,
  title     = {Negative Hyper-Resolution for Proving Statements Containing Transitive Relations},
  author    = {Gergely, Tamás and Vershinin, Konstantin},
  booktitle = {Proceedings of the Eighth International Joint Conference on
               Artificial Intelligence, {IJCAI-83}},
  publisher = {International Joint Conferences on Artificial Intelligence},
  editor    = {Alan Bundy},
  pages     = {877--880},
  year      = {1983},
  note      = {Theorem Proving},
  url       = {https://ijcai.org/proceedings/1983/210},
}

TY  - CPAPER
TI  - Negative Hyper-Resolution for Proving Statements Containing Transitive Relations
AU  - Gergely, Tamás
AU  - Vershinin, Konstantin
T2  - Proceedings of the Eighth International Joint Conference on Artificial Intelligence, IJCAI-83
PB  - International Joint Conferences on Artificial Intelligence
PY  - 1983
SP  - 877
EP  - 880
UR  - https://ijcai.org/proceedings/1983/210
ER  -