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/

[1] S. N. Vasilev, A. K. Zherlov, E. A. Fedunov, B. E. Fedosov, Intellektnoe upravlenie dinamicheskimi sistemami, Fizmatlit, M., 2000

[2] A. K. Zherlov, S. N. Vasilev, “Ischisleniya pozitivno-obrazovannykh formul”, Aktualnye problemy informatiki, prikladnoi matematiki i mekhaniki, Ch. 1, Sb. nauchnykh trudov, Krasnoyarsk, 1996, 44–56

[3] J. A. Robinson, “A Machine-Oriented Logic Based on Resolution Principle”, Journal of ACM, 1965, January, 23–41 | DOI | MR | Zbl

[4] Peter Graf, “Substitution Tree Indexing”, Proceedings of the 6th International Conference on Rewriting Techniques and Applications, 1995, 117–131

[5] M. Stickel, The path-indexing method for indexing terms, Technical Note 473, Artificial Intelligence Center, SRI International, RAVENSWOOD AVE., MENLO PARK, CA 94025

[6] E. A. Cherkashin, “Razdelyaemye struktury dannykh v sisteme avtomaticheskogo dokazatelstva teorem KVANT/3”, Vychislitelnye tekhnologii, 13 (2008), 102–107

[7] W. W. McCune, “Experiments with Discrimination-Tree indexing and Path Indexing for Term Retrieval”, Journal of Automated Reasoning, 9:2 (1992), 147–167 | DOI | MR | Zbl

[8] A. V. Davydov, “Ischislenie pozitivno-obrazovannykh formul s funktsionalnymi simvolami”, Prikladnye algoritmy v diskretnom analize, Sb. nauch. tr., ed. d-r fiz.-mat. nauk, prof. Yu. D. Korolkov, Izd-vo Irkut. gos. Un-ta, Irkutsk, 2008