Содержаться результаты исследований авторов, полученные при реализации системы автоматического доказательства теорем и логическом языке позитивно-образованных формул первого порядка и его исчислении. Рассмотрены вопросы разработки и адаптации современных подходов к повышению производительности систем автоматического поиска логического вывода к свойствам языка и исчисления. Проведен анализ результатов тестирования программы на разных классах задач.
Монография предназначена для специалистов, чьи научные интересы находятся в области информатики, теории программирования. компьютерной логики. автоматического доказательства теорем, а также она будет полезна аспирантам и студентам старших курсов математических специальностей, изучающих компьютерную логику и логическое программирование.
Издание выходит в рамках Программы стратегического развития ФГБОУ ВПО "ИГУ" на 2012-2016 гг., проект Р121-02-001.