Диссертация (1149226), страница 26
Текст из файла (страница 26)
— P. 1–23.101. Loveland, D. W. Mechanical Theorem-Proving by Model Elimination //Journal of the ACM. — 1968. — 15 (2). — P. 236–251.102. Maehara, Sh. Eine Darstellung der intuitionistischen Logik in derklassischen // Nagoya Math. — 1954. — Vol. 7.
— P. 45–64.103. Martin-Löf, P. Constructive mathematics and computer programming //Proceedings of the Sixth International Congress for Logic, Methodology, andPhilosophy of Science. — Amsterdam : North-Holland, 1982. — P. 153–175.104. McCune, W. Prover9andMace4. [Электронный ресурс].URL:https://www.cs.unm.edu/~mccune/mace4/ (дата обращения: 17.09.2017).105. McCune, W. Solution of the Robbins Problem // Journal of AutomatedReasoning. — 1997. — 19 (3). — P.
263–276.106. McLaughlin, S. Efficient Intuitionistic Theorem Proving with the PolarizedInverse Method / S. McLaughlin, F. Pfenning // CADE-22. LNCS. — Springer BerlinHeidelberg, 2009. — Vol. 5663. — P. 230–244.154107. McLaughlin, S. The Focused Constraint Inverse Method for IntuitionisticModal Logics (Draft manuscript, January 2010) [Электронный ресурс] /S. McLaughlin, F. Pfenning. URL: https://www.cs.cmu.edu/~fp/papers/inviml10.pdf(дата обращения: 17.09.2017).108. Mints, G. Decidability of the Class E by Maslov’s Inverse Method // EssaysDedicated to Yuri Gurevich on the Occasion of His 70th Birthday. LNCS.
— SpringerBerlin Heidelberg, 2010. — Vol. 6300. — P. 529–537.109. Mints, G. Resolution strategies for the Intuitionistic Logic // ConstraintProgramming. NATO ASI Series. — Springer Berlin Heidelberg, 1994. — Vol. 131. —P. 289–311.110. Mints, G. Transfer of Sequent Calculus Strategies to Resolution for S4 /G. Mints, V. Orevkov, T. Tammet // Proof Theory of Modal Logic. Applied LogicSeries. — Springer Netherlands, 1996. — Vol. 2. — P. 17–31.111. Оtten, J.
Non-clausal Connection-based Theorem Proving in IntuitionisticFirst-Order Logic // Proceedings of the 2nd International Workshop on AutomatedReasoning in Quantified Non-Classical Logics (ARQNL/IJCAR 2016), CEURWorkshop Proceedings. — 2016. — Vol. 1770. — P. 9–20.112. Otten, J.RestrictingBacktrackinginConnectionCalculi//AICommunications. — IOS Press, 2010. — 23 (2–3). — P. 159–182.113. Owre, S. Formal Verification for Fault-Tolerant Architectures: Prolegomenato the Design of PVS / S.
Owre [et al.] // IEEE Transactions on Software Engineering.— 1995. — 21 (2). — P. 107–125.114. Pavlov, V. Exploring Automated Reasoning in First-Order Logic: Tools,Techniques and Application Areas / V. Pavlov, A. Schukin, T. Cherkasova // 4thInternational Conference Knowledge Engineering and the Semantic Web (KESW2013). Communications in Computer and Information Science (CCIS). — SpringerBerlin Heidelberg, 2013. — Vol. 394. — P. 102–116.115. Pavlov, V.
The Inverse Method and First-Order Logic Theorem Proving /V. Pavlov, V. Pak // Nonlinear Dynamics and Applications. — 2014. — Vol. 20. — P.127–135.155116. Pavlov, V. The Inverse Method Application for Non-Classical Logics /V. Pavlov, V. Pak // Nonlinear Phenomena in Complex Systems. — 2015. — 18 (2). —P. 181–190.117. Pientka, B. Focusing the Inverse Method for LF: A Preliminary Report /B. Pientka, X. Li, F. Pompigne // Electronic Notes in Theoretical Computer Science(ENTCS). — 2008. — Vol.
196. — P. 95–112.118. Priest, G. An Introduction to Non-Classical Logic. — Second edition. —New York : Cambridge University Press, 2008. — 613 p.119. PRL Project Home — Proofs as Programs [Электронный ресурс]. URL:http://www.nuprl.org/ (дата обращения: 17.09.2017).120. Rahli, V. A diversified and correct-by-construction broadcast service /V.
Rahli [et al.] // The 2nd International Workshop on Rigorous Protocol Engineering(WRiPE), Austin, TX. — IEEE, 2012. — P. 1–6.121. Raths, T. The ILTP Library: Benchmarking Theorem Provers forIntuitionistic Logic / T. Raths, J. Otten, C. Kreitz // Automated Reasoning with AnalyticTableaux and Related Methods, TABLEAUX 2005. LNAI. — Springer BerlinHeidelberg, 2005. — Vol. 3702.
— P. 333–337.122. Riazanov, A. The design and implementation of VAMPIRE / A. Riazanov,A. Voronkov // AI Communications. — CASC. — Amsterdam : IOS Press, 2002. —15 (2–3). — P. 91–110.123. Robinson, J. A. A Machine-Oriented Logic Based on the ResolutionPrinciple // Communications of the ACM. — 1965. — Vol. 5. — P. 23–41.124. Sahlin, D. An Intuitionistic Predicate Logic Theorem Prover / D. Sahlin,T. Franzen, S. Haridi // Journal of Logic and Computation. — 1992. — 2 (5). — P.619–656.125.
Schellhorn, D. The WAM Case Study: Verifying Compiler Correctness forProlog with KIV / D. Schellhorn, W. Ahrendt // Automated Deduction — A Basis forApplications. Applied Logic Series. — Springer Netherlands, 1998. — Vol. 10. — P.165–194.156126. Schiper, N. Developing correctly replicated databases using formal tools /N. Schiper [et al.] // DSN’14: Proceedings of the 44th Annual IEEE/IFIP InternationalConference on Dependable Systems and Networks.
— IEEE, 2014. — P. 395–406.127. Schmitt, S. JProver: Integrating Connection-Based Theorem Proving intoInteractive Proof Assistants / S. Schmitt [et al.] // First International Joint Conference,IJCAR 2001. LNCS. — Springer Berlin Heidelberg, 2001. — Vol. 2083. — P. 421–426.128. Schulz, S. E: A Brainiac Theorem Prover // Journal of AI Communications.— 2002. — 15 (2/3). — P. 111–126.129. Schulz, S.
System Description: E 1.8 // Proceedings of the 19th LPAR.LNCS. — Springer Berlin Heidelberg, 2013. — Vol. 8312. — P. 477–483.130. Shao, Zh. Certified software // Communications of the ACM. — 2010. —Vol. 53. — P. 56–66.131. Smith, D. R. Toward Practical Applications of Software Synthesis /D. R. Smith, C. Green // Proceedings of FMSP’96, The First Workshop on FormalMethods in Software Practice. — San Diego, CA, 1996. — P. 31–39.132. Smullyan, R.
M. First-Order Logic. — Second corrected edition (firstpublished by Springer-Verlag, NY, 1968). — New York : Courier Dover Publications,1995. — 165 p.133. Srivas, M. K. Applying formal verification to the AAMP5 microprocessor:A case study in the industrial use of formal methods / M. K. Srivas, S. P. Miller //Formal Methods in System Design. —1996. — 8 (2).
— P. 153–188.134. Stump, A. Programming with Proofs: Language-Based Approaches toTotally Correct Software // Verified Software: Theories, Tools, Experiments (VSTTE2005). LNCS. — Springer Berlin Heidelberg, 2008. — Vol. 4171. — P. 502–509.135.
Sutcliffe, G. Automated theorem proving: theory and practice // AIMagazine. — 2002. — 23 (1). — P. 121–122.136. Sutcliffe, G. Evaluating general purpose automated theorem provingsystems / G. Sutcliffe, C. Suttner // Artificial Intelligence. — 2001. — 131 (1–2). — P.39–54.157137. Sutcliffe, G. TPTP Problem Library and Associated Infrastructure: The FOFand CNF Parts, v3.5.0 // Journal of Automated Reasoning. — 2009. — 43 (4).
— P.337–362.138. Szekeres, G. Computer solution to the 17-point Erdős-Szekeres problem /G. Szekeres, L. Peters // ANZIAM Journal. — 2006. — 48 (2). — P. 151–164.139. Tammet, T. A resolution theorem prover for intuitionistic logic // CADE13. LNCS (LNAI). — Springer Berlin Heidelberg, 1996. — Vol.
1104. — P. 2–16.140. Tammet, T. Using Resolution for Deciding Solvable Classes and BuildingFinite Models // Proceedings of Baltic Computer Science, Selected Papers. LNCS. —Springer Berlin Heidelberg, 1991. — Vol. 502. — P. 33–64.141. TheAgdaWiki[Электронныйресурс].URL:http://wiki.portal.chalmers.se/agda/pmwiki.php (дата обращения: 17.09.2017).142. The Coq Proof Assistant [Электронный ресурс]. URL: https://coq.inria.fr/(дата обращения: 17.09.2017).143.
TheETheoremProver[Электронныйресурс].URL:http://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html (дата обращения: 17.09.2017).144. The ILTP Library. Benchmarking Theorem Provers for Intuitionistic Logic[Электронный ресурс]. URL: http://iltp.de/index.html (дата обращения: 17.09.2017).145. The TPTP Problem Library for Automated Theorem Proving[Электронный ресурс].
URL: http://www.cs.miami.edu/~tptp/ (дата обращения:17.09.2017).146. Tiberghien, T.SemanticReasoninginContext-AwareAssistiveEnvironments to Support Ageing with Dementia / T. Tiberghien [et al.] // The SemanticWeb — ISWC 2012. LNCS.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
