Статья: Как вычислять интересные следствия

В современном дедуктивном анализе к основным задачам относятся следующие: поиск доказательства заданного утверждения с помощью аксиом и правил вывода и проверка корректности заданного следствия из определенных посылок. Что касается задачи вывода следствий с заранее заданными свойствам (в литературе они названы интересными следствиями), то о них в настоящее время известно немного. Также нет четкого ответа на следующие вопросы: какие свойства присущи интересному следствию и как вычислить интересное следствие?

Ответы на эти вопросы можно получить, если для моделирования рассуждений воспользоваться математическим аппаратом алгебры кортежей, в основу которой заложены ранее неизвестные свойства декартова произведения множеств. Объектами алгебры кортежей являются произвольные многоместные отношения. Эти отношения можно рассматривать как интерпретации формул мате-матической логики. Они представляют собой матрицеподобные структуры, у которых ячейки со-держат не элементы, а подмножества соответствующих атрибутов. Операции (дополнение, обоб-щенное пересечение и обобщенное объединение) в алгебре кортежей соответствуют логическим связкам математической логики (отрицание, конъюнкция, дизъюнкция), а отношение обобщенное включение – отношению выводимости. Вычисление кванторных операций выполняется с помо-щью операций с атрибутами (добавление фиктивного атрибута, что соответствует правилу обобщения в исчислении предикатов, и элиминация атрибута). Для двух из четырех типов струк-тур алгебры кортежей элиминация атрибутов соответствует вычислению проекции отношения. Для вывода интересных следствий в алгебре кортежей используется структура, названная мини-мальным следствием, которая равна обобщенному пересечению посылок, выраженных структу-рами алгебры кортежей. Интересные следствия вычисляются как проекции минимального следст-вия. В результате вычислений и проверок получаются следствия с сокращенным или заданным составом переменных, а также с сокращенным объемом записи.