Алгоритм распознавания выполнимости формул логики ветвящегося времени и эффективный алгоритм построения выводов общезначимых формул из аксиом
Аннотация:
Рассматривается логика ветвящегося времени, являющаяся обобщением логики высказываний с помощью введения специальных временнЫх операторов
и кванторов перед ними. Истинность формул пределяется по значениям пропозициональных переменных в вершинах связного ориентированного графа.
В работе построен и детально изложен оригинальный табличный алгоритм, распознающий выполнимость формулы логики ветвящегося времени и строящий для любой выполнимой формулы модель. Дано детальное
доказательство корректности и полноты этого алгоритма. Сформулирован эффективный алгоритм построения вывода произвольной общезначимой формулы из аксиом, доказаны его полнота и корректность.
