Головная страница ИПМ Библиотеки, издания  •  Поиск публикаций  English 
Публикация

Статья в сборнике "Математические вопросы кибернетики" №15, Москва, 2006
Авторы: Хелемендик Р.В.
Алгоритм распознавания выполнимости формул логики ветвящегося времени и эффективный алгоритм построения выводов общезначимых формул из аксиом
Аннотация:
Рассматривается логика ветвящегося времени, являющаяся обобщением логики высказываний с помощью введения специальных временнЫх операторов и кванторов перед ними. Истинность формул пределяется по значениям пропозициональных переменных в вершинах связного ориентированного графа. В работе построен и детально изложен оригинальный табличный алгоритм, распознающий выполнимость формулы логики ветвящегося времени и строящий для любой выполнимой формулы модель. Дано детальное доказательство корректности и полноты этого алгоритма. Сформулирован эффективный алгоритм построения вывода произвольной общезначимой формулы из аксиом, доказаны его полнота и корректность.
Ключевые слова:
логика ветвящегося времени, алгоритм распознавания выполнимости, модель, аксиома, общезначимость, логический вывод
Язык публикации: русский, страниц: 60 (с. 217-266)
Направление исследований:
Математические вопросы и теория численных методов
Полный текст: Сведения об авторах:
  • Хелемендик Роман Викторович,  ИПМ им. М.В. Келдыша РАН