Archive of Issues
Russia Izhevsk
Section  Mathematics 
Title  Interactive realizations of logical formulas 
Author(s)  Beltyukov A.P.^{a} 
Affiliations  Udmurt State University^{a} 
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. 177193. 
References 

Full text 