A Computer Algorithm for the Determination of Deducibility on the Basis of the Inverse Method
The object of the present article is to give a brief description of an algorithm developed by the Mathematical Logic Group of the Leningrad Branch of the V.A. Steklov Mathematical Institute (LOMI) of the Academy of Sciences of the USSR for the determination of deducibility in the classical predicate calculus with function symbols. The deducibility determination algorithm (DDA) has its theoretical foundation in the inverse method of establishing deducibility for logical calculi, as described, for example, in ; we shall use the terminology of the latter without further explanations.
Unable to display preview. Download preview PDF.