<< Back to People & Contacts Go to Logic in Informatics Home Page

Alexander Vadimovich Lyaletski



 Alexander Vadimovich Lyaletski
Senior Scientific Researcher, Ph.D.
Chair of Theoretical Cybernetics
Faculty of Cybernetics
Kiev National Taras Shevchenko University
See below:
Short Curriculum Vitae
Scientific Interests
Address
Participation in International Projects
Publications
Proceedings of Conferences and Workshops

SHORT CURRICULUM VITAE:

Title:Senior Scientific Researcher, Candidate of physics and mathematics (Ph.D.) by specialty "Mathematical Cybernetics"

Born:1947, Bishkek (Frunze from 1926 to 1991), Kyrgyzstan

Student:Faculty of Mechanics and Mathematics (1965 - 1969),
Faculty of Cybernetics (1969 - 1970), Kiev State Taras Shevchenko University
Post Graduated Courses by Gluchkov Institute of Cybernetics (1972-1975)

Employment:1970 - 1983: Department of Theory of Digital Automates, Glushkov Institute of Cybernetics (Kiev, Ukraine): Engineer, Junior Scientific Researcher

1883 - by now: Chair of Theoretical Cybernetics, Faculty of Cybernetics, Kiev National Taras Shevchenko University (Kiev, Ukraine): Senior Scientific Researcher


SCIENTIFIC INTERESTS:

  • Automated Reasoning
  • Automated Theorem Proving (ATP)
  • Linguistic Tools for ATP Support
  • Mathematical and Applied Logics

ADDRESS:

Faculty of Cybernetics,
Kiev National Taras Shevchenko University,
2, Glushkov avenue, building 6,
03680 Kiev, Ukraine

phones: +(38 044) 259 05 30 (office)
fax: +(38 044) 259 04 39

e-mails: lav@unicyb.kiev.ua, forlav@mail.ru

PARTICIPATION IN INTERNATIONAL PROJECTS:

  1. Leader of the group fulfilling the current project SAD in accordance with the Evidence Algorithm-2000 Programme (since 1999)
  2. Member of the Intas/RFBR 95-0095 “Automated Deduction and Program Synthesis” (1996-1998)
  3. Leader of the Kiev National University team of the Intas 96-0760 “Rewriting Techniques and Efficient Theorem Proving” (1998-2000)
  4. Leader of the Kiev National University team of the Intas 2000-447 “Weak Arithmetics” (2001-2004)

SELECTED PAPERS:

  • Alexander Lyaletski. Sequent Forms of Herbrand Theorem and their Applications. To be published in the Annals of Mathematics and Artificial Inteligence.
  • Alexander Lyaletski, Alexander Letichevsky, and Oleksandr Kalinovskyy. Literal Trees and Resolution Technique. In: Advances in Soft Computing (Proceedings of the International Conference "Intelligent Information Systems 2005: New Trends in Intelligent Information Processing and Web Mining", Gdansk, Poland), 2005.
  • Alexander Lyaletski, Andrei Paskevich, and Konstantin Verchinine. SAD as a Mathematical Assistant - How Should We Go from Here to There? To be published in the Journal of Applied Logic.
  • Alexander Lyaletski, Andrey Paskevich, and Konstantin Verchinine. Theorem Proving and Proof Verification in the System SAD. In: Lecture Notes in Computer Science (Mathematical Knowledge Management Third International Conference, MKM 2004, Bialowieza, Poland, September 19-21, 2004, Proceedings), No. 3119, ISBN: 3-540-23029-7, pages 236-250, 2004.
  • Alexander Lyaletski. Computer-oriented calculus of sequent trees. In: Lecture Notes in Computer Science (Foundations of Information and Knowledge Systems: Third International Symposium, FoIKS 2004, Wilheminenburg Castle, Austria, February 17-20, 2004, Proceedings), Publisher: Springer-Verlag Heidelberg, v. 2942, ISSN: 0302-9743, ISBN: 3-540-20965-4, pages 213-230, 2004.
  • Alexander Lyaletski. Admissible Substitutions in Classical and Intuitionistic Sequent Logics. In: Intelligent Information Processing and Web Mining (Proceedings of the International IIS: IIPWM'04 Conference held in Zakopane, Poland, May 17-20, 2004), Series: Advances in Soft Computing, XIV, ISBN: 3-540-21331-7 (Klopotek, Mieczyslaw A.; Wierzchon, Slawomir T.; Trojanowski, Krzysztof (Eds.)), Physica/Springer Verlag Heidelberg New York, pages 49-58, 2004.
  • Alexander Lyaletski, Anatoly Doroshenko, Andrei Paskevich, and Konstantin Verchinine. In: Lecture Notes in Informatics (LNI) (ISTA 2004: 3rd International Conference on Information Systems Technology and its Applications, Salt Lake City, Utah, USA July 15-17), Bonner Kollen Verlag, ISSN 1617-5468, pages 205-211, 2004.
  • Alexander Lyaletski. Evidential Paradigm: the Logical Aspect. In: Cybernetics and System Analysis, vol. 39, No. 5, Kluwer Academic Publishers, pages 659-667, 2003.
  • Alexander Lyaletski. Admissible Substitutions in Sequent Calculi. In: International Journal on Information Theories and Applications, Bulgaria, Sofia, vol.10, No 4, pages 388-393, 2003.
  • Alexander Lyaletski. Computer-Oriented Sequent Inferring without Preliminary Skolemization. In: Advances in Soft Computing (Intelligent Information Processing and Web Mining Proceedings of the International IIS: IIPWM'03 Conference held in Zakopane, Poland, June 2-5, 2003. - Klopotek, M. A., Wierzchon, S. T., Trojanowski, K. (Eds.)), pages 373-382, Physica/Springer Verlag, Heidelberg New York, ISBN-3-540-00843-8, pages 373-382, 2003.
  • Alexander Lyaletski, Konstantin Verchinine, Anatoli Degtyarev, and Andrey Paskevich. Peculiarities of Mathematical Texts Processing in the System for Automated Deduction, SAD (in Russian). In: Artificial Intelligence (Proceedings of the 3rd International Conference "Artificial Intelligence", October 2002, Katsiveli, Ukraine), No 4, pages 164-171, 2002.
  • Alexander Lyaletski, Konstantin Verchinine, Anatoli Degtyarev, and Andrey Paskevich. System of Automated Deduction (SAD): Linguistic and Deductive Peculiarities. In M.A. Klopotek, S.T. Wierzchon, and M. Michaliwicz, editors, Advances in Soft Computing: Intelligent Information Systems 2002, pages Physica-Verlag, Springer, pages 413-422, 2002.
  • Anatoli Degtyarev, Alexander Lyaletski, and Marina Morokhovets. On the EA-style integrated processing of self-contained mathematical texts. In: M. Kerber and M. Kohlhase, editors, Symbolic Calculation and Automated Theorem Proving, A K Peters, pages 126-141, 2001.
  • Alexander Lyaletski. On Herbrand Theorem. In: The Bulletin of Symbolic Logic (Proceedings of the European Congress of the Association for Symbolic Logic of the millennium, Logic Colloquium 2000, La Sorbonne, Paris, France, July 23--31, 2000), volume 7, No 1, pages 132-133, March 2001.
  • Anatoli Degtyarev, Alexander Lyaletski, and Marina Morokhovets. On An Approach to Automated Proving of Mathematical Assertions (In Russian). In: Journal of Automation and Information Science, No 4, pages 105-115, 2000.
  • Alexander Lyaletski and Marina Morokhovets. On Linguistic Aspects of Integration of Computer Mathematical Knowledge. In: Electronic Notes in Theoretical Computer Science, volume 23, issue 3, Elsevier Science, pages 165-178, 1999.
  • Anatoli Degtyarev, Yuliya Kapitonova, Alexander Letichevsky, Alexander Lyaletski, and Marina Morokhovets. The Evidence Algorithm and Some Problems of the Presentation and Processing of Computer Mathematical Knowledge (In Russian). In: Cybernetics and System Analysis, No 6, pages 9-17, 1999.
  • Anatoli Degtyarev, Alexander Lyaletski, and Marina Morokhovets. Evidence Algorithm and Sequent Logical Inference Search. In: H. Ganzinger, D. McAllester, and A. Voronkov, editors, Logic for Programming and Automated Reasoning (LPAR'99), Lecture Notes in Computer Science, volume 1705, Springer-Verlag, pages 44-61, September 1999.
  • Alexander Lyaletski. On paramodulation Extensions of the Linear Refutation and of the Model Elimination Method. In: Bulletin of the Kiev University, volume 2, pages 225-235, Kiev State University, 1997.
  • Alexander Lyaletski and Vasiliy Yurchishin. Conjunctive Trees and Refutation Search (In Russian). In: Bulletin of the Kiev University, volume 1, Kiev State University, pages 225-230, 1996.
  • Alexander Lyaletski and Vasiliy Yurchishin. On the Complete Extension of the Input Refutation (In Russian). In: Cybernetics, No 4, pages 128-128, 1990.
  • Pavel Gorshkov, Alexander Lyaletski, Vladimir Frolov, and Vasiliy Yurchishin. Simulation of Robot-Manipulators with Program Control. In: Control Machines and Systems. No 1, pages 107-111, 1989.
  • Pavel Gorshkov, Alexander Lyaletski, Vladimir Frolov, and Vasiliy Yurchishin. On Linguistic Tools for the System of Simulation of Robots with Programmed Control (In Russian). In: Bulletin of the Kiev University, volume 6, Kiev State University, pages 107-109, 1987.
  • Anatoli Degtyarev and Alexander Lyaletski. Logical Inference in the System of Automated Proving, SAD (In Rissian). In: Mathematical Foundations of Artificial Intelligent Systems, , Institute of Cybernetics, Publ., Kiev, pages 3-11, 1981.
  • Alexander Lyaletski. Variant of Herbrand Theorem for Formulas in the Prefix Normal Form (In Russian). In: Cybernetics, No. 1, pages 112-116, 1981.
  • Alexander Lyaletski. On a Procedure of Refutation Search (In Russian). In: Semiotics and Informatics, All-Union Institute of Scientific and Technical Information, Publ., pages 29-32, Moscow, 1979.
  • Anatoli Degtyarev, Alexander Lyaletski, and Alexander Zhezherun. On some Deductive Tools of the System of Mathematical Texts Processing (in Russian). In: Cybernetics, No. 5, pages 105-107, 1978.
  • Alexander Lyaletski and Anatoli Malashonok. A Calculus of C-clauses Based on the Clash-resolution Rule (in Russian). In: Mathematical Questions of Intellectual Machines Theory, pages 3-33, Institute of Cybernetics, Publ., Kiev, 1975.
  • Alexander Lyaletski. On a Calculus of C-clauses (in Russian). In: Mathematical Questions of Intellectual Machines Theory, pages 34-48, Institute of Cybernetics, Publ., Kiev, 1975.

PROCEEDINGS OF SELECTED CONFERENCES AND WORKSHOPS:

  • Boris Konev and Alexander Lyaletski. Tableau Proof Search with Admissible Substitutions. In: Proceedings of the International Workshop on First-Order Theorem Proving, Koblenz, Germany, September 14-17, 2005.
  • Alexander Lyaletski, On Herbrand Theorem for Intutionistic Sequent Logic (in Russian). In: Abstract of the International Conference "Algebra, Logic and Cybernetics" (ALC-2004), in honour of the 75-th anniversary of the birth of A.I. Kokorin Irkutsk, Russia, page 173, August 25-28, 2004.
  • Alexander Lyaletski, Andrei Paskevich, and Konstantin Verchinine, The System SAD: Computer-aided Mathematical Text Processing. In: Artificial Intelligence Studies (Proceedings of the 19th International Conference on Artificial Intelligence (AI'19), Siedlce, Poland, September 21-24, 2004),University of Podlasie Publishers, 2004.
  • Alexander Lyaletski, Konstantin Verchinine, and Andrey Paskevich. On verification tools implemented in the System for Automated Deduction. In: Proceedings of the Second COLOGNET Workshop on Implementation Technology for Computational Logic Systems (ITCLS 2003), Pizza, Italy, September 9, pages 3-14, 2003.
  • Alexander Lyaletski. On Efficient Quantifiers Manipulation in Gentzen's Calculi LK and LJ. In: Absracts of the International Meeting "Second St.Peterburg Days of Logic and Computability" devoted to the centennial of an eminent Russian mathematician Andrey Adreevich Markov (Jr.), St.Petersburg, Russia, August 24-26, 2003.
  • Alexander Lyaletski. Admissible Substitutions in Sequent Calculi. In: Proceeding of the X-th International Conference "Knowledge-Dialogue-Solution" (KDS'2003), Varna (Bulgaria), June 16-26, pages 412-418, 2003.
  • Zainutdin Aselderov, Konstantine Verchinine, Anatoli Degtyarev, Alexander Lyaletski, Andrey Paskevich, and Alexander Pavlov. Linguistic Tools and Deductive Technique of the System for Automated Deduction. In: Proceedings of the 3rd International Workshop on the Implementation of Logics, Tbilisi, Georgia, October 14-18, pages 21-24, 2002.
  • Konstantine Verchinine, Anatoli Degtyarev, Alexander Lyaletski, and Andrey Paskevich. SAD, a System for Automated Deduction: a Current State. In: Preliminary Proceedings of the Workshop on 35 Years of Automating Mathematics, Heriot-Watt University, Edinburgh, Scotland, April, pages 10-13, 2002.
  • Alexander Lyaletski and Andrey Paskevich. Goal-Driven Inference Search in Classical Propositional Logic. In: Proceedings of the 4th International Workshop "STRATEGIES-2001", Siena, Italy, pages 65-74, July 18, 2001.
  • Alexander Lyaletski. About One Specificity of the Inverse Method. In: The page on the Web-site of the Logic Colloquium 2001, Kurt Godel Society, Vienna, Austria, August of 2001.
  • Alexander Lyaletski and Marina Morokhovets. Evidential Paradigm: A Current State. In: Abstracts of the International Conference "Mathematical Challenges of the 21st Century", University of California, Los Angeles, page 81, August 7-12, 2000.
  • Alexander Lyaletski and Marina Morokhovets. On Principles of Proof Search and Construction of Mathematical Knowledge Bases in the Evidence Algorithm. In: CD-ROM with the Proceedings of the 16th International Congress IMACS'2000 on Scientific Computation, Applied Mathematics and Simulation. Lausanne, Switzerland? pages 111-115, August 21- 25, 2000.
  • Alexander Lyaletski and Marina Morokhovets. The EA-style Deductive Processing of Mathematical Texts. In: Proceedings of the International Workshop "Rewriting techniques and Efficient Theorem Proving" (RTETP-2000), pages 54-61, Kyiv, Ukraine, May 2000.
  • Alexander Lyaletski. The Sequential Formalism and Deductive Systems for 1st-order Classical Logic (in Russian). In: Proceedings of the International Conference "Logic and Applications", pages 69-70, Novosibirsk, Russia, May 2000.
  • Alexander Lyaletski and Marina Morokhovets. Automated Theorem Proving and Integrate Mathematical Text Processing. In: Proceedings of the International Conference on Mathematical Logic, Novosibirsk, Russia, pages 95-96, 1999.
  • Yuliya Kapitonova, Alexander Letichevsky, Alexander Lyaletski, and Marina Morokhovets. The Evidence Algorithm '2000 (a Project). In: Proceedings of the 1st International Conference UkrPROG'98, Kiev, Ukraine, pages 68-70, 1998.
  • Alexander Lyaletski. Gentzen calculi and admissible substitutions. In: Actes Preliminaieres, du Symposium Franco-Sovietique "Informatika-91", Grenoble, France, pages 99-111, October 16-19, 1991.
  • Alexander Lyaletski and Vasiliy Yurchishin. The Input Resolution and the Method of Trees Modification (in Russian). In: Abstracts of the 2nd All-Union Conference on Applied Logic, Novosibirsk, USSR, 1988.
  • Alexander Lyaletski and Vasiliy Yurchishin. On a Way of Knowledge Presentation for Solving the Task of Planning Robots Acts (in Russian). In: Proceedings of the IV All-Union Conference "Applications of Mathematical Logic Methods", Tallinn, USSR, pages 94-96, 1986.
  • Alexander Lyaletski. Interactive Proof Search Based on Gentzen-type Calculus (in Russian). In: Proceedings of the VII All-Union Conference "Problems of Theoretical Cybernetics", Irkutsk, USSR, 1985.
  • Alexander Lyaletski. On a Modification of Kanger's Method (in Russian). In: Abstracts of VI All-Union Conference on Mathematical Logic, Tbilisi, USSR, pages 98-99, 1982.
  • Alexander Lyaletski. On a variant of Herbrand Theorem (in Russian). In: Abstracts of V All-Union Conference on Mathematical Logic, Novosibirsk, USSR, page 87, 1979.
  • Alexander Lyaletski and Anatoli Degtyarev. The Evidence Algorithm-78. In: Abstracts and Proceedings of the All-Union Symposium "Artificial Intelligence and Automation of Investigations in Mathematics", Kiev, USSR, pages 56-57, 1978.

<< Back to People & Contacts Go to Logic in Informatics Home Page