TY - GEN
T1 - Hyper resolution and equality axioms without function substitutions
AU - Ozturk, Yusuf
AU - Henschen, Lawrence Joseph
PY - 1990/1/1
Y1 - 1990/1/1
N2 - When hyperresolution used with equality axioms, the function substitution axioms tend to produce myriads of new clauses whenever a positive equality literal is present. The analogue for paramodulation is the large number of potential paramodulants where the “into” term is not at the top level of its literal. In this study, we will prove that for some class of clause sets, the use of function substitution axioms can be eliminated. Analogously, paramodulation can be applied to the top level terms only.
AB - When hyperresolution used with equality axioms, the function substitution axioms tend to produce myriads of new clauses whenever a positive equality literal is present. The analogue for paramodulation is the large number of potential paramodulants where the “into” term is not at the top level of its literal. In this study, we will prove that for some class of clause sets, the use of function substitution axioms can be eliminated. Analogously, paramodulation can be applied to the top level terms only.
UR - http://www.scopus.com/inward/record.url?scp=85031793221&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85031793221&partnerID=8YFLogxK
U2 - 10.1007/3-540-52885-7_107
DO - 10.1007/3-540-52885-7_107
M3 - Conference contribution
AN - SCOPUS:85031793221
SN - 9783540528852
VL - 449 LNAI
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 456
EP - 469
BT - 10th International Conference on Automated Deduction, Proceedings
PB - Springer Verlag
T2 - 10th International Conference on Automated Deduction, CADE 1990
Y2 - 24 July 1990 through 27 July 1990
ER -