Литература

• [Andrews] Andrews, P. Transforming matings into natural deduction proofs

// 5^th Conference on Automated Deduction, 1980.

• [Basin et al] Basin, D., Matthews, S.

non-classical logics // Studia Logica, vol. 60, №1, 1998.

• [Bocharov et al] Bocharov, V., Bolotov, A., Gorchakov, A. and V. Shangin.

Proof-searching algorithm in first order classical natural deduction calculus // 12th International Congress of Logic, Methodology and Philosophy of Science. Oviedo (Spain), August 7-13, 2003.

• [Bochmann] Bochmann, G. Hardware specification with temporal logic: an

example // IEEE Transactions on computers, vol. C-31, №3, 1982.

• [Bolotov & Fisher] Bolotov, A. and M. Fisher. A resolution method for

computational tree branching time temporal logic // IV International workshop on temporal representation and reasoning (TIME'97). Florida, 1997.

• [Byrnes] Byrnes, J. Proof search and normal forms in natural deduction.

PhD thesis, Pittsburgh, 1999.

• [Church] Church, A. A note on the Entscheidungsproblem // The Journal

of Symbolic Logic, vol. 1, №1, 1936.

• [Church1] Church, A. Correction to A note on the Entscheidungsproblem //

The Journal of Symbolic Logic, vol. 1, №3, 1936.

• [Copi] Copi, I. Symbolic logic. 3^rd ed. New-York, London, 1967.

• [Fitch] Fitch, F. Symbolic logic. New York, 1952.

• [Hintikka] Hintikka, J. A new approach to sentential logic // Societas

Scientarium Fennica Commentationes Physico-Mathematicae XVII, 2, 1957.

• [Hintikka 1] Hintikka, J. Notes on the quantification theory // Societas

Scientarium Fennica Commentationes Physico-Mathematicae XVII, 11, 1957.

• [Jaskowski] Jaskowski, S. On the rules of suppositions in formal logic //

Studia Logica, №1, 1934.

• [Kalish] Kalish, D. Review of Copi: Symbolic logic.

London, 1967 // The Journal of Symbolic Logic, vol. 39, №1, 1974.

Akademische Verlagsgesellschaft M.B.H., Leipzig, 1936.

quantifiers in natural deduction automated theorem proving // Journal of Automated

Reasoning, vol. 18, №1, 1997.

StudiaLogica, vol. 60, №1, 1998, доступна по адресу: http://www.cs.ualberta.ca/~jeffp/.

Philosophy of Logic, vol. 20, 1999, доступна по адресу: http://www.cs.ualberta.ca/~jeffp/.

automatic theorem provers // Journal of Automated Reasoning, 1986.

неопубликованная версия статьи доступна по адресу: http://oscarhome.soc- sci.arizona.edu/ftp/publications.html.

Studia Logica, vol. 60, №1, 1998.

Logic, vol. 15, №2, 1950.

principle // Journal of the ACM, vol. 12, №1, 1965.

classical logic) // Studia Logica, vol. 60, №1, 1998.

вывода в классической логике предикатов // Логические исследования. Вып. 5. М.,

Наука, 1998.

• [Болотов и др.1] Болотов ΛΈ., Бочаров ВА., Горчаков ΛΈ. Λлгоритм поиска

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

• [Болотов и др.2] Болотов ΛΈ., Бочаров ВА, Горчаков ΛΈ., Макаров В.В.,

Шангин В.О. Пусть докажет компьютер ∕∕ Логика и компьютер. Вып. 5. М., Наука, 2004. (Серия «Кибернетика - неограниченные возможности и возможные

ограничения».)

• [Бочаров и Маркин] Бочаров В.Д., Маркин В.И. Основы логики. М., Космополис, 1994.

• [Бочаров] Бочаров ВА. Исчисление предикатов с универсалиями (II.

Семантика) // Логические методы в компьютерных науках. (Труды научно-исслед. семинара по логике Ин-та философии АН СССР); Сб. ст. / Редкол.: Смирнов В.Λ. (отв. ред.) и др. М., ИФДН, 1991.

• [Братко] Братко И. Программирование на языке Пролог для

искусственного интеллекта: Пер.

• [Войшвилло] Войшвилло Е.К. Понятие. М., Изд-во МГУ, 1967.

• [Войшвилло 1] Войшвилло Е.К. Процедура поиска доказательства для

формул системы Е // Войшвилло Е.К. Философско-методологические аспекты релевантной логики. М., МГУ, 1989.

• [Генцен] Генцен Г. Исследования логических выводов //

Математическая теория логического вывода: Пер. с англ. ΛΈ. Идельсона / Под ред. ΛΈ. Идельсона и Г.Е. Минца. М., Наука, 1967.

• [Ивлев] Ивлев Ю.В. Логика: Учебник для высших учебных

заведений. 2-е изд., перераб. и доп. М., Логос, 1997.

• [Макаров] Макаров В.В. Λлгоритм поиска натурального вывода для

интуиционистской логики высказываний // Λвтореферат диссертации на соиск. учен. степ. канд. филос. наук. М., Соцветие красок, 2002.

• [Мендельсон] Мендельсон Э. Введение в математическую логику: Пер. с

англ. Φ.Λ. Кабакова / Под ред. С.И. Λдяна. 2-е изд., испр. М., Наука, 1976.

• [Минц] Минц Г.Е. Теорема Эрбрана // Математическая теория

логического вывода: Под ред. ΛΈ. Идельсона и Г.Е. Минца. М., Наука, 1967.

• [Непейвода] Непейвода Н.Н. Прикладная логика: Учебное пособие. 2-е

изд., испр. и доп. Новосибирск, Изд-во Новосиб. ун-та, 2000.

• [Смирнов] Смирнов ВА. Теория логического вывода. M., РОССПЭН,

2000.

• [Смирнов и др.] Смирнов В.A., Mаркин В.И., Новодворский AΕ., Смирнов

A3. Доказательство и его поиск (курс логики и компьютерный практикум) // Логика и компьютер. Вып. 3. M., Наука, 1996. (Серия «Кибернетика - неограниченные возможности и возможные ограничения».)

• [Смирнов-мл.] Смирнов A3. Система интерактивного доказательства

теорем // Логические исследования. Вып. 2. M., Наука, 1993.

• [Смирнов-мл.1] Смирнов AΕ. Язык описания логических систем для

автоматического поиска доказательства // Aвтореферат диссертации в виде научного доклада на соиск. учен. степ. канд. филос. наук. M., 1998.

• [Чень и Ли] Чень Ч., Ли Р. Mатематическая логика и автоматическое

доказательство теорем. Пер. с англ. / Под ред. С.Ю. Mаслова. M., Наука, 1983.

• [Шангин] Шангин В. О. Теорема корректности для алгоритма поиска

вывода в классической пропозициональной логике // Материалы VI Международной научной конференции «Современная логика: проблемы теории, истории и применения в науке». СПб., СПбГУ, 2000.

• [Шангин 1] Шангин В. О. Aвтоматический поиск натурального вывода в

интуиционистской логике и проблема дубликации // Материалы VII Международной научной конференции «Современная логика: проблемы теории, истории и применения в науке». СПб., СПбГУ, 2002.

• [Шангин2] Шангин В.О. Mетатеоретические свойства натурального

вывода // Материалы IV Международной конференции «Смирновские чтения».M., ИФРAН, 2003.

• [Шангин3] Шангин В. О. Aвтоматический поиск натурального вывода в

интуиционистской логике и проблема дубликации // Аспекты, Том 2. M., Современные тетради, 2003.

• [Шанин] Шанин НА., Давыдов Г.В., Mаслов С.Ю., Mинц Г.Е.,

Оревков В.П., Слисенко AO. Aлгорифм машинного поиска естественного логического вывода в исчислении высказываний. Л., Наука, 1964.