Страница публикации

The Calculus of Positively Constructed Formulas, its Features, Strategies and Implementation

Авторы: Larionov A., Davydov A., Cherkashin E.

Журнал: Proc. of 36th Intern. Convention on Information and Communication Technology, Electronics and Microelectronics (Opatija, Croatia, 20–24 May 2013)



Год: 2013

Отчётный год: 2013


Местоположение издательства:


Аннотация: Originally, the calculus of positively constructed formulas without function symbols was developed by Russian scientists S.N. Vassilyev and A.K. Zherlov by an evolutionary way in describing and solving of control theory problems. This calculus has features which are important, without loss of generality, for control theory applications. Later investigations shown that the calculus has features providing a good possibility to combine the proof procedure and the problem heuristics. Thus, calculus of positively constructed formulas can be characterized both as machine- and human-oriented. In this paper the calculus of positively constructed formulas with function symbols is considered. We provide the proofs of soundness and completeness for this calculus. Features, strategies, and some prototype prover implementation aspects are presented.

Индексируется WOS: 1

Индексируется Scopus: 1

Индексируется РИНЦ: 1

Публикация в печати: 0

Добавил в систему: