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

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

Тип публикации: Статья в журнале

Тип материала: Текст

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

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

Язык публикации: russian

Том: 17

Номера страниц: 60–69

Количество страниц: 10

Номер: 4

Год публикации: 2010

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

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

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

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

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

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

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

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