A Computer Algorithm for the Determination of Deducibility on the Basis of the Inverse Method

  • A. O. Slisenko
Part of the Symbolic Computation book series (SYMBOLIC)


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 [1]; we shall use the terminology of the latter without further explanations.


Function Symbol Inverse Method Atomic Formula Basis Skeleton Logical Calculus 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Literature Cited

  1. 1.
    S.Yu. Maslov, “An inverse method for establishing deducibility for logical calculi”, Trudy Mathem. Inst. AN SSSR, 98: 26–87 (1968).MATHGoogle Scholar
  2. 2.
    S.Yu. Maslov, “Deduction-search tactics based on unification of the order of members in a favorable assemblage”, this volume, p. 64.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1983

Authors and Affiliations

  • A. O. Slisenko

There are no affiliations available

Personalised recommendations