Geodesic
Interactive realizations of logical formulas
Vestnik Udmurtskogo universiteta. Matematika, mehanika, kompʹûternye nauki, Tome 26 (2016) no. 2, pp. 177-193 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice de l'article

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. 
@article{VUU_2016_26_2_a3,
     author = {A. P. Beltyukov},
     title = {Interactive realizations of logical formulas},
     journal = {Vestnik Udmurtskogo universiteta. Matematika, mehanika, kompʹ\^uternye nauki},
     pages = {177--193},
     year = {2016},
     volume = {26},
     number = {2},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/VUU_2016_26_2_a3/}
}
TY  - JOUR
AU  - A. P. Beltyukov
TI  - Interactive realizations of logical formulas
JO  - Vestnik Udmurtskogo universiteta. Matematika, mehanika, kompʹûternye nauki
PY  - 2016
SP  - 177
EP  - 193
VL  - 26
IS  - 2
UR  - http://geodesic.mathdoc.fr/item/VUU_2016_26_2_a3/
LA  - ru
ID  - VUU_2016_26_2_a3
ER  - 
%0 Journal Article
%A A. P. Beltyukov
%T Interactive realizations of logical formulas
%J Vestnik Udmurtskogo universiteta. Matematika, mehanika, kompʹûternye nauki
%D 2016
%P 177-193
%V 26
%N 2
%U http://geodesic.mathdoc.fr/item/VUU_2016_26_2_a3/
%G ru
%F VUU_2016_26_2_a3
A. P. Beltyukov. Interactive realizations of logical formulas. Vestnik Udmurtskogo universiteta. Matematika, mehanika, kompʹûternye nauki, Tome 26 (2016) no. 2, pp. 177-193. http://geodesic.mathdoc.fr/item/VUU_2016_26_2_a3/

[1] Markov A. A., “An attempt to construct the logic of constructive mathematics”, Investigations on the theory of algorithms and mathematical logic, Proceedings, v. 2, M., 1976, 3–31 (in Russian)

[2] Shanin N. A., “A hierarchy of ways of understanding judgements in constructive mathematics”, Tr. Mat. Inst. Steklova, 129 (1973), 203–266 (in Russian) | MR | Zbl

[3] Kleene S. C., Introduction to metamathematics, North-Holland, 1951, 500 pp. | MR

[4] Vereshchagin N. K., Shen' A., Lectures on mathematical logic and algorithm theory, v. 3, Computable functions, Moscow Center for Continuous Mathematical Education, M., 2012, 160 pp.

[5] Maslov S. Yu., “The inverse method for establishing deducibility for logical calculi”, Tr. Mat. Inst. Steklova, 98 (1968), 26–87 (in Russian) | MR | Zbl

[6] Beltiukov A. P., “Intuitionistic formal theories with realizability in subrecursive classes”, Annals of Pure and Applied Logic, 89 (1997), 3–15 | DOI | MR | Zbl

[7] Beltiukov A. P., “A strong induction scheme that leads to polynomially computable realizations”, Theoretical Computer Science, 322 (2004), 17–39 | DOI | MR | Zbl

[8] 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, 27 (2006), 11–19