Системные предикаты для управления логическим выводом в системе автоматического доказательства теорем для исчисления позитивно-образованных формул
Автор: Ларионов Александр Александрович, Черкашин Евгений Александрович, Терехин Иван Николаевич
Журнал: Вестник Бурятского государственного университета. Философия @vestnik-bsu
Рубрика: Системный анализ, обработка информации и информационные технологии
Статья в выпуске: 9, 2011 года.
Бесплатный доступ
В статье предлагается подход к реализации процесса управления поиском автоматического доказательства теорем в исчислении позитивно-образованных формул. Управление выводом представляется в виде комбинации системных предикатов в оригинальном логическом языке представления формул. Предложены рекомендации по использованию подхода.
Исчисление позитивно-образованных формул, автоматическое доказательство теорем, логический вывод
Короткий адрес: https://sciup.org/148180546
IDR: 148180546 | УДК: 004.832.38
System predicates for control of logical inference in automated theorem proving systems based on calculi of positively constructed formulae
An approach for a control process implementation of search for automated theorem proof in the calculi of positively constructed formulae is described in the paper. The search process is represented as system predicates and their combinations in the original logical language for formulae definition. Application recommendations of the approach are proposed.
