Formalization as the Immanent Part of Logical Solving
##plugins.themes.bootstrap3.article.sidebar##
Published:
30.05.2018
##plugins.themes.bootstrap3.article.main##
Abstract
The work is devoted to the logical analysis of the problem solving by logical means.
It starts from general characteristic of the applied logic as a tool:
1. to bound logic with its applications in theory and practice; 2. to import methods and methodologies from other domains into logic; 3. to export methods and methodologies from logic into other domains.
The precise solving of a precisely stated logical problem occupies only one third of the whole process of solving real problems by logical means. The formalizing precedes it and the deformalizing follows it.
The main topic when considering formalization is a choice of a logic. The classical logic is usually the best one for a draft formalization. The given problem and peculiarities of the draft formalization could sometimes advise us to use some other logic.
If axioms of the classical formalization have some restricted form this is often the advice to use temporal, modal or multi-valued logic. More precisely, if all binary predicates occur only in premises of implications then it is possible sometimes to replace a predicate classical formalization by a propositional modal or temporal in the appropriate logic. If all predicates are unary and some of them occur only in premises then the classical logic maybe can replaced by a more adequate multi-valued. This idea is inspired by using Rosser–Turkette operator $J_i$in the book [22]. If we are interested not in a bare proof but in construction it gives us it is often to transfer to an appropriate constructive logic. Its choice is directed by our main resource (time, real values, money or any other imaginable resource) and by other restrictions.Logics of different by their nature resources are mutually inconsistent (e.g. nilpotent logics of time and linear logics of money).
Also it is shown by example how Arnold’s principle works in logic: too “precise” formalization often becomes less adequate than more “rough”. DOI: 10.21146/2074-1472-2018-24-1-129-145
It starts from general characteristic of the applied logic as a tool:
1. to bound logic with its applications in theory and practice; 2. to import methods and methodologies from other domains into logic; 3. to export methods and methodologies from logic into other domains.
The precise solving of a precisely stated logical problem occupies only one third of the whole process of solving real problems by logical means. The formalizing precedes it and the deformalizing follows it.
The main topic when considering formalization is a choice of a logic. The classical logic is usually the best one for a draft formalization. The given problem and peculiarities of the draft formalization could sometimes advise us to use some other logic.
If axioms of the classical formalization have some restricted form this is often the advice to use temporal, modal or multi-valued logic. More precisely, if all binary predicates occur only in premises of implications then it is possible sometimes to replace a predicate classical formalization by a propositional modal or temporal in the appropriate logic. If all predicates are unary and some of them occur only in premises then the classical logic maybe can replaced by a more adequate multi-valued. This idea is inspired by using Rosser–Turkette operator $J_i$in the book [22]. If we are interested not in a bare proof but in construction it gives us it is often to transfer to an appropriate constructive logic. Its choice is directed by our main resource (time, real values, money or any other imaginable resource) and by other restrictions.Logics of different by their nature resources are mutually inconsistent (e.g. nilpotent logics of time and linear logics of money).
Also it is shown by example how Arnold’s principle works in logic: too “precise” formalization often becomes less adequate than more “rough”. DOI: 10.21146/2074-1472-2018-24-1-129-145
##plugins.generic.usageStats.downloads##
##plugins.generic.usageStats.noStats##
##plugins.themes.bootstrap3.article.details##
How to Cite
Nepejvoda N. N. Formalization as the Immanent Part of Logical Solving // Logicheskie Issledovaniya / Logical Investigations. 2018. VOL. 24. № 1. C. 129-145.
Issue
Section
Papers
References
“6th World Congress and School on Universal Logic”, [https://www.unilog.org/vichy2018 accessed on 08.08.2017].
“The AGDA Wiki”, [http://wiki.portal.chalmers.se/agda/pmwiki.php accessed on 08.08.2017].
Aristotle. The Complete Works of Aristotle: The Revised Oxford Translation. Princeton, N.J: Princeton University Press, 1984.
Arnold, V.I. “Zhestkie” i “myagkie» matematicheskie modeli” [“Hard” and “soft” mathematical models]. Moscow: MCNIMO, 2004. 32 pp. (In Russian)
Bell, J. L. “The Development of Categorical Logic”. In: Handbook of Philosophical Logic, Vol. 12. Springer: 2005.
Belyakin, N.V. “Ot redaktora perevoda” [Editor’s Notes]. in: Vopenka P. Al’ternativnaya teoriya mnozhestv: novyj vzglyad na beskonechnost [Alternative set theory: new pointo of view on infinity]. Novosibirsk: Izdatelstvo Insutituta Mastematiki, 2004. pp. 11–29. (in Russian)
Belyakin, N.V. “O nesushchestvovanii bol’shih kardinalov” [On non-existence of large cardinals], Chislo [Number], Мoscow: MAKS Press, 2009. pp. 169–192. (In Russian)
Burstall, R.M. “Electronic category theory”. In: Dembi_nski P. (eds) Mathematical Foundations of Computer Science 1980. MFCS 1980. Lecture Notes in Computer Science, Vol. 88. Berlin, Heidelberg: Springer, 1980.
Cotrini, C., Gurevich, Yu. “Basic primal infon logic”, Journal of Logic and Computation, 2016, Vol. 26, Issue 1, pp. 117–141.
Belyakin, N.V., Zhevlakova, E.K. “Operaciya diagonalizacii v voprosno-otvetnyh sistemah” [Diagonalization in QA systems], Vychislitelnye sistemy [Computing systems], 1976, No. 67, pp. 113–126.
Boole, G. The Mathematical Analysis of Logic, Being an Essay towards a Calculus of Deductive Reasoning. London, England: Macmillan, Barclay & Macmillan, 1847.
Boole, G. The Laws of Thought, facsimile of 1854 edition, with an introduction by John Corcoran. Buffalo: Prometheus Books, 2003.
Clarke, E. M., Grumberg, O., Peled, D. Model checking. MIT Press, 2010, pp. 330.
Di Cosmo R., Miller, D. “Linear Logic”, The Stanford Encyclopedia of Philosophy (Winter 2016 Edition), ed. by Edward N. Zalta, [https://plato.stanford.edu/archives/win2016/entries/logic-linear/ accessed on 08.08.2017].
Finn, V.K. Iskusstvewnnyj intellekt: metodologiya,primeneniya, filosofiya [Artificial intelligence: methodology, applications, philosophy]. Moscow: KRASAND, 2011, 448 pp. (In Russian)
Fortnow, L.; Homer, S. “A Short History of Computational Complexity”, Bulletin of the EATCS, 2003, Vol. 80, pp. 95–133.
Girard, J.-Y. “Linear logic”, Theoretical Computer Science, 1987, Vol. 50, pp. 1–102.
Girard, J.-Y. “Light Linear Logic”, Information and Computation, 1998, Vol. 143, No. 2, pp. 175–204.
Godel, K. “Uber formal unentscheidbare S_atze der Principia Mathematica und verwandter Systeme, I”, Monatshefte fur Mathematik und Physik, 1931, Vol. 38, pp. 173–198.
Gurevich, Yu., Neeman, I. “Infon logic: the propositional case”, ACM Transactions on Computation Logic, January 2011, Vol. 12, Issue 2, No. 9, pp. 1–28.
Collected Papers of Stig Kanger with Essays on his Life and Work, 2 vol., eds. by Ghita Holmstr_om-Hintikka, Sten Lindstr_om & Rysiek Sliwinski. Dordrecht (NL): Kluwer Academic Publishers, 2001.
Karpenko, A.S. Razvitie mnogoznachnoj logiki [The development of multi-valued logic]. Moscow: LKI Publishers, 2014. 448 pp. (In Russian)
Lord Kelvin, Tait, P.G. Treatise of natural philosophy part I, II. Cambridge: University Press, 1912.
Kiselev, A.A. Nedostizhimost’ i subnedostizhimost: monografiya v dvuch chastyah. Ch. 1 [Inaccessibility and subinaccessibility. In two parts. Part 1]. Minsk: BGU Edition, 2011. 113 pp. (In Russian)
Kiselev, A.A. Nedostizhimost’ i subnedostizhimost: monografiya v dvuch chastyah. Ch. 1 [Inaccessibility and subinaccessibility. In two parts. Part 2]. Minsk: BGU Edition, 2011, 154 pp. (In Russian)
Kleene, S.C. Introduction to Metamathematics. N. Y.: 1952.
Kochurov, E.V. “Konstruktivnyj sintez pol’zovatel’skih interfejsov Webprilozhenij” [Constructive synthesis of user interfaces of Web-applications], Programmnye sistemy: teoriya i prilozheniya [Program Systems: Theory and Applications], 2013, Vol. 4, No. 18, pp. 3–25. (In Russian)
Kochurov, E.V. “Ob odnoj konstruktivnoj logike postroenij na grafah” [On one constructive logic of graph constructions], Devyatye smirnovskie chteniya po logike, Moscow: Sovremennye tetradi, 2015, pp. 22–24. (In Russian)
Kochurov, E.V. “Primenenie logiki postroenij na grafah k ispolneniyu modelelj biznes-processov” [Application of the graph constructions logic to businessprocess modelling], Programmnye sistemy: teoriya i prilozheniya [Program Systems: Theory and Applications], 2015, Vol. 6, No. 4, pp. 359–366. (In Russian)
Kochurov, E.V., Nepejvoda N.N., Grigotrevskij I.N. “Zamechaniya o logikah postroenij na grafah i ih primenenii” [Notes on logics of graph constructions and their applications], Sbornik nauchnyh dokladov Vtoroj mezhdunarodnoj nauchno-prakticheskoj konferencii ‘Tehnicheskie nauki: teoriya, metodologiya i praktika’ [Collection of scientific presentations. Second international scientific-practical conference ‘Technical science: theory,methodology and practice’], Moscow: ANO ‘Scientific Survey’, 2014. (In Russian)
Kohen, M.R., Nagel, E. An Introduction to logic and scientific method. Harcourt: Brace and Co. 2nd ed. 1993.
Lambek, J., Scott, P.J. Introduction to Higher Order Categorical Logic. Cambridge: University Press, 1986.
Lincoln, P., Mitchell, J., Scedrov A., Shankar, N. “Decision problems for propositional linear logic”, Annals of Pure and Applied Logic, 1992, no 56, pp. 239–311.
Luxemburg, W.A.J. Nonstandard Analysis, Lectures on A. Robinson’s theory of infinitesimal and infinitely large numbers. Caltech Bookstore, 1962.
Luxemburg, W.A.J. “What is Nonstandard Analysis?“, American Mathematical Monthly, 1973, Vol. 80, pp. 38–67.
Macintyre, A.J., Wilkie, A.J. “On the decidability of the real exponential field”. In: Odifreddi P.G. Kreisel 70th Birthday Volume, CLSI, 1995.
Meshveliani, S.D. “Programmirovanie vychislitel’noj algebry na osnove konstruktivnoj matematiki. Oblasti s razlozheniem na prostye mnozhiteli” [Programming of computer algebra by constructive mathematics. Domains with factorization], Programmnye sistemy: teoriya i prilozheniya [Program Systems: Theory and Applications], 2017, Vol. 8, no 1, pp. 3–46. (In Russian)
Mill, J.S A System of Logic, Ratiocinative and Inductive. New York: Harper & Brothers, 1874.
Mints, G. A Short Introduction to Intuitionistic Logic. Kluwer, 2000.
De Morgan, A. Logic: On the Syllogism and Other Logical Writings, ed. by P. Heath, Routledge, 1966.
Nepejvoda, N.N. “O formalizacii neformalizuemyh ponyatiy: avtoproduktivnye sistemy teoriy” [Formalizing informalizable notions: autoproductive systems of theories], Semiotika i iniformatika [Semiotics and informatics], 1985, Vol. 25, pp. 46–93. (In Russian)
Nepejvoda, N.N. “O formalizacii neformalizuemogo” [Formalizinfg informalizablr], Logicheskiye issledovasniya [Logical Investigations], 2001, Vol. 8, pp. 129–143. (In Russian)
Nepejvoda, N.N. “Neformalizuemost kak logicheskaya harakteristika zhizni” [Informalizability as logical characteristic of life], Online journal ‘Logical Studies’, 1999, No. 3. (In Russian)
Nepejvoda, N.N. “A constructive logic of program schemata on a decidable universe”, Bulletin of the Section of Logic, 1988, Vol. 17, No. 3/4, pp. 138–145.
Nepejvoda, N.N. “Konstruktivnaya matematika: obzor dostizheniy, nedostatkov i urokov. Chast’ I” [Constructive mathematics: survey of susccesses, shortcomings and lessons. Part I], Logiceskie issledovaniya [Logical Investigations], 2001, Vol. 17, pp. 191–239. (In Russian)
Nepejvoda, N.N. “Konstruktivnaya matematika: obzor dostizheniy, nedostatkov i urokov. Chast’ II” [Constructive mathematics: survey of susccesses, shortcomings and lessons. Part II], Logiceskie issledovaniya [Logical Investigations], 2012, Vol. 18, pp. 157–181. (In Russian)
Nepejvoda, N.N. “Konstruktivnaya matematika: obzor dostizheniy, nedostatkov i urokov. Chast’ III” [Constructive mathematics: survey of susccesses, shortcomings and lessons. Part III], Logiceskie issledovaniya [Logical Investigations], 2014, Vol. 20, pp. 112–150. (In Russian)
Nepejvoda, N.N. “O konstruktivnyh logikah” [On constructive logics], Sintaksicheskie i semanticheskie issledovaniya neekstensionalnyh logik [Syntactic and semantic investigations of non-extensional logics], Moscow: Nauka, 1989, pp. 81–92. (In Russian)
Nepejvoda, N.N. Prikladnaya logika [Applied logics]. Novosibirsk: NGUPress, 2000, 521 pp. (In Russian)
Nepejvoda, N.N. Uroki konstruktivizma [Lessons of constructivism]. Heidelberg, 2011, 108 pp. (In Russian)
Nepejvoda, N.N. “Vyzovy logiki i matematiki XX v. i ‘otvet’ na nih civilizacii” [Challenges of logics and mathematics of XX century and ‘responce’ on them of the civilization], Voprosy Filosofii [Problems of Philosophy], 2005, No. 8, pp. 118–128. (In Russian)
Nepejvoda, N.N. “Vyvody v forme grafov” [Proofs as graphs], Semiotika i informatika [Semiotics and informatics]. Vol. 26. Moscow: VINITI, 1985. (In Russian)
Van Oosten, J. “Realizability: a historical essay”, Mathematical Structures in Comp. Sci., Vol. 12, No. 3, Cambridge University Press, 2002.
Peled, D., Pelliccione, P., Spoletini, P. “Model Checking”, Wiley Encyclopedia of Computer Science and Engineering, 2009.
Robinson, A. Non-standard analysis, ed. by Revised. Princeton University Press, 1996.
Sanjeev, A., Boaz, B. Computational Complexity: A Modern Approach. Cambridge, 2009.
Sei Shonagon. The Pillow Book. London, England: Penguin Books, 2006.
Shamkanov, D.S. “Circular proofs for the G_odel-L_ob provability logic”, Mathematical Notes, September 2014, Vol. 96, Issue 3–4, pp. 575–585.
Shestakov, V.I. Nekotorye matematicheskiye metody konstruirivaniyac i uproshcheniya dvuhpolusnyh elektricheskih shem klassa A [Some mathematical methods constructing and simplification of two-polar electricalk schemes of class A], Dr.Sc. Thesis, 1938. (In Russian)
Shestakov, V.I. “ Algebra dvuhpolusnyh shem postroennyh isklyuchitel’no iz dvuhpolusnikov (algebra A-shem)” [Algebra of bipolar schemes builded only by bipolar elements (algebra of A-schemes)], Avtomatika i telemehanika [Automatics and telemechanics], 1941, No. 2, pp. 15–24. (In Russian)
Solovay, R. M., Arthan, R. D., Harrison, J. “Some new results on decidability for elementary algebra and geometry”, Annals of Pure and Applied Logic, December 2012, Vol. 163, Issue 12, pp. 1765–1802.
Statman, R. “Intuitionistic Propositional Logic is Polynomial-Space Complete”, Theoretical Computer Science, 1979, Vol. 9, No. 1, pp. 67–72.
Tichy, P. The Foundations of Frege’s Logic. Berlin and New York: De Gruyter, 1988. 333 pp.
Vasyukov, V.L. Categorical Logic. Moscow: ANO Institute of Logic, 2005. 194 pp.
Vizel, Y., Weissenbacher, G., Malik, S. “Boolean Satisfiability Solvers and Their Applications in Model Checking”, Proceedings of the IEEE, 2015, Vol. 103, No. 11, pp. 2021–2035.
Vopenka, P. Mathematics in the Alternative Set Theory. Leipzig, 1979.
Whitehead, A.N., Russell, B. Principia Mathematica, 3 vols. Cambridge: Cambridge University Press, 1925–1927. (In Russian)
“The AGDA Wiki”, [http://wiki.portal.chalmers.se/agda/pmwiki.php accessed on 08.08.2017].
Aristotle. The Complete Works of Aristotle: The Revised Oxford Translation. Princeton, N.J: Princeton University Press, 1984.
Arnold, V.I. “Zhestkie” i “myagkie» matematicheskie modeli” [“Hard” and “soft” mathematical models]. Moscow: MCNIMO, 2004. 32 pp. (In Russian)
Bell, J. L. “The Development of Categorical Logic”. In: Handbook of Philosophical Logic, Vol. 12. Springer: 2005.
Belyakin, N.V. “Ot redaktora perevoda” [Editor’s Notes]. in: Vopenka P. Al’ternativnaya teoriya mnozhestv: novyj vzglyad na beskonechnost [Alternative set theory: new pointo of view on infinity]. Novosibirsk: Izdatelstvo Insutituta Mastematiki, 2004. pp. 11–29. (in Russian)
Belyakin, N.V. “O nesushchestvovanii bol’shih kardinalov” [On non-existence of large cardinals], Chislo [Number], Мoscow: MAKS Press, 2009. pp. 169–192. (In Russian)
Burstall, R.M. “Electronic category theory”. In: Dembi_nski P. (eds) Mathematical Foundations of Computer Science 1980. MFCS 1980. Lecture Notes in Computer Science, Vol. 88. Berlin, Heidelberg: Springer, 1980.
Cotrini, C., Gurevich, Yu. “Basic primal infon logic”, Journal of Logic and Computation, 2016, Vol. 26, Issue 1, pp. 117–141.
Belyakin, N.V., Zhevlakova, E.K. “Operaciya diagonalizacii v voprosno-otvetnyh sistemah” [Diagonalization in QA systems], Vychislitelnye sistemy [Computing systems], 1976, No. 67, pp. 113–126.
Boole, G. The Mathematical Analysis of Logic, Being an Essay towards a Calculus of Deductive Reasoning. London, England: Macmillan, Barclay & Macmillan, 1847.
Boole, G. The Laws of Thought, facsimile of 1854 edition, with an introduction by John Corcoran. Buffalo: Prometheus Books, 2003.
Clarke, E. M., Grumberg, O., Peled, D. Model checking. MIT Press, 2010, pp. 330.
Di Cosmo R., Miller, D. “Linear Logic”, The Stanford Encyclopedia of Philosophy (Winter 2016 Edition), ed. by Edward N. Zalta, [https://plato.stanford.edu/archives/win2016/entries/logic-linear/ accessed on 08.08.2017].
Finn, V.K. Iskusstvewnnyj intellekt: metodologiya,primeneniya, filosofiya [Artificial intelligence: methodology, applications, philosophy]. Moscow: KRASAND, 2011, 448 pp. (In Russian)
Fortnow, L.; Homer, S. “A Short History of Computational Complexity”, Bulletin of the EATCS, 2003, Vol. 80, pp. 95–133.
Girard, J.-Y. “Linear logic”, Theoretical Computer Science, 1987, Vol. 50, pp. 1–102.
Girard, J.-Y. “Light Linear Logic”, Information and Computation, 1998, Vol. 143, No. 2, pp. 175–204.
Godel, K. “Uber formal unentscheidbare S_atze der Principia Mathematica und verwandter Systeme, I”, Monatshefte fur Mathematik und Physik, 1931, Vol. 38, pp. 173–198.
Gurevich, Yu., Neeman, I. “Infon logic: the propositional case”, ACM Transactions on Computation Logic, January 2011, Vol. 12, Issue 2, No. 9, pp. 1–28.
Collected Papers of Stig Kanger with Essays on his Life and Work, 2 vol., eds. by Ghita Holmstr_om-Hintikka, Sten Lindstr_om & Rysiek Sliwinski. Dordrecht (NL): Kluwer Academic Publishers, 2001.
Karpenko, A.S. Razvitie mnogoznachnoj logiki [The development of multi-valued logic]. Moscow: LKI Publishers, 2014. 448 pp. (In Russian)
Lord Kelvin, Tait, P.G. Treatise of natural philosophy part I, II. Cambridge: University Press, 1912.
Kiselev, A.A. Nedostizhimost’ i subnedostizhimost: monografiya v dvuch chastyah. Ch. 1 [Inaccessibility and subinaccessibility. In two parts. Part 1]. Minsk: BGU Edition, 2011. 113 pp. (In Russian)
Kiselev, A.A. Nedostizhimost’ i subnedostizhimost: monografiya v dvuch chastyah. Ch. 1 [Inaccessibility and subinaccessibility. In two parts. Part 2]. Minsk: BGU Edition, 2011, 154 pp. (In Russian)
Kleene, S.C. Introduction to Metamathematics. N. Y.: 1952.
Kochurov, E.V. “Konstruktivnyj sintez pol’zovatel’skih interfejsov Webprilozhenij” [Constructive synthesis of user interfaces of Web-applications], Programmnye sistemy: teoriya i prilozheniya [Program Systems: Theory and Applications], 2013, Vol. 4, No. 18, pp. 3–25. (In Russian)
Kochurov, E.V. “Ob odnoj konstruktivnoj logike postroenij na grafah” [On one constructive logic of graph constructions], Devyatye smirnovskie chteniya po logike, Moscow: Sovremennye tetradi, 2015, pp. 22–24. (In Russian)
Kochurov, E.V. “Primenenie logiki postroenij na grafah k ispolneniyu modelelj biznes-processov” [Application of the graph constructions logic to businessprocess modelling], Programmnye sistemy: teoriya i prilozheniya [Program Systems: Theory and Applications], 2015, Vol. 6, No. 4, pp. 359–366. (In Russian)
Kochurov, E.V., Nepejvoda N.N., Grigotrevskij I.N. “Zamechaniya o logikah postroenij na grafah i ih primenenii” [Notes on logics of graph constructions and their applications], Sbornik nauchnyh dokladov Vtoroj mezhdunarodnoj nauchno-prakticheskoj konferencii ‘Tehnicheskie nauki: teoriya, metodologiya i praktika’ [Collection of scientific presentations. Second international scientific-practical conference ‘Technical science: theory,methodology and practice’], Moscow: ANO ‘Scientific Survey’, 2014. (In Russian)
Kohen, M.R., Nagel, E. An Introduction to logic and scientific method. Harcourt: Brace and Co. 2nd ed. 1993.
Lambek, J., Scott, P.J. Introduction to Higher Order Categorical Logic. Cambridge: University Press, 1986.
Lincoln, P., Mitchell, J., Scedrov A., Shankar, N. “Decision problems for propositional linear logic”, Annals of Pure and Applied Logic, 1992, no 56, pp. 239–311.
Luxemburg, W.A.J. Nonstandard Analysis, Lectures on A. Robinson’s theory of infinitesimal and infinitely large numbers. Caltech Bookstore, 1962.
Luxemburg, W.A.J. “What is Nonstandard Analysis?“, American Mathematical Monthly, 1973, Vol. 80, pp. 38–67.
Macintyre, A.J., Wilkie, A.J. “On the decidability of the real exponential field”. In: Odifreddi P.G. Kreisel 70th Birthday Volume, CLSI, 1995.
Meshveliani, S.D. “Programmirovanie vychislitel’noj algebry na osnove konstruktivnoj matematiki. Oblasti s razlozheniem na prostye mnozhiteli” [Programming of computer algebra by constructive mathematics. Domains with factorization], Programmnye sistemy: teoriya i prilozheniya [Program Systems: Theory and Applications], 2017, Vol. 8, no 1, pp. 3–46. (In Russian)
Mill, J.S A System of Logic, Ratiocinative and Inductive. New York: Harper & Brothers, 1874.
Mints, G. A Short Introduction to Intuitionistic Logic. Kluwer, 2000.
De Morgan, A. Logic: On the Syllogism and Other Logical Writings, ed. by P. Heath, Routledge, 1966.
Nepejvoda, N.N. “O formalizacii neformalizuemyh ponyatiy: avtoproduktivnye sistemy teoriy” [Formalizing informalizable notions: autoproductive systems of theories], Semiotika i iniformatika [Semiotics and informatics], 1985, Vol. 25, pp. 46–93. (In Russian)
Nepejvoda, N.N. “O formalizacii neformalizuemogo” [Formalizinfg informalizablr], Logicheskiye issledovasniya [Logical Investigations], 2001, Vol. 8, pp. 129–143. (In Russian)
Nepejvoda, N.N. “Neformalizuemost kak logicheskaya harakteristika zhizni” [Informalizability as logical characteristic of life], Online journal ‘Logical Studies’, 1999, No. 3. (In Russian)
Nepejvoda, N.N. “A constructive logic of program schemata on a decidable universe”, Bulletin of the Section of Logic, 1988, Vol. 17, No. 3/4, pp. 138–145.
Nepejvoda, N.N. “Konstruktivnaya matematika: obzor dostizheniy, nedostatkov i urokov. Chast’ I” [Constructive mathematics: survey of susccesses, shortcomings and lessons. Part I], Logiceskie issledovaniya [Logical Investigations], 2001, Vol. 17, pp. 191–239. (In Russian)
Nepejvoda, N.N. “Konstruktivnaya matematika: obzor dostizheniy, nedostatkov i urokov. Chast’ II” [Constructive mathematics: survey of susccesses, shortcomings and lessons. Part II], Logiceskie issledovaniya [Logical Investigations], 2012, Vol. 18, pp. 157–181. (In Russian)
Nepejvoda, N.N. “Konstruktivnaya matematika: obzor dostizheniy, nedostatkov i urokov. Chast’ III” [Constructive mathematics: survey of susccesses, shortcomings and lessons. Part III], Logiceskie issledovaniya [Logical Investigations], 2014, Vol. 20, pp. 112–150. (In Russian)
Nepejvoda, N.N. “O konstruktivnyh logikah” [On constructive logics], Sintaksicheskie i semanticheskie issledovaniya neekstensionalnyh logik [Syntactic and semantic investigations of non-extensional logics], Moscow: Nauka, 1989, pp. 81–92. (In Russian)
Nepejvoda, N.N. Prikladnaya logika [Applied logics]. Novosibirsk: NGUPress, 2000, 521 pp. (In Russian)
Nepejvoda, N.N. Uroki konstruktivizma [Lessons of constructivism]. Heidelberg, 2011, 108 pp. (In Russian)
Nepejvoda, N.N. “Vyzovy logiki i matematiki XX v. i ‘otvet’ na nih civilizacii” [Challenges of logics and mathematics of XX century and ‘responce’ on them of the civilization], Voprosy Filosofii [Problems of Philosophy], 2005, No. 8, pp. 118–128. (In Russian)
Nepejvoda, N.N. “Vyvody v forme grafov” [Proofs as graphs], Semiotika i informatika [Semiotics and informatics]. Vol. 26. Moscow: VINITI, 1985. (In Russian)
Van Oosten, J. “Realizability: a historical essay”, Mathematical Structures in Comp. Sci., Vol. 12, No. 3, Cambridge University Press, 2002.
Peled, D., Pelliccione, P., Spoletini, P. “Model Checking”, Wiley Encyclopedia of Computer Science and Engineering, 2009.
Robinson, A. Non-standard analysis, ed. by Revised. Princeton University Press, 1996.
Sanjeev, A., Boaz, B. Computational Complexity: A Modern Approach. Cambridge, 2009.
Sei Shonagon. The Pillow Book. London, England: Penguin Books, 2006.
Shamkanov, D.S. “Circular proofs for the G_odel-L_ob provability logic”, Mathematical Notes, September 2014, Vol. 96, Issue 3–4, pp. 575–585.
Shestakov, V.I. Nekotorye matematicheskiye metody konstruirivaniyac i uproshcheniya dvuhpolusnyh elektricheskih shem klassa A [Some mathematical methods constructing and simplification of two-polar electricalk schemes of class A], Dr.Sc. Thesis, 1938. (In Russian)
Shestakov, V.I. “ Algebra dvuhpolusnyh shem postroennyh isklyuchitel’no iz dvuhpolusnikov (algebra A-shem)” [Algebra of bipolar schemes builded only by bipolar elements (algebra of A-schemes)], Avtomatika i telemehanika [Automatics and telemechanics], 1941, No. 2, pp. 15–24. (In Russian)
Solovay, R. M., Arthan, R. D., Harrison, J. “Some new results on decidability for elementary algebra and geometry”, Annals of Pure and Applied Logic, December 2012, Vol. 163, Issue 12, pp. 1765–1802.
Statman, R. “Intuitionistic Propositional Logic is Polynomial-Space Complete”, Theoretical Computer Science, 1979, Vol. 9, No. 1, pp. 67–72.
Tichy, P. The Foundations of Frege’s Logic. Berlin and New York: De Gruyter, 1988. 333 pp.
Vasyukov, V.L. Categorical Logic. Moscow: ANO Institute of Logic, 2005. 194 pp.
Vizel, Y., Weissenbacher, G., Malik, S. “Boolean Satisfiability Solvers and Their Applications in Model Checking”, Proceedings of the IEEE, 2015, Vol. 103, No. 11, pp. 2021–2035.
Vopenka, P. Mathematics in the Alternative Set Theory. Leipzig, 1979.
Whitehead, A.N., Russell, B. Principia Mathematica, 3 vols. Cambridge: Cambridge University Press, 1925–1927. (In Russian)