Cравнение эффективности реализаций алгоритма поиска вывода в секвенциальном исчислении высказываний на языках рефал-5 и Haskell.
Ключевые слова:
автоматическое доказательство теорем, пропозициональная логика, секвенциальное исчисление, рефал-5, Haskell, удобочитаемость программы, временная эффективность программы
Аннотация
В статье предлагаются реализации на языках рефал-5 и Haskell алгоритма поиска вывода в секвенциальном исчислении высказываний. Реализации сравниваются по временной эффективности и удобочитаемости. В приложениях изложены базовые сведения об использованных языках программирования. Данную статью можно рассматривать как ориентирующую программиста при выборе языка программирования для реализации машины вывода в системах автоматического доказательства теорем и других интеллектуальных системах, основанных на логическом выводе.
Литература
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).
Опубликован
2015-12-30
Как цитировать
Григорьев, В. Д. (2015). Cравнение эффективности реализаций алгоритма поиска вывода в секвенциальном исчислении высказываний на языках рефал-5 и Haskell. Компьютерные инструменты в образовании, (6), 19-33. извлечено от http://cte.eltech.ru/ojs/index.php/kio/article/view/1448
Выпуск
Раздел
Информатика
Материал публикуется под лицензией:
