METHOD OF ESTABLISHING DEDUCIBILITY
G. V. Davydov · 1969
1. In [1] and [2], S. Yu. Maslov proposed an inverse of establishing deducibility in classical predicate calculus.t In the deduction search by this method the volume of choices grows substantially as the quantity of favorable sets accumulated to a given time increases. Moreover, in discarding the ends of favorable sets by rule B in the inverse some information is lost, whose utilization might shorten the subsequent process of establishing deducibility in a number of cases. Hence, it is expedient to try to decrease the quantity of objects participating in the choice by the max imal merger offavorable sets into one objeCt (if only of more complex structure) and to take account of the mentioned information.