Geodesic
On the calculus of positively constructed formulas for authomated theorem proving
Modelirovanie i analiz informacionnyh sistem, Tome 17 (2010) no. 4, pp. 60-70

Voir la notice de l'article provenant de la source Math-Net.Ru

The paper deals with an expressive logic language LF and its calculus. Formulas of this language consist of some large-block structural elements, such as type quantifiers. The language LF contains only two logic symbols — $\forall$ and $\exists$, which form the set of logic connectives of the language. A logic calculus JF and complete strategy for automated proof search based on a single unary rule of inference are considered. This calculus has a number of other features that lead to the reduction of combinatorial complexity of finding the deductions in comparison with the known systems for automated theorem proving as the resolution method and Genzen calculus. Problems of effective implementation of JF as a program system for automated theorem proving are considered.
Keywords: automated theorem proving, mathematical logic, nonclassical logics, artificial intelligence. 
@article{MAIS_2010_17_4_a6,
     author = {A. V. Davydov and A. A. Larionov and E. A. Cherkashin},
     title = {On the calculus of positively constructed formulas for authomated theorem proving},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {60--70},
     publisher = {mathdoc},
     volume = {17},
     number = {4},
     year = {2010},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a6/}
}
TY  - JOUR
AU  - A. V. Davydov
AU  - A. A. Larionov
AU  - E. A. Cherkashin
TI  - On the calculus of positively constructed formulas for authomated theorem proving
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2010
SP  - 60
EP  - 70
VL  - 17
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a6/
LA  - ru
ID  - MAIS_2010_17_4_a6
ER  - 
%0 Journal Article
%A A. V. Davydov
%A A. A. Larionov
%A E. A. Cherkashin
%T On the calculus of positively constructed formulas for authomated theorem proving
%J Modelirovanie i analiz informacionnyh sistem
%D 2010
%P 60-70
%V 17
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a6/
%G ru
%F MAIS_2010_17_4_a6
A. V. Davydov; A. A. Larionov; E. A. Cherkashin. On the calculus of positively constructed formulas for authomated theorem proving. Modelirovanie i analiz informacionnyh sistem, Tome 17 (2010) no. 4, pp. 60-70. http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a6/