Диссертация (1149226), страница 25
Текст из файла (страница 25)
Д. Решение задач логико-предметного распознаванияобразов с использованием тактик обратного метода Маслова / Н. Д. Петухова,Т. М. Косовская // Компьютерные инструменты в образовании. — 2014. — № 3.— С. 9–20.48. Свидетельство№ 2016615547.Программадляавтоматическогодоказательства теорем в интуиционистских логических исчислениях обратнымметодом Маслова «WhaleProver» (WhaleProver) / автор и правообладательПавлов В. А.
— № 2016612689 ; заявл. 28.03.2016 ; зарегистр. 26.05.2016.49. Филипповский, В. А. Система автоматического поиска доказательствтеорем, основанная на специальном варианте обратного метода С. Ю. Маслова:магистерская диссертация. — СПб. : СПбГУ, 2015.50. Чень, Ч. Математическая логика и автоматическое доказательствотеорем / Ч. Чень, Р. Ли ; пер.
с англ. ; под ред. С. Ю. Маслова. — М. : Наука, 1983.— 360 с.51. Шанин, Н. А. Конструктивные вещественные числа и конструктивныефункциональные пространства // Тр. МИАН СССР. — 1962. — Т. 67. — С. 15–294.52. Avigad, J. A formally verified proof of the prime number theorem / J. Avigad[et al.] // ACM Transactions on Computational Logic (TOCL). — 2007. — 9 (1). —Article 2. — P. 1–23.14953. Bachmair, L.
Resolution theorem proving / L. Bachmair, H. Ganzinger //Handbook of Automated Reasoning. — 2001. — Vol. 1. — P. 19–99.54. Barendregt, H. Autarkic Computations in Formal Proofs / H. Barendregt,E. Barendsen // Journal of Automated Reasoning. — 2002. — 28 (3). — P. 321–336.55. Bates, J. L. Proofs as programs / J. L. Bates, R. L. Constable // ACMTransactions of Programming Language Systems. — 1985 — 7 (1). — P.
53–71.56. Baumgartner, P. Hyper Tableau — The Next Generation // AutomatedReasoning with Analytic Tableaux and Related Methods, TABLEAUX’98. LNCS. —1998. — Vol. 1397. — P. 60–76.57. Beth, E. W. Semantic entailment and formal derivability // Med.
Kon.Nederl. Akad. v. Wetensch., Nieuwe Reeks. — 1955. — 18 (13). — P. 309–342.58. Bibel, W. Automated Theorem Proving. — Second edition. — SpringerVieweg, Braunschweig, 1987. — 289 p.59. Bondyfalat, D. An Application of Automatic Theorem Proving in ComputerVision / D. Bondyfalat, B. Mourrain, T.
Papadopoulo // Automated Deduction inGeometry. LNCS. — Springer Berlin Heidelberg, 1999. — Vol. 1669. — P. 207–232.60. Bove, A. A Brief Overview of Agda — A Functional Language withDependent Types / A. Bove, P. Dybjer, U. Norell // Theorem Proving in Higher OrderLogics, TPHOLs 2009. LNCS. — Springer Berlin Heidelberg, 2009. — Vol. 5674. —P. 73–78.61. Brock, B. ACL2 theorems about commercial microprocessors / B.
Brock,M. Kaufmann,J. S. Moore//FormalMethodsinComputer-AidedDesign(FMCAD’96). LNCS. — Springer Berlin Heidelberg, 1996. — Vol. 1166. — P. 275–293.62. CASC 25. Results: Full Summary [Электронный ресурс]. URL:http://www.cs.miami.edu/~tptp/CASC/25/WWWFiles/ResultsSummary.html(датаобращения: 17.09.2017).63. Chaudhuri, K. A logical characterization of forward and backward chainingin the inverse method / K.
Chaudhuri, F. Pfenning, G. Price // Journal of AutomatedReasoning. — 2008. — 40 (2–3). — P. 133–177.15064. Chaudhuri, K. Focusing the inverse method for linear logic / K. Chaudhuri,F. Pfenning // Proceedings of the 14th Annual Conference on Computer Science Logic(CSL’05).
LNCS. — Springer Berlin Heidelberg, 2005. — Vol. 3634. — P. 200–215.65. Constable, R. L. Two Lectures on Constructive Type Theory (OregonProgramming Languages Summer School, 2015) [Электронный ресурс]. URL:https://www.cs.uoregon.edu/research/summerschool/summer15/notes/OPLSS-Short2015-2.pdf (дата обращения: 17.09.2017).66. Curry, H. B. Foundations of mathematical logic. — Second edition. — NewYork : Dover Publications, Inc., 1977.
— 410 p.67. Degtyarev, A. Equality elimination for the inverse method and extensionprocedures / A. Degtyarev, A. Voronkov // Proc. International Joint Conference onArtificial Intelligence (IJCAI). — 1995. — Vol. 1. — P. 342–347.68. Degtyarev, A. The inverse method / A. Degtyarev, A Voronkov // Handbookof Automated Reasoning. — Amsterdam : Elsevier, 2001. — Vol. 1. — P.
179–272.69. Dijkstra, E. W. Algol 60 translation: An Algol 60 translator for the x1 andMaking a translator for Algol 60. — Research Report 35, Mathematisch Centrum,Amsterdam,1961.—Reprintarchivedhttp://www.cs.utexas.edu/users/EWD/MCReps/MR35.PDF(датаatURL:обращения:17.09.2017).70. Donnelly, K. The Inverse Method for the Logic of Bunched Implications /K. Donnelly [et al.] // LPAR 2004. LNAI.
— Springer Berlin Heidelberg, 2005. — Vol.3452. — P. 466–480.71. Egly, U. Intuitionistic proof transformations and their application toconstructive program synthesis / U. Egly, S. Schmitt // Artificial Intelligence andSymbolic Computation, AISC 1998. LNCS. — Springer Berlin Heidelberg, 1998. —Vol. 1476. — P. 132–144.72. Fitting, M.
С. Intuitionistic Logic, Model Theory, and Forcing. — NorthHolland, Amsterdam, 1969. — 191 p.73. Fitting, M. C. Proof Methods for Modal and Intuitionistic Logics. —Springer Netherlands, 1983. — 555 p.15174. Furbach, U.ApplicationsofAutomatedReasoning/U. Furbach,C. Obermaier // KI 2006: Advances in Artificial Intelligence.
LNCS. — Springer BerlinHeidelberg, 2007. — Vol. 4314. — P. 174–187.75. Glivenko, V. I. Sur la Logique de M.Brouwer // Académie Royale deBelgique. Bulletins de la classe de sciences. — 1928. — 5 (14). — P. 225–228.76. Gonthier, G. A Machine-Checked Proof of the Odd Order Theorem /G. Gonthier [et al.] // International Conference on Interactive Theorem Proving, ITP2013. LNCS. — Springer Berlin Heidelberg, 2013.
— Vol. 7998. — P. 163–179.77. Gonthier, G. Formal proof — the Four Colour Theorem // Notices of theAMS. — 2008. — 55 (11). — P. 1382–1393.78. Gordon, M. J. Edinburgh LCF. A Mechanised Logic of Computation /M. J. Gordon, A. J. Milner, Ch. P. Wadsworth. — Springer Berlin Heidelberg, 1979. —159 p.79. Hähnle, R. Tableaux and Related Methods // Handbook of AutomatedReasoning. — 2001.
— Vol. 1. — P. 101–177.80. Hales, T. C. The Jordan curve theorem, formally and informally // TheAmerican Mathematical Monthly. — 2007. — 114 (10). — P. 882–894.81. Haneberg, D. Verification of Mondex electronic purses with KIV: fromtransactions to a security protocol / D. Haneberg [et al.] // Formal Aspects ofComputing. — Springer Berlin Heidelberg, 2008. — 20 (1). — P.
41–59.82. Harrison, J. A short survey of automated reasoning // Proceedings of the 2ndinternational conference on Algebraic biology, AB 2007. LNCS. — Springer BerlinHeidelberg, 2007. — Vol. 4545. — P. 334–349.83. Harrison, J. Formal verification of IA-64 division algorithms // TPHOLs2000. LNCS. — Springer Berlin Heidelberg, 2000. — Vol. 1869. — P. 234–251.84. Harrison, J. Handbook of Practical Logic and Automated Reasoning. —New York : Cambridge University Press, 2009.
— 702 p.85. Heyting, A. Die formalen Regeln der intuitionistischen Logik // Sitzungsber.preuss. Akad. Wiss. — Berlin, 1930. — P. 42–56.15286. Hintikka, J. Form and Content in Quantification Theory // Acta PhilosophicaFennica. — 1955. — No. 8. — P. 7–55.87. Horrocks, I. Knowledge Representation and Reasoning on the SemanticWeb: OWL / I. Horrocks, P. F. Patel-Schneider // Handbook of Semantic WebTechnologies. — Springer Berlin Heidelberg, 2011. — P. 365–398.88. Howard, W. A. The formulae-as-types notion of construction // Essays onCombinatory Logic, Lambda Calculus and Formalism.
— Boston : Academic Press,1980. — P. 479–490.89. ImogenGitHubPageресурс].[ЭлектронныйURL:https://github.com/seanmcl/imogen (дата обращения: 17.09.2017).90. Janicic, P. Automated Reasoning: Some Successes and New Challenges //22nd Central European Conference on Information and Intelligent Systems (CECIIS2011). — Croatia, 2011. — P. 13–22.91. Kapur, D. An Overview of Rewrite Rule Laboratory (RRL) / D. Kapur,H.
Zhang // Journal of Computer and Mathematics with Applications. — 1995. — Vol.29. — P. 91–114.92. Katsiri, E. Model Checking for Sentient Computing: An axiomatic approach/ E. Katsiri, A. Mycroft // The 1st Workshop on Semantics for Mobile Environments(SME’05),May2005[Электронныйресурс].URL:https://www.cl.cam.ac.uk/research/dtg/www/files/publications/public/ek236/satisfiability6.pdf (дата обращения: 17.09.2017).93.
Kaufmann, M. Some Key Research Problems in Automated TheoremProving for Hardware and Software Verification / M. Kaufmann, J. S. Moore // Revistade la Real Academia de Ciencias Exactas, Físicas y Naturales. Serie A: Matemáticas(RACSAM). — 2004. — 98 (1).
— P. 181–195.94. Kornilowicz, A. Formalization of the Jordan Curve Theorem in Mizar //International Congress of Mathematicians, Volume of Abstracts. — 2006. — P. 611.95. Kovács, L. The Inverse Method for Many-Valued Logics / L. Kovács,A. Mantsivoda, A. Voronkov // 12th Mexican International Conference on Artificial153Intelligence MICAI 2013. LNCS.
— Springer Berlin Heidelberg, 2013. — Vol. 8265.— P. 12–23.96. Kunze, F. Towards the Integration of an Intuitionistic First-Order Prover intoCoq // Proceedings of the 1st International Workshop Hammers for Type Theories(HaTT 2016) (arXiv:1606.05948).97.
Leroy, X. Formal certification of a compiler back-end or: programming acompiler with a proof assistant // Proceedings of the 33d ACM SIGPLAN-SIGACTsymposium on Principles of programming languages. — ACM Press, 2006. — P. 42–54.98. Letz, R. Model elimination and connection tableau procedures / R.
Letz,G. Stenz // Handbook of Automated Reasoning. — 2001. — Vol. 2. — P. 2015–2114.99. Lifschitz, V. Knowledge Representation and Classical Logic / V. Lifschitz,L. Morgenstern, D. Plaisted // Handbook of Knowledge Representation. — Elsevier,2008. — P. 3–88.100. Lifschitz, V. What is the inverse method? // Journal of AutomatedReasoning. — 1989. — 5 (1).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
