В чем заключается метод обратного вычисления логических формул?

Метод обратного вычисления логических формул заключается в построении логического вывода в направлении «сверху вниз» (от аксиом к доказываемой формуле). infocom.spbstu.ru

Этот метод был изобретён советским математиком С. Ю. Масловым в 1964 году и подходит для автоматизации доказательств в различных логических исчислениях: логика высказываний, классическая логика первого порядка, интуиционистская логика, модальные логики и т. д.. infocom.spbstu.ru

Алгоритм обратного вывода основан на рекурсивной замене заданной целевой формулы в соответствии с фактами и правилами базы знаний: cyberleninka.ru

1. На первом шаге каждый предикат целевой формулы, содержащий переменные, подвергается возможной замене на соответствующий факт базы знаний. cyberleninka.ru Новая полученная целевая формула рекурсивно анализируется по точно такому же алгоритму. cyberleninka.ru
2. После того как все возможные подобные замены будут произведены, для каждого предиката целевой формулы ищется соответствующее правило базы знаний, согласно которому данный предикат можно заменить последовательностью других предикатов, составляющих условие правила. cyberleninka.ru Новая формула также рекурсивно подвергается точно такой же процедуре, начиная с первого шага. cyberleninka.ru
3. Процесс продолжается до тех пор, пока целевая формула не превратится в аксиому, то есть все её предикаты не станут тождественно равными какому-либо факту базы знаний. cyberleninka.ru

Если за время вывода не было найдено ни одного преобразования, превращающего целевую формулу в аксиому, это означает, что данная формула ложна. cyberleninka.ru Если же такие преобразования нашлись, то целевая формула истинна. cyberleninka.ru