Моделирование и анализ информационных систем
RUS  ENG    ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB  
Общая информация
Последний выпуск
Архив
Импакт-фактор

Поиск публикаций
Поиск ссылок

RSS
Последний выпуск
Текущие выпуски
Архивные выпуски
Что такое RSS


Модел. и анализ информ. систем:
Год:
Том:
Выпуск:
Страница:
Найти




Персональный вход:
Логин:
Пароль:
Запомнить пароль
Войти
Забыли пароль?
Регистрация

Моделирование и анализ информационных систем, 2010, том 17, номер 4, страницы 60–70 (Mi mais36)  
Эта публикация цитируется в 1 научной статье (всего в 1 статье)

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

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

a Институт динамики систем и теории управления СО РАН
b Институт математики, экономики и информатики ИГУ
PDF полного текста (326 kB) Список цитирования (1)
Список литературы:
PDF
HTML
Аннотация: Рассматривается выразительный логический язык LF и основанное на нем исчисление. Формулы этого языка состоят из некоторых крупно-блочных структурных элементов, таких как ти́повые кванторы. Язык LF содержит всего два логических символа — $\forall$ и $\exists$, которые составляют множество логических связок языка. Рассматривается логическое исчисление JF и полные стратегии автоматического поиска выводов, основанные на единственном унарном правиле вывода. Это исчисление обладает рядом других особенностей, благодаря которым достигается уменьшение комбинаторной сложности при поиске выводов в сравнении с такими известными системами автоматического доказательства теорем (АДТ), как метод резолюций и генценовские исчисления. Рассмотрены вопросы об эффективной реализации нового исчисления в виде программной системы для автоматического доказательства теорем.
Ключевые слова: автоматическое доказательство теорем, математическая логика, неклассические логики, искусственный интеллект.
Поступила в редакцию: 18.10.2010
Тип публикации: Статья
УДК: 517.51+514.17
Образец цитирования: А. В. Давыдов, А. А. Ларионов, Е. А. Черкашин, “Об исчислении позитивно-образованных формул для автоматического доказательства теорем”, Модел. и анализ информ. систем, 17:4 (2010), 60–70
Цитирование в формате AMSBIB
\RBibitem{DavLarChe10}
\by А.~В.~Давыдов, А.~А.~Ларионов, Е.~А.~Черкашин
\paper Об исчислении позитивно-образованных формул для автоматического доказательства теорем
\jour Модел. и анализ информ. систем
\yr 2010
\vol 17
\issue 4
\pages 60--70
\mathnet{http://mi.mathnet.ru/mais36}
Образцы ссылок на эту страницу:
  • https://www.mathnet.ru/rus/mais36
  • https://www.mathnet.ru/rus/mais/v17/i4/p60
    • Эта публикация цитируется в следующих 1 статьяx:
    Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    		Моделирование и анализ информационных систем
     
      Обратная связь:
    		  Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2024