Geodesic
A synthesis of the resolution method and the inverse method
Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part IV, Tome 20 (1971), pp. 24-35 
G. V. Davydov. A synthesis of the resolution method and the inverse method. Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part IV, Tome 20 (1971), pp. 24-35. http://geodesic.mathdoc.fr/item/ZNSL_1971_20_a2/
@article{ZNSL_1971_20_a2,
     author = {G. V. Davydov},
     title = {A~synthesis of the resolution method and the inverse method},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {24--35},
     year = {1971},
     volume = {20},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_1971_20_a2/}
}
TY  - JOUR
AU  - G. V. Davydov
TI  - A synthesis of the resolution method and the inverse method
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 1971
SP  - 24
EP  - 35
VL  - 20
UR  - http://geodesic.mathdoc.fr/item/ZNSL_1971_20_a2/
LA  - ru
ID  - ZNSL_1971_20_a2
ER  - 
%0 Journal Article
%A G. V. Davydov
%T A synthesis of the resolution method and the inverse method
%J Zapiski Nauchnykh Seminarov POMI
%D 1971
%P 24-35
%V 20
%U http://geodesic.mathdoc.fr/item/ZNSL_1971_20_a2/
%G ru
%F ZNSL_1971_20_a2

Voir la notice du chapitre de livre provenant de la source Math-Net.Ru

It is introduced a compact coding of (finite sets of) propositional formulas by means of plane configurations called diagrams. A special kind of diagrams (called closed ones) is defined by some pure combinatorial properties. It is proved that a formula is a tautology iff its diagram is closed. An inductive procedure of generation of all closed diagrams is described. This procedure combines the ideas of the resolution method [1] and the inverse method [2]. Some isomorphism between the mentioned methods is stated.