Прикладной логический анализ

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