Страница публикации

Об исчислении позитивно-образованных формул для автоматического доказательства теорем

Авторы: Давыдов А.В., Ларионов А.А., Черкашин Е.А.

Журнал: Моделирование и анализ информационных систем

Том: 17

Номер: 4

Год: 2010

Отчётный год: 2010

Издательство:

Местоположение издательства:

URL:

Проекты:

DOI:

Аннотация: Рассматривается выразительный логический язык LF и основанное на нем исчисление. Формулы этого языка состоят из некоторых крупно-блочных структурных элементов, таких как типовые кванторы. Язык LF содержит всего два логических символа - для каждого и существует, которые составляют множество логических связок языка. Рассматривается логическое исчисление JF и полные стратегии автоматического поиска выводов, основанные на единственном унарном правиле вывода. Это исчисление обладает рядом других особенностей, благодаря которым достигается уменьшение комбинаторной сложности при поиске выводов в сравнении с такими известными системами автоматического доказательства теорем (АДТ), как метод резолюций и генценовские исчисления. Рассмотрены вопросы об эффективной реализации нового исчисления в виде программной системы для автоматического доказательства теорем.

Индексируется WOS: Нет

Индексируется Scopus: Нет

Индексируется УБС: Нет

Индексируется РИНЦ: Да

Индексируется ВАК: Нет

Индексируется CORE: Нет

Публикация в печати: 0