Алгоритм поиска натурального вывода для интуиционистской логики высказываний тема диссертации и автореферата по ВАК РФ 09.00.07, кандидат философских наук Макаров, Валентин Валентинович

• Макаров, Валентин Валентинович
• кандидат философских наук
• 2002

Оглавление диссертации кандидат философских наук Макаров, Валентин Валентинович

Введение. Общая характеристика работы.

Глава 1. Исторические предпосылки.

§1.1. Предыстория создания формальных систем и исчислений.,

§1.2. Предыстория создания вычислительных машин.

§1.3. Первые системы автоматического вывода.

§1.4. Тематическая структура.

Глава 2. Секвенциальные системы генерирования доказательств теорем для интуиционистской логики.

§2.1. Секвенциальные исчисления.

§ 2.2. Префиксные исчисления.

Глава 3. Поиск доказательств теорем в натуральном исчислении.

§3.1. Поиск вывода в классической логике высказываний.

§ 3.2. Поиск вывода в интуиционистской логике высказываний.

Глава 4. Алгоритм поиска доказательств теорем интуиционистской пропозициональной логики

§4.1. Натуральное исчисление MNJ.

§ 4.2. Алгоритм поиска вывода.

§ 4.3. Адекватность алгоритма.

Введение диссертации (часть автореферата) на тему «Алгоритм поиска натурального вывода для интуиционистской логики высказываний»

Актуальность темы. На современном этапе развития человечества с особой остротой встал вопрос о передаче части мыслительных действий человека машине, что отразилось в возникновении новой сферы исследований -исследований в области искусственного интеллекта. Одним из многих направлений этой бурно развивающейся отрасли является автоматический поиск доказательств в некоторой формальной системе.

Задачи, связанные с нахождением доказательства некоторого утверждения, а следовательно, с разрешимостью формальной системы интересовали человечество и ранее. Однако само понятие автоматического поиска доказательств заставило по-новому рассматривать данные задачи и, в конечном счете, определило один из критериев оценки исчислений. А именно, выбор между исчислениями, реализующими одну и ту же логику, производится на основе наименьшей сложности вычислений, которые необходимо произвести для установления общезначимости (доказательства) утверждения. Поэтому, становится важным построение таких исчислений, которые обладают не только разрешимостью и достаточной выразимостью, но и приемлемой для практических целей сложностью. Другой проблемой, довольно тесно связанной с первой, считается задача представления данных в понятной для человека форме, одним из путей решения которой является моделирование самой человеческой деятельности машиной.

Разработки в области автоматического поиска доказательств проводятся в целом ряде крупных мировых научно-исследовательских центров, таких как, например: Argonne National Laboratory, США (программа "Otter", основанная на теории резолюций), University of Cambridge (программа автоматической дедукции Isabelle), Carnegie Mellon University (автоматическое доказательство теорем для логики высоких порядков), КАКЕШ Laboratory, WASEDA University, Япония (программа автоматического доказательства для секвенциального исчисления) и др. Как было отмечено в ряде работ1, эти процедуры

1 Болотов А.Е., Бочаров В.А., Горчаков А,Е. Алгоритмы поиска вывода в классической пропозициональной логике. // Труды научно-исследовательского семинара логического центра Института философии РАН. М., 1996.

Болотов А.Е., Бочаров В.А., Горчаков А.Е. Алгоритм поиска вывода для натурального классического исчисления высказываний. // Логические Исследования, вып. 3, М., 1995. 4 автоматического поиска доказательств обычно строятся либо на базе секвенциальных исчислений и теории резолюций, либо на некотором аппарате, который в той или иной мере близок к этим представлениям логики. Однако во всех таких приемах процедура выведения одних положений из других или вообще не представлена в явном виде, или осуществляется в таком виде, который весьма далек от того, что понималось под выводом в истории логики2. И секвенции, и метод резолюций - это скорее алгоритмы проверки общезначимости утверждений, чем вывод. Все они строятся на основе чисто аналитических процедур, в то время как традиционное понятие вывода представляет собой метод синтеза доказуемого утверждения из имеющихся посылок. Концентрация внимания исследователей в области автоматического поиска доказательств на этих популярных дедуктивных методах не случайна и обусловлена, в первую очередь, практическими соображениями3. Так, исследования в области теории резолюций тесно связаны с языками логического программирования (в частности, типа Пролог), где выводы основаны на методе резолюций, который изначально являлся как бы составной частью Пролога4. Другие области, диктующие необходимость совершенствования методов автоматического доказательств, - это компьютерная алгебра, а также некоторые аспекты тестирования программ5.

Наиболее же приближенными к естественным человеческим рассуждениям являются на данный момент натуральные исчисления. Однако создание и реализация на их основе алгоритмов автоматического поиска доказательств до сих пор является мало разработанной областью. Оригинальной работой в этом направлении стало создание алгоритма поиска доказательств теорем для классической логики Болотовым А.Е., Бочаровым В.А. и Горчаковым А.Е. Разработка автоматической процедуры для неклассических логик, в том числе и для интуиционистской логики, работающей в натуральном исчислении, до сих пор не реализована и, таким образом, имеет научную ценность.

Бочаров В.А., Болотов А.Е., Горчаков А.Е., Шангин В.О. Алгорифм поиска вывода в классической пропозициональной логике, (не опубликовано)

2 Бочаров В.А., Маркин В. И. Основы логики. М., 1994.

3 Jansen G. Hardware Verification using Temporal Logic: A Practical View // Formal VLSI Correctness Verifiation, VLSI Design Methods-П. Elsevier Science Publishers, 1990.

4 Братко И. Программирование на языке Пролог для искусственного интеллекта. Пер. с англ. Лупенко А.И., Степанова А.М., под ред. Степанова А.М. М., 1990.

5 Baain D., Klarlund N. Hardware Verification using Monadic Second-Order Logic // BRICS Technical Report Series, RS-95-7.1995. 5

Основанием актуальности работы в неклассических логиках является факт достаточно успешного практического применения неклассических логик в рамках различных проектов тестирования аппаратных средств (hardware verification)6, нередко спонсирующихся ведущими производителями таких средств (например, Intel). Здесь самыми распространенными и эффективными на сегодняшний день являются методы тестирования моделей (model checking)7, где для описания моделей hardware используется тот или иной дедуктивный аппарат, чаще всего основанный на модальной или временной логиках8.

В свете вышеизложенного, интересно следующее направление современных исследований в области автоматического поиска доказательств. Речь идет о попытке симбиоза различных методов, включая теорию резолюций, секвенциальные исчисления, элементы натурального вывода и другие. Это частично характерно для центра исследований Otter, но наиболее четко проявляется в подходе группы по разработке проекта Isabelle (University of Cambridge)9, где авторы прямо заявляют о такой стратегии симбиоза. Как отмечается, этот подход является, во-первых, достаточно обоснованным (в силу специфик и ограниченности каждого из методов дедукции) и, во-вторых, многообещающим (учитывая не только теоретические моменты, но и практические возможности применения техники параллельных процессоров). В этой связи предпринятое в данной диссертационной работе направление исследований приобретает дополнительную значимость.

Степень разработанности проблемы. Несмотря на то, что первую разрешающую процедуру для интуиционистской логики предложил еще Генцен Г., попытки построения более эффективного алгоритма не прекращаются до сих пор. Вопросами построения удобного для автоматического поиска доказательств исчисления для интуиционистской логики занимались Корн Д., Ваалер А., Дикхоф Р., Вайх К., Салин Д. и другие. Их исследования привели к нахождению способов устранения процедуры

6 Bochmann G. Hardware Specification with Temporal Logic: An Example // ШЕЕ Transactions on Computers, Vol.C-31. № 3.1982.

7 Pnueli A. Now you can compose temporal logic specifications // Proceedings of the 16-th ACM Symposium on Theory of Computing, 1984.

8 Bolotov A., Fisher M. A Resolution Method for Computation Tree Branching Time Temporal Logic // IV International Workshop on Temporal Representation and Reasoning (TIME'97). Published by the IEEE. Florida, 1997.

Davis M. and Putnam H. A Computing Procedure for Quantification Theoiy // JACN 7(3), 1960.

9 Izabelle. User's guide. University of Cambridge, 1996. 6 поиска циклов, которая обычно детерминируется наличием структурного правила сокращения. Однако, общей для них трудностью оказалась проблема устранения перебора различных стратегий поиска вывода, когда в зависимости от порядка применения правил вывода следует успешное или неудачное его построение. Более подробное описание их результатов приводится во второй главе данного диссертационного исследования.

В отечественной литературе можно отметить работы Воробьева Н.Н., Шанина Н.А., Смирнова В.А., Непейводы Н.Н. и других.

Научная новизна исследования. Как было отмечено, создание и реализация на основе натурального исчисления алгоритмов автоматического поиска доказательств до сих пор является мало разработанной областью. Недостаток внимания, уделяемого натуральному выводу в области автоматического доказательств, обусловлен некоторым скептицизмом, порожденным именно фактом специфики этого метода доказательства как синтетической процедуры. Наличие правил введения логических связок рассматривается как камень преткновения на пути автоматизации натурального вывода.

Заметное влияние на такое отношение к натуральным исчислениям оказала также тесная их связь с секвенциальными исчисления. Так, Бибель В.10 определяет для натуральных исчислений лишь роль переводчика аналитически найденного доказательства в удобную для пользователя форму и возможного источника идей по улучшению аналитических процедур. (Характерно, что в англоязычной литературе часто под термином "natural deduction systems" полагаются не системы натурального вывода в нашем понимании, а как раз те или иные варианты секвенциального представления логики.) В представленной диссертационной работе замечание Бибеля В. отчасти подтвердилось тем, что работу алгоритма, разработанного Болотовым А.Е., Бочаровым В.А. и Горчаковым А.Е., возможно описать односукцедентным секвенциальным исчислением. Однако в доказательстве, построенном таким алгоритмом, используются более традиционные правила, чем это имеет место в этом секвенциальном исчислении. Построение процедуры автоматического

10 W. Bibel. Deduktion: Automatisierung der Logik. Miinchen, Wien, Oldenburg, 1992. S. 107. 7 доказательства в натуральном исчислении для иных логическим систем, в том числе и для интуиционистской логики, оставалось открытым.

В интуиционистских секвенциальных исчислениях значительно увеличиваются трудности алгоритмизации поиска доказательств по сравнению с классической логикой. Так, например, появляется зацикливание поиска вывода, возникает большое количество несущественных вхождений формул в выводе, которые могут однако помешать построению доказательства, и прочее. Выявление путей создания алгоритма поиска доказательств для интуиционистской логики в натуральном исчислении, лишенного подобных негативных свойств, представляет собой научную новизну данного исследования.

Цель и задачи исследования. Основная цель диссертационного исследования заключается в том, чтобы разработать и обосновать решение проблемы построения алгоритма поиска доказательств теорем для интуиционистской логики высказываний в натуральном исчислении, т.е. решить следующие задачи:

- построить удобное для такой цели натуральное исчисление,

- построить алгоритм поиска доказательств для данного натурального исчисления,

- доказать непротиворечивость, полноту и конечность алгоритма,

- осуществить компьютерную реализацию данного алгоритма.

Методологической основой исследования является аппарат современной логики и компьютерных наук. Автор опирается на современные данные, относящиеся к интуиционистской логике.

Основные положения, выносимые на защиту:

- на основе анализа существующих методов поиска доказательств теорем для интуиционистской логики высказываний было показано, что имеется ряд методов, позволяющих оптимизировать поиск доказательства в интуиционистской логике: использование префиксов для фиксации информации семантического характера, для чего вводятся новые объекты языка логики; введение новых правил вывода, которые применяются на основе более глубокого исследования структуры формулы, а не только на основе ее главного знака; 8

- через объединение этих методов построено секвенциальное префиксное многосукцедентное интуиционистское исчисление MLJ+, в котором процедура поиска вывода свободна от перебора стратегий и зацикливаний; сложность вычислений в этом исчислении определяется процедурой унификации префиксов, как О

Г22п\

4п

- построено секвенциальное префиксное односукцедентное исчисление MLJ++, являющимся консервативным расширением MLJ+, и на его основе был создан алгоритм поиска доказательств, который состоит из двух этапов работы: построение макета вывода, в котором используются переменные по префиксам формул, и проведение процедур унификации и минимизации, в результате чего элиминируются все переменные по префиксам;

- сформулировано содержащееся в алгоритме исчисление натурального вывода, являющееся консервативным расширением интуиционистской логики и характеризующееся разнообразием непрямых правил вывода «от противного», в которых фиксируется различные случаи наличия противоречия между формулами вывода;

- предложен новый вариант односукцедентного классического секвенциального исчисления высказываний, отличающийся от известных ранее исчислений этого типа;

- осуществлена предварительная компьютеризация процедур поиска доказательств в интуиционистском натуральном исчислении на языке программирования СИ, которая позволила отработать эти процедуры и алгоритм поиска вывода в целом; в дальнейшем предстоит полностью реализовать данный алгоритм на вычислительных машинах.

Практическая значимость исследования. Результаты исследования могут быть использованы в дальнейших разработках алгоритмов, как для интуиционистской логики предикатов, так и для иных логик; они могут быть использованы также в научно-исследовательской работе как инструмент для проверки утверждений интуиционистской логики. Большое значение имеют полученные результаты и в педагогической практике при чтении курсов по интуиционистской логике и компьютеристике. 9

Апробация работы состоялась в ходе обсуждения результатов исследования на кафедре логики философского факультета МГУ им. М.В. Ломоносова. Результаты диссертационного исследования нашли также свое отражение в 4 научных работах автора и обсуждались на 5-ой Общероссийской научной конференции «Современная логика: проблемы теории, истории и применения в науке» (СПб, 1998), 3-их Смирновских чтениях по логике (Москва, 2001) и на философском факультете университета Росток, Германия.

Структура диссертации. Диссертация состоит из введения, 4 глав, заключения, приложения и библиографии.

Заключение диссертации по теме «Логика», Макаров, Валентин Валентинович

Заключение

В диссертационной работе исследованы различные средства префиксных и секвенциальных исчислений, построенных к настоящему моменту, с точки зрения их эффективности для автоматического поиска вывода. На основе этого анализа было построено исчисление MLJ+, которое обладает более лучшими характеристиками для автоматического поиска вывода, чем проанализированные исчисления. Оно лишено таких серьезных недостатков, как поиск циклов и перебор различных стратегий применений правил вывода. Поиск вывода в исчислении MLJ+ разбивается на два этапа: построение макета вывода согласно правилам исчисления и унификация префиксов макета вывода. Унификация является основной по сложности операцией поиска вывода и составляет О ггп\

4п

В диссертации проанализирован алгоритм поиска натурального вывода для классической логики высказываний: сформулированы правила алгоритма в виде секвенциального исчисления LK+, для которого характерны отсутствие структурных правил и односукцедентность секвенций, и доказано соответствие построения вывода в этом исчислении работе алгоритма.

На основе выявленных характеристик секвенциального исчисления LK+ для классической логики построено исчисление MLJ++ для последующего создания алгоритма поиска натурального вывода для интуиционистской логики высказываний. Исчисление MLJ++ оказалось консервативным расширение интуиционистской логики, причиной чего является введение в язык связки «~», позволившей достичь односукцедентность секвенций исчисления MLJ++.

По исчислению MLJ++ сформулирован алгоритм поиска натурального вывода и построено натуральное исчисление MNJ, в котором строится вывод. Исчисление MNJ является консервативным расширением интуиционистской логики высказываний, что доказывается обоснованием правил MNJ через правила исчисления MLJ++. Отличительной чертой исчисления MNJ, помимо использования префиксов, является наличие четырех правил «от противного», фиксирующих различные случаи наличия противоречия между формулами.

Автором осуществлена предварительная компьютеризация процедур алгоритма поиска доказательства в интуиционистском натуральном исчислении на языке программирования СИ, которая позволила отработать эти процедуры и

102 алгоритм поиска вывода в целом; в дальнейшем предстоит полностью реализовать данный алгоритм на вычислительных машинах.

Возможные направления дальнейших исследований состоят в следующем:

1. в разработке версии алгоритма, дающего более приближенный к естественным рассуждениям вывод, т.е. без префиксов и дополнительных связок,

2. в создании подобного алгоритма поиска вьшода для интуиционистской логики предикатов и других логик,

3. в исследования вопроса о взаимоотношении алгоритмических свойств логики и принимаемых в ней структурных правил.

103

Список литературы диссертационного исследования кандидат философских наук Макаров, Валентин Валентинович, 2002 год

1. Baain D., Klarlund N. Hardware Verification using Monadic Second-Order Logic // BR1.S Technical Report Series, RS-95-7. 1995.

2. Bibel W. Deduktion: Automatisierung der Logik. Miinchen, Wien, Oldenburg, 1992.

3. Bochenski J.M. Formale Logik.- Freiburg im Breisgau., Munchen: Alber, 1978.

4. Bochmann G. Hardware Specification with Temporal Logic: An Example // IEEE Transactions on Computers, Vol.C-31. № 3. 1982.

5. Bole L., Borowik P. Many-valued logics: Theoretical foundations. Vol. 1. Berlin, 1992.

6. Bolotov A., Fisher M. A Resolution Method for Computation Tree Branching Time Temporal Logic // IV International Workshop on Temporal Representation and Reasoning (TIME'97). Published by the IEEE. Florida, 1997.

7. Davis M., Putnam H. A Computing Procedure for Quantification Theory // JACN 7(3), 1960.

8. Deduktionssysteme: Automatisierung des logischen Denkens / hrsg. von Blasius K.H. und Burckert H.-J. Mit Beitr. von Blasius K.H. 2. Munchen; Wien: Oldenbourg, 1992.

9. Dyckhoff R. Contraction-free Sequent Calculi for Intuitionistic Logic. Journal of Symbolic Logic 57(3), pp. 795-807,1992

10. Dyckhoff R., Pinto L. A Permutation-free Sequent Calculus for Intuitionistic Logic; unpublished

11. Fitch F. Symbolic Logic. N.Y. 1952.

12. Fitting M. Intuitionistic Logic Model Theory and Forcing // Studies in Logic and the Foundations of Mathematics / North Holland publishing company Amsterdam. London, 1969.

13. Fitting M. Proof methods for modal and intuitionistic logics. Synthese Library. Vol. 169. Dortrecht, D. Reidel Publishing Company, 1983.

14. Frege G. Uber den Zweck der Begriffsschrift, 1882. // Frege Gottlob. Begriffsschrift. G. Olms. Verlagsbuchhandlung, Hildesheim, 1964.

15. Heyting A. Intuitionism. Amsterdam, 1956. Русский перевод: Гейтинг A. Интуиционизм.- M.: "Мир", 1965.109

16. Hudelmaier J. A PROLOG program for intuitionistic logic/ SNS-Bericht 88-28, Universitat Tubingen, 1988.

17. Hudelmaier J. An 0(n log n)-space decision procedure for intuitionistic propositional logic and Kuroda logic. Rapporto interno 99-93, Dipartimento di Scienze dell'Informazione, Universita degli Studi di Milano, 1993.

18. Izabelle. User's guide. University of Cambridge, 1996.

19. Jansen G. Hardware Verification using Temporal Logic: A Practical View // Formal VLSI Correctness Verification, VLSI Design Methods-П. Elsevier Science Publishers, 1990.

20. Korn D. Konstruktiv adaquate Beweisautomatisierung fur intuitionistische Logik. Sankt Augustin: Infix, 1999 (Dissertationen zur kiinstlichen Intelligenz; Bd. 198).

21. Korn D., Kreitz C. A Constructively Adequate Refutation System for Intuitionistic Logic. International Conference TABLEAUX'97 (Position Papers), Technischer Bericht CRIN 97-R-030, Centre de Recherche en Informatique de Nancy, 1997.

22. Korn D., Kreitz C. A Constructively Adequuate Refutation System for Intuitionistic Logic. Technischer Bericht AIDA-96-14, TU Darmstadt, 1996.

23. Miglioli P., Moskato U., Ornaghi M. An Improved Refutation System for Intuitionistic Predicate Logic. Journal of Automated Reasoning 13, pp. 361-373, 1994.

24. Minsky M. Steps toward Artificial Intelligence. In: Computer and Thoughts (ed. E. Feigenbann and D. Feldmann) McGraw Hill. 1963.

25. Otten J. and Kreitz K. Towards efficient prefix unification in non-classical theorem proving. Technical Report AIDA-00-03, Intellectics Group, Darmstadt University of Technology, May 2000.

26. Otten J. and Kreitz K. T-string unification: Unifying prefixes in non-classical proof methods. In Proc. 4-th TABLEAUX'95, volume 918 of LNAI, pp. 244 -260, Springer Verlag, Berlin, 1995.

27. Otten J. IleanTAP: An Intuitionistic Theorem Prover. In Automated Reasoning with Analytic Tableaux and Related Methods. Inter. Conference, TABLEAUX' 97, LNAI, Springer Verlag, 1997.110

28. Otten J., Kreitz C. A Connection Based Proof Method for Intuitionistic Logic. In Theorem Proving with Analytic Tableaux and Related Metods, TABLEAUX' 95, Springer Verlag, 1995.

29. Pnueli A. Now you can compose temporal logic specifications // Proceedings of the 16-th ACM Sumposium on on Theory of Computing, 1984.

30. Sahlin D., Franzen Т., Haridi S. An Intuitionistic Predicate Logic Theorem Prover. Journal of Logic and Computation 2(5), pp. 619 656,1992.

31. Schmitt S., Kreitz C. Converting Non-Classical Matrix Proofs into Sequent-Style Systems. 13-th International Conference on Automated Deduction, LNAI 1104, pp. 418 432, Springer, 1996.

32. Tammet T. A Resolution Theorem Prover for Intuitionistic Logic. In Proceedings of CADE-13, LNAI, Springer Verlag, 1996 .

33. Waaler A. Position paper: Termination in intuitionistic connection-driven search. In Automated Reasoning with Analytic Tableaux and Related Methods. International Conference, Tableaux'2000. Position Papers and Tutorials.

34. Weich K. Decision Procedures for Intuitionistic Propositional Logic by Program Extraction. Proceedings of the TABLEAUX'9 8 Conference, edited by H. de Swart, LNCS 1397, Springer-Verlag, pp. 292-308, 1998.

35. Wessel H. Logik.- VEB Deutscher Verlag der Wissenschaften, Berlin, 1989.

36. Бет Э. Метод семантических таблиц, (пер. А.О. Слисенко) // Математическая теория логического вывода. М.: Наука. Главная редакция физико-математической литературы, 1967.

37. Болотов А.Е., Бочаров В.А., Горчаков А.Е. Алгоритм поиска вывода в классической логике предикатов. // Логические исследования. Вып. 5. М.: Наука, 1998.

38. Болотов А.Е., Бочаров В.А., Горчаков А.Е. Алгоритм поиска вывода для натурального классического исчисления высказываний. // Логические исследования, вып. 3, М., 1995.1.l

39. Болотов A.E., Бочаров В.А., Горчаков А.Е. Алгоритм поиска вывода для натурального классического исчисления высказываний. // 11 Международная конференция. Логика, методология, философия науки, ч. 2, М.-Обнинск, 1995.

40. Болотов А.Е., Бочаров В.А., Горчаков А.Е. Алгоритмы поиска вывода в классической пропозициональной логике. // Труды научно-исследовательского семинара логического центра Института философии РАН. М., 1996.

41. Бочаров В.А., Болотов А.Е., Горчаков А.Е., Шангин В.О. Алгорифм поиска вьшода в классической пропозициональной логике (не опубликовано).

42. Бочаров В.А., Маркин В.И. Основы логики. Учебник.- М.: Космополис, 1994.

43. Братко И. Программирование на языке Пролог для искусственного интеллекта. Пер. с англ. А.И. Лупенко, A.M. Степанова, под ред. А.М. Степанова. М., 1990.

44. Васюков В.Л. Автоматическое доказательство теорем. // Логика и компьютер. Вьш. 2. Логические языки, содержательные рассуждения и методы поиска доказательств. -М.: Наука, 1995.

45. Генцен Г. Исследования логических выводов, (пер. А.В. Идельсона) // Математическая теория логического вьшода.- М.: Наука. Главная редакция физико-математической литературы, 1967.

46. Драгалин А.Г. Математический интуиционизм. Введение в теорию доказательств.- М.: Наука. Главная редакция физико-математической литературы, 1979.

47. Кангер С. Упрощенный метод доказательства для элементарной логики (пер. С.Ю. Маслова) // Математическая теория логического вьшода.- М.: Наука. Главная редакция физико-математической литературы, 1967.112

48. Клини С.К. Перестановочность применений правил в генценовских исчислениях LK и LJ. // Математическая теория логического вывода. М.: Наука. Главная редакция физико-математической литературы, 1967.

49. Клини С.К. Математическая логика.- М.: "Мир", 1973.

50. Крайзель Г. Исследования по теории доказательств. // Математика: новое в зарубежной науке. №23. М.: "Мир", 1981.

51. Логика и компьютер. Вып. 1. Моделирование рассуждений и проверка правильности программ / Н.А. Алешина, A.M. Анисов, П.И. Быстрое и др. -М.: Наука, 1990.

52. Логика и компьютер. Вып. 4. Карпенко А.С. Многозначные логики.- М.: Наука, 1997.

53. Логический подход к искусственному интеллекту: от классической логики к логическому программированию: Пер. с франц./ Тейз А., Грибомон П., Луи Ж., и др.-М.: Мир, 1990.

54. Макаров В.В. Автоматическое доказательство теорем интуиционистской пропозициональной логики.\\ Современная логика: проблемы теории, истории и применения в науке. Материалы 5-ой всероссийской научной конференции, СПб, 1998.

55. Макаров В.В. Некоторые проблемы компьютерной реализации автоматической процедуры доказательства для натурального вывода, (совместно с Горчаковым А.Е., Спириным С.В.). В Online Journal «Логические исследования», 1998.

56. Макаров В.В. Односукцедентное секвенциальное классическое пропозициальное исчисление. Материалы международной конференции «Третьи Смирноские чтения», 2001.

57. Маслов С.Ю., Минц Г.Е. Теория поиска вывода и обратный метод. // ЧеньЧ., Ли Р. Математическая логика и автоматическое доказательство теорем. М., "Наука", 1983.113

58. Мендельсон Э. Введение в математическую логику. Пер. с англ. Кабакова Ф.А. / Под ред. Адяна С.И. М.: Наука. Главная редакция физико-математической литературы, 1971.

59. Минц Г.Е. Исчисления резолюций для неклассических логик. // Семиотика и информатика. Вып.25. М., 1985.

60. Непейвода Н.Н. Практическая логика: Учеб. пособие. Новосибирск, Из-во Новосибирского университета, 2000.

61. Новиков П.С. Конструктивная математическая логика с точки зрения классической.- М.: Наука. Главная редакция физико-математической литературы, 1977.

62. Правиц Д. Натуральный вывод. Теоретико-доказательственное исследование. Пер. с англ. Быстрова П.И. М.: Изд-во "ЛОРИ", 1997.

63. Расева Е., Сикорский Р. Математика метаматематики. Пер. с англ. Янкова В.А. М.: Наука. Главная редакция физико-математической литературы, 1972.

64. Смирнов А., Новодворский А. Язык описания логических систем. // Логические исследования. Вып. 3. М.: Наука, 1995.

65. Справочная книга по математической логике. Часть 4. М., 1983.

66. Суханов К.Н. Критический очерк гносеологии интуиционизма. Челябинск: Юж.-Ур. кн. изд-во, 1973.

67. Такеути Г. Теория доказательств. М.: "Мир", 1978.

68. Успенский В. Абстракция актуальной бесконечности. // Философская энциклопедия в 5 томах, т. 1. М., 1960.

69. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем: Пер. с англ. // Под ред. Маслова С.Ю. М.: Наука. Главная редакция физико-математической литературы, 1983.

70. Шрамко Я.В. Логическое следование и интуиционизм (проблема релевантизации интуиционистской логики).-Киев: "ВИПОЛ", 1997.