Eefficiency Comparison of Iimplementations of Inference Algorithm for Sequent Propositional Calculus in Refal-5 and Haskell.
Keywords:
automated theorem proving, propositional logic, sequent calculus, Refal-5, Haskell, readability of program, time efficiency of program
Abstract
In this paper author describes implementations of inference algorithm for sequent propositional calculus in Refal-5 and Haskell programming languages. Time efficiency and readability of these implementations are compared. Also, there is a concise description of considered programming languages presented in appendix section. The aim of this paper is to provide the basis of the programming language selection for the implementation of inference engine for artificial intelligence systems, based on logical inference and automated theorem proving tools in particular.
References
1. Банчев Б. Язык Рефал — взгляд со стороны // Практика функционального программирования, 2011. Т. 7, № 1. С. 9–30. URL:http://fprog.ru/2011/issue7/ (дата обращения: 28.11.2015).
2. Гаврилова Т.А., Хорошевский В.Ф. Базы знаний интеллектуальных систем. СПб: Питер, 2000.
3. Герасимов А.С. Курс математической логики и теории вычислимости. СПб: Изд-во «Лема», 2011. С. 284 http://www.mccme.ru/free-books/gerasimov-3ed-mccme.pdf (дата обращения: 28.11.2015).
4. Душкин Р. Модель типизации Хиндли-Милнера и пример её реализации на языке Haskell // Практика функционального программирования, 2010. T. 5, № 6. С. 158–178.http://www.fprog.ru/2010/issue5/ (дата обращения: 28.11.2015).
5. Кормен Т., Лейзерсон Ч., Ривест Р., Штайн К. Алгоритмы: построение и анализ, 2-е издание. М.: «Вильямс», 2005.
6. Косовский Н.К. Элементы математической логики и теория субрекурсивных алгоритмов. Л.: Изд-во Ленинградского универститета, 1981.
7. Косовский Н.К., Косовская Т.М. Полиномиальный тезис Чёрча для рефал-5 функций, нормальных алгоритмов и их обобщений // Компьютерные инструменты в образовании, 2010. № 5.С. 12–21.
8. Турчин В.Ф., Сердобольский В.И. Язык Рефал и его использование для преобразования алгебраических выражений // Кибернетика, 1969. № 3. C. 58–62.
http://pat.keldysh.ru/~roman/doc/Turchin/1969-Turchin_Serdobol’skij--Yazyk_Refal_i_ego_ispol’zovanie_dlya_preobrazovaniya_algebraicheskix_vyrazhenij.pdf (дата обращения: 28.11.2015).
9. Холомьев А. Учебник по Haskell. https://anton-k.github.io/ru-haskell-book/book/home.html.
10. Bridge J. Machine learning and automated theorem proving: Tech. Rep. 792: University of Cambridge, Computer Laboratory, 2010. https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-792.pdf (дата обращения: 28.11.2015).
11. Gentzen G. Untersuchungen uber das logische Schließen. I // Mathematische Zeitschrift, 1935. Bd. 39, ¨ H. 1. S. 176–210. http://dx.doi.org/10.1007/BF01201353 (дата обращения: 28.11.2015).
12. Gentzen G. Untersuchungen uber das logische Schließen. II // Mathematische Zeitschrift, 1935. Bd. 39, ¨ H. 1. S. 405–431. http://dx.doi.org/10.1007/BF01201363 (дата обращения: 28.11.2015).
13. Haskell language home page. https://www.haskell.org/ (дата обращения: 28.11.2015).
14. Hudak P., Hughes J., Peyton Jones S., Wadler P. A History of Haskell: Being Lazy with Class // Proceedings of the Third ACM SIGPLAN Conference on History of Programming Languages. HOPL III. New York, NY, USA: ACM, 2007. P. 12–1–12–55. http://doi.acm.org/10.1145/1238844.1238856 (дата обращения: 28.11.2015).
15. Huff D. Proper. GitHub repository. https://github.com/dillonhuff/Proper (дата обращения: 03.12.2015).
16. Kleene S. C. Mathematical logic. John Willey & Sons, Inc., 1967. Перевод на русский язык: Клини С.К. Математическая логика. М.: «Мир», 1973.
17. Korkut J. WangsAlgorithm. GitHub repository. https://github.com/joom/WangsAlgorithm (дата обращения: 03.12.2015).
18. Lisitsa A. Introduction to Refal. Meeting of the BCS Advanced Programming Specialist Group, 2014. http://www.bcs.org/upload/pdf/intro-to-refal-130314.pdf (дата обращения: 28.11.2015).
19. Turchin V. REFAL-5 Programming Guide & Reference Manual. http://refal.botik.ru/book/html/index.html (дата обращения: 28.11.2015).
2. Гаврилова Т.А., Хорошевский В.Ф. Базы знаний интеллектуальных систем. СПб: Питер, 2000.
3. Герасимов А.С. Курс математической логики и теории вычислимости. СПб: Изд-во «Лема», 2011. С. 284 http://www.mccme.ru/free-books/gerasimov-3ed-mccme.pdf (дата обращения: 28.11.2015).
4. Душкин Р. Модель типизации Хиндли-Милнера и пример её реализации на языке Haskell // Практика функционального программирования, 2010. T. 5, № 6. С. 158–178.http://www.fprog.ru/2010/issue5/ (дата обращения: 28.11.2015).
5. Кормен Т., Лейзерсон Ч., Ривест Р., Штайн К. Алгоритмы: построение и анализ, 2-е издание. М.: «Вильямс», 2005.
6. Косовский Н.К. Элементы математической логики и теория субрекурсивных алгоритмов. Л.: Изд-во Ленинградского универститета, 1981.
7. Косовский Н.К., Косовская Т.М. Полиномиальный тезис Чёрча для рефал-5 функций, нормальных алгоритмов и их обобщений // Компьютерные инструменты в образовании, 2010. № 5.С. 12–21.
8. Турчин В.Ф., Сердобольский В.И. Язык Рефал и его использование для преобразования алгебраических выражений // Кибернетика, 1969. № 3. C. 58–62.
http://pat.keldysh.ru/~roman/doc/Turchin/1969-Turchin_Serdobol’skij--Yazyk_Refal_i_ego_ispol’zovanie_dlya_preobrazovaniya_algebraicheskix_vyrazhenij.pdf (дата обращения: 28.11.2015).
9. Холомьев А. Учебник по Haskell. https://anton-k.github.io/ru-haskell-book/book/home.html.
10. Bridge J. Machine learning and automated theorem proving: Tech. Rep. 792: University of Cambridge, Computer Laboratory, 2010. https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-792.pdf (дата обращения: 28.11.2015).
11. Gentzen G. Untersuchungen uber das logische Schließen. I // Mathematische Zeitschrift, 1935. Bd. 39, ¨ H. 1. S. 176–210. http://dx.doi.org/10.1007/BF01201353 (дата обращения: 28.11.2015).
12. Gentzen G. Untersuchungen uber das logische Schließen. II // Mathematische Zeitschrift, 1935. Bd. 39, ¨ H. 1. S. 405–431. http://dx.doi.org/10.1007/BF01201363 (дата обращения: 28.11.2015).
13. Haskell language home page. https://www.haskell.org/ (дата обращения: 28.11.2015).
14. Hudak P., Hughes J., Peyton Jones S., Wadler P. A History of Haskell: Being Lazy with Class // Proceedings of the Third ACM SIGPLAN Conference on History of Programming Languages. HOPL III. New York, NY, USA: ACM, 2007. P. 12–1–12–55. http://doi.acm.org/10.1145/1238844.1238856 (дата обращения: 28.11.2015).
15. Huff D. Proper. GitHub repository. https://github.com/dillonhuff/Proper (дата обращения: 03.12.2015).
16. Kleene S. C. Mathematical logic. John Willey & Sons, Inc., 1967. Перевод на русский язык: Клини С.К. Математическая логика. М.: «Мир», 1973.
17. Korkut J. WangsAlgorithm. GitHub repository. https://github.com/joom/WangsAlgorithm (дата обращения: 03.12.2015).
18. Lisitsa A. Introduction to Refal. Meeting of the BCS Advanced Programming Specialist Group, 2014. http://www.bcs.org/upload/pdf/intro-to-refal-130314.pdf (дата обращения: 28.11.2015).
19. Turchin V. REFAL-5 Programming Guide & Reference Manual. http://refal.botik.ru/book/html/index.html (дата обращения: 28.11.2015).
Published
2015-12-30
How to Cite
Григорьев, В. Д. (2015). Eefficiency Comparison of Iimplementations of Inference Algorithm for Sequent Propositional Calculus in Refal-5 and Haskell. Computer Tools in Education, (6), 19-33. Retrieved from http://cte.eltech.ru/ojs/index.php/kio/article/view/1448
Issue
Section
Computer science
This work is licensed under a Creative Commons Attribution 4.0 International License.
