Vestnik Udmurtskogo Universiteta. Matematika. Mekhanika. Komp'yuternye Nauki General information Latest issue Archive Impact factor Search papers Search references RSS Latest issue Current issues Archive issues What is RSS

 Vestn. Udmurtsk. Univ. Mat. Mekh. Komp. Nauki: Year: Volume: Issue: Page: Find

 Personal entry: Login: Password: Save password Enter Forgotten password? Register

 Vestn. Udmurtsk. Univ. Mat. Mekh. Komp. Nauki, 2016, Volume 26, Issue 2, Pages 177–193 (Mi vuu529)  MATHEMATICS

Interactive realizations of logical formulas

A. P. Beltyukov

Udmurt State University, ul. Universitetskaya, 1, Izhevsk, 426034, Russia

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.

DOI: https://doi.org/10.20537/vm160204  Full text: PDF file (222 kB) References: PDF file   HTML file

Bibliographic databases:  UDC: 510.252
MSC: 03B20, 03B30

Citation: A. P. Beltyukov, “Interactive realizations of logical formulas”, Vestn. Udmurtsk. Univ. Mat. Mekh. Komp. Nauki, 26:2 (2016), 177–193 Citation in format AMSBIB
\Bibitem{Bel16} \by A.~P.~Beltyukov \paper Interactive realizations of logical formulas \jour Vestn. Udmurtsk. Univ. Mat. Mekh. Komp. Nauki \yr 2016 \vol 26 \issue 2 \pages 177--193 \mathnet{http://mi.mathnet.ru/vuu529} \crossref{https://doi.org/10.20537/vm160204} \mathscinet{http://www.ams.org/mathscinet-getitem?mr=3522922} \elib{https://elibrary.ru/item.asp?id=26244777} 

 SHARE:      •  Contact us: math-net2021_10 [at] mi-ras ru Terms of Use Registration to the website Logotypes © Steklov Mathematical Institute RAS, 2021