Все шпаргалки / Математическая логика / 

Исчисление высказываний. Расширение принципа резолюции (линейность и упорядоченность литер в дизъюнкте).

см. вопрос 9.Для усиления принципа резолюции оказалось возможным повторное и неоднократное использование резольвент в процессе вывода, т. е. превращать центральные узлы графа в боковые вершины. Этот метод получил название линейной резолюции.Следует обратить внимание, что использование закона дистрибутивности ведёт к “разбуханию” формул, что разрушает их структуру и может привести к неверным заключениям в принципе резолюции. Более того учёт невостребованных посылок также не обеспечивает пустой резольвенты.Для усиления принципа резолюции вводят упорядоченные дизъюнкты по их вхождению в резольвенты и учёт информации об удаляемых контрарных литерах для возможного их восстановления в последующих склеиваниях.