 +7 (3412) 91 60 92 imi@udsu.ru

## Archive of Issues

Russia Izhevsk
Year
2016
Volume
26
Issue
2
Pages
177-193
 Section Mathematics Title Interactive realizations of logical formulas Author(-s) Beltyukov A.P.a Affiliations Udmurt State Universitya Abstract A new constructive understanding of logical formulas is considered. This understanding corresponds to intuition and traditional means of constructive logical inference. The new understanding is logically simpler than traditional realizability (in the sense of quantifier depth), but it also natural with respect to algorithmic solution of tasks. This understanding uses not only witness (realization) of the formula to understand but it also uses notion of test (counteraction) of this realization at the given formula. The main form of a sentence to understand a formula $A$ is $a:A:b$, that means that “the witness $a$ wins the obstacle $b$ while trying to approve the formula $A$”. This procedure can be regarded as a procedure of arbitration for making the necessary solution. The basis of the arbitration procedure for atomic formulas is defined by the interpretation of the language. The procedure for complex sentences is given by special rules determining the meaning of logical connectives. In the most natural definition of the arbitration procedure it has polynomial time complexity. A formula $A$ is considered to be true in the new sense if there is a witness of the formula that wins all possible obstacles at the formula. A language without negation is considered. A theorem of correctness of traditional intuitionistic axioms and inference rules is proved. The system of logical inference is formulated in sequent form. It is oriented to the inverse method of logical inference search. Keywords logical formulas, understanding, realization, counteraction UDC 510.252 MSC 03B20, 03B30 DOI 10.20537/vm160204 Received 5 May 2016 Language Russian Citation Beltyukov A.P. Interactive realizations of logical formulas, Vestnik Udmurtskogo Universiteta. Matematika. Mekhanika. Komp'yuternye Nauki, 2016, vol. 26, issue 2, pp. 177-193. References Markov A.A. An attempt to construct the logic of constructive mathematics, Issledovaniya po teorii algorifmov I matematicheskoi logike: Sbornik statei, Tom 2 (Investigations on the theory of algorithms and mathematical logic: Proceedings, vol. 2), Moscow, 1976, pp. 3-31 (in Russian). Shanin N.A. A hierarchy of ways of understanding judgements in constructive mathematics, Tr. Mat. Inst. Steklova, 1973, vol. 129, pp. 203-266 (in Russian). Kleene S.C. Introduction to metamathematics, North-Holland, 1951, 500 p. Translated under the title Vvedenie v metamatematiku, Moscow: Inostr. Lit., 1957, 526 p. Vereshchagin N.K., Shen' A. Lektsii po matematicheskoi logike i teorii algoritmov. Chast' 3. Vychislimye funktsii (Lectures on mathematical logic and algorithm theory. Part 3. Computable functions), Moscow: Moscow Center for Continuous Mathematical Education, 2012, 160 p. Maslov S.Yu. The inverse method for establishing deducibility for logical calculi, Tr. Mat. Inst. Steklova, 1968, vol. 98, pp. 26-87 (in Russian). Beltiukov A.P. Intuitionistic formal theories with realizability in subrecursive classes, Annals of Pure and Applied Logic, 1997, vol. 89, pp. 3-15. Beltiukov A.P. A strong induction scheme that leads to polynomially computable realizations, Theoretical Computer Science, 2004, vol. 322, pp. 17-39. Beltiukov A.P. A polinomial programming language, Mathematical Problems of Computer Science: Transactions of the Institute for Informatics and Automation Problems of the National Academy of Sciences of Armenia, 2006, vol. 27, pp. 11-19. Full text