Раздел 10. Хорновские формулы

Определим вначале один интересный класс булевых формул – Хорновские формулы.

Определение: Пусть – это множество логических (булевых) переменных. Хорновская ( -) формула – это формула вида

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

В этих и других областях представляют интерес связанные между собой задачи о минимальности набора -формул и о выводимости некоторой -формулы из заданного набора -формул. Первая задача состоит в выяснении того, входит ли в набор -формул некоторая формула , которая может быть удалена из без потери информации, т.е. которая выводится из , а это и есть задача о выводимости. Уточним эту задачу.

Определение: -формула является следствием или выводится из множества -формул , если на всяком наборе значений переменных из , на котором истинны все формулы из , истинна и (будем это обозначать как ).

Это понятие следования некоторой формулы из множества формул можно сформулировать и для произвольных булевых формул, а не только для Хорновских. Следующее простое утверждение показывает, что понятие следования (выводимости) можно переформулировать в терминах тождественной истинности.

Предложение: -формула является следствием множества тогда и только тогда, когда формула

(*)

является истинной на всех наборах значений переменных (т.е. тождественно истинной).

Доказательство: непосредственно следует из определения значений конъюнкции и импликации.

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

Мы изложим этот алгоритм на примере одного из интересных «экономических» приложений -формул – задачи о возможности производства заданной продукции (набора товаров) из некоторого множества исходных продуктов (товаров, сырья).

Дата добавления: 2015-10-28