RUS  ENG JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PERSONAL OFFICE
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:

Document Type: Article
UDC: 510.252
MSC: 03B20, 03B30
Received: 05.05.2016

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{http://elibrary.ru/item.asp?id=26244777}


Linking options:
  • http://mi.mathnet.ru/eng/vuu529
  • http://mi.mathnet.ru/eng/vuu/v26/i2/p177

    SHARE: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Вестник Удмуртского университета. Математика. Механика. Компьютерные науки
    Number of views:
    This page:92
    Full text:24
    References:21

     
    Contact us:
     Terms of Use  Registration  Logotypes © Steklov Mathematical Institute RAS, 2018