← Publications

[1]

Bobot, F., and Paskevich, A. Expressing polymorphic types in a many-sorted language. In FroCoS 2011, 8th International Symposium on Frontiers of Combining Systems (Saarbrücken, Germany, Oct. 2011), C. Tinelli and V. Sofronie-Stokkermans, Eds., vol. 6989 of Lecture Notes in Computer Science, Springer, pp. 87-102. [ bib | .pdf | Abstract ]

[2]

Bobot, F., and Paskevich, A. Expressing polymorphic types in a many-sorted language, July 2011. Extended report. [ bib | http | .pdf | Abstract ]

[3]

Bobot, F., Filliâtre, J.-C., Marché, C., and Paskevich, A. Why3: Shepherd your herd of provers. In Boogie 2011, First International Workshop on Intermediate Verification Languages (Wrocław, Poland, Aug. 2011), pp. 53-64. [ bib | .pdf | Abstract ]

[4]

Contejean, É., Courtieu, P., Forest, J., Paskevich, A., Pons, O., and Urbain, X. A3PAT, an approach for certified automated termination proofs. In PEPM'10, Proceedings of the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (Madrid, Spain, Jan. 2010), ACM, pp. 63-72. [ bib | DOI | .pdf | Abstract ]

[5]

Verchinine, K., Lyaletski, A., Paskevich, A., and Anisimov, A. On correctness of mathematical texts from a logical and practical point of view. In Intelligent Computer Mathematics, AISC/Calculemus/MKM 2008 (Birmingham, United Kingdom, July 2008), S. Autexier, J. Campbell, J. Rubio, V. Sorge, M. Suzuki, and F. Wiedijk, Eds., vol. 5144 of Lecture Notes in Computer Science, Springer, pp. 583-598. [ bib | .pdf | Abstract ]

[6]

Paskevich, A. Connection tableaux with lazy paramodulation. Journal of Automated Reasoning 40, 2-3 (2008), 179-194. [ bib | .pdf | Abstract ]

[7]

Paskevych, A. Méthodes de formalisation des connaissances et des raisonnements mathématiques: aspects appliqués et théoriques. PhD thesis, Université Paris 12, 2007. In French. [ bib | .pdf | Abstract ]

[8]

Paskevich, A., Verchinine, K., Lyaletski, A., and Anisimov, A. Reasoning inside a formula and ontological correctness of a formal mathematical text. In Calculemus/MKM 2007 - Work in Progress (Hagenberg, Austria, June 2007), M. Kauers, M. Kerber, R. Miner, and W. Windsteiger, Eds., no. 07-06 in RISC-Linz Report Series, University of Linz, Austria, pp. 77-91. [ bib | .pdf | Abstract ]

[9]

Verchinine, K., Lyaletski, A., and Paskevich, A. System for Automated Deduction (SAD): a tool for proof verification. In Automated Deduction, 21st International Conference, CADE-21 (Bremen, Germany, July 2007), F. Pfenning, Ed., vol. 4603 of Lecture Notes in Computer Science, Springer, pp. 398-403. [ bib | .pdf | Abstract ]

[10]

Paskevich, A. Connection tableaux with lazy paramodulation. In Automated Reasoning, 3rd International Joint Conference, IJCAR 2006 (Seattle WA, USA, Aug. 2006), U. Furbach and N. Shankar, Eds., vol. 4130 of Lecture Notes in Computer Science, Springer, pp. 112-124. [ bib | .pdf | Abstract ]

[11]

Lyaletski, A., Paskevich, A., and Verchinine, K. SAD as a mathematical assistant - how should we go from here to there? Journal of Applied Logic 4, 4 (2006), 560-591. [ bib | .ps.gz | Abstract ]

[12]

Paskevych, A. Methods of formalization of mathematical knowledge and reasoning: theoretical and practical aspects. PhD thesis, Kiev National Taras Shevchenko University, 2005. In Ukrainian. [ bib | .pdf ]

[13]

Lyaletski, A., Verchinine, K., and Paskevich, A. Theorem proving and proof verification in the system SAD. In Mathematical Knowledge Management, 3rd International Conference, MKM 2004 (Bialowieza, Poland, Sept. 2004), A. Asperti, G. Bancerek, and A. Trybulec, Eds., vol. 3119 of Lecture Notes in Computer Science, Springer, pp. 236-250. [ bib | .ps.gz | Abstract ]

[14]

Lyaletski, A. V., Doroshenko, A. E., Paskevich, A., and Verchinine, K. Evidential paradigm and intelligent mathematical text processing. In Information Systems Technology and its Applications, 3rd International Conference, ISTA 2004 (Salt Lake City UT, USA, July 2004), A. E. Doroshenko, T. A. Halpin, S. W. Liddle, and H. C. Mayr, Eds., vol. 48 of Lecture Notes in Informatics, GI, pp. 205-211. [ bib | .pdf | Abstract ]

[15]

Lyaletski, A., Verchinine, K., and Paskevich, A. On verification tools implemented in the System for Automated Deduction. In Implementation Technology for Computational Logic Systems, 2nd CoLogNet Workshop, ITCLS 2003 (Pisa, Italy, Sept. 2003), pp. 3-14. [ bib | .ps.gz | Abstract ]

[16]

Verchinine, K., Lyaletski, A., and Paskevich, A. Applying the System for Automated Deduction to mathematical text verification. International Journal “Iskustvennyj Intellekt” 3 (2003), 57-69. In Russian. [ bib | .pdf | Abstract ]

[17]

Aselderov, Z., Verchinine, K., Lyaletski, A., Paskevich, A., Klimenko, V., and Fishman, Yu. Deductive, inductive, and analytic methods of presentation and processing of computer knowledge in the intellectual systems (1. Deductive methods and tools). “Matematychni mashyny i systemy” (3,4) (2003), 51-74. In Ukrainian. [ bib ]

[18]

Paskevich, A. A notion of local truth and its applications in automated theorem proving. Bulletin of the University of Kiev (physics and mathematics series) 1 (2003), 199-203. In Ukrainian. [ bib | .ps.gz | Abstract ]

[19]

Verchinine, K., Degtyarev, A., Morokhovets, M., Lyaletski, A., and Paskevich, A. Evidence Algorithm and processing of formalized mathematical texts. International Journal “Problemy upravleniya i informatiki” 5 (2002), 80-95. In Russian. [ bib ]

[20]

Aselderov, Z., Verchinine, K., Degtyarev, A., Lyaletski, A., Paskevich, A., and Pavlov, A. Linguistic tools and deductive technique of the System for Automated Deduction. In Implementation of Logics, 3rd International Workshop, WIL 2002 (Tbilisi, Georgia, Oct. 2002), pp. 21-24. [ bib | .ps.gz | Abstract ]

[21]

Lyaletski, A., Verchinine, K., Degtyarev, A., and Paskevich, A. System for Automated Deduction (SAD): Linguistic and deductive peculiarities. In Intelligent Information Systems, 11th International Symposium, IIS 2002 (Sopot, Poland, June 2002), M. A. Klopotek, S. T. Wierzchon, and M. Michalewicz, Eds., Advances in Soft Computing, Physica-Verlag, pp. 413-422. [ bib | .ps.gz | Abstract ]

[22]

Aselderov, Z., Verchinine, K., Degtyarev, A., Lyaletski, A., and Paskevich, A. Peculiarities of mathematical text processing in the System for Automated Deduction (SAD). International Journal “Iskustvennyj Intellekt” 4 (2002), 163-171. In Russian. [ bib | .pdf | Abstract ]

[23]

Lyaletski, A., and Paskevich, A. Goal-driven inference search in classical propositional logic. In Proc. International Workshop STRATEGIES'2001 (Siena, Italy, June 2001), pp. 65-74. [ bib | .ps.gz | Abstract ]

[24]

Lyaletski, A., and Paskevich, A. On some strategies of logical inference search that are driven by goals. Bulletin of the University of Kiev (physics and mathematics series) 2 (2001), 277-285. In Ukrainian. [ bib | .ps.gz | Abstract ]

[25]

Vershinin, K., and Paskevich, A. ForTheL - the language of formal theories. International Journal of Information Theories and Applications 7, 3 (2000), 120-126. [ bib | .ps.gz | Abstract ]

[26]

Paskevich, A. Peculiarities of the implementation of a high-level language for processing of mathematical texts. Bulletin of the University of Kiev (physics and mathematics series) 2 (1999), 284-288. In Ukrainian. [ bib | .ps.gz | Abstract ]