Table | Card | RUSMARC | |
Allowed Actions: Read Download (344 Kb) Group: Anonymous Network: Internet |
Annotation
Статья посвящена обратному методу Маслова, который подходит для автоматизации доказательств в различных логических исчислениях: логика высказываний, классическая логика первого порядка, интуиционистская логика, модальные логики и т. д. Приведен обзор основных публикаций по обратному методу, рассмотрено разработанное авторами исчисление обратного метода для интуиционистской логики первого порядка. Предложены адаптированные и оригинальные стратегии оптимизации для этого исчисления. Рассмотрены алгоритм логического вывода в полученном исчислении и разработанная на его основе программа автоматического доказательства теорем WhaleProver.
We discuss the inverse method of automated theorem-proving that was invented by S. Maslov. The inverse method can be applied to various logics: propositional logic, first-order logic, modal logics, intuitionistic logic, etc. In the current article, we present an overview of the key publications on the inverse method, describe in detail an inverse method calculus for first-order intuitionistic logic. We propose adapted as well as original optimizing strategies for the developed calculus. We discuss a proof search algorithm for the proposed calculus and our program implementation named WhaleProver.
Usage statistics
Access count: 859
Last 30 days: 6 Detailed usage statistics |