Connection Structures
Elmar Eder · 1992
In Sections 2.4 and 2.5 we have shown that resolution can p-simulate (and even simulate step by step) the connection calculus, but that the connection calculus cannot p-simulate resolution. We have noted at the end of Section 2.5 that there are two main features which resolution has but the connection calculus does not have, and this is the main reason why the connection calculus cannot p-simulate resolution. One of these features is the use of lemmata. The other is the ability to forget variables.