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

Метод обратного вывода Маслова — это способ построения логического вывода, предложенный советским математиком С. Ю. Масловым в 1964 году. infocom.spbstu.ru

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

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

В отличие от ряда табличных методов, обратный метод Маслова не требует использования глобальных переменных, выполнения поиска с возвратом и отслеживания циклов. disser.spbu.ru www.dissercat.com