ножество правил вывода. В качестве примера приведем классическое правило отделения, или modus ponens :
(A, A - B) / B
которое читается так "если истинна формула A и истинно, что из A следует B, то истинна и формула B ". Формулы, находящиеся над чертой, называются посылками вывода, а под чертой - заключением. Это правило вывода формализует основной закон дедуктивных систем: из истинных посылок всегда следуют истинные заключения. Аксиомы и правила вывода исчисления предикатов первого порядка задают основу формальной дедуктивной системы, в которой происходит формализация схемы рассуждений в логическом программировании. Можно упомянуть и другие правила вывода.
Modus tollendo tollens : Если из A следует B и B ложно, то и A ложно.
Modus ponendo tollens : Если A и B не могут одновременно быть истинными и A истинно, то B ложно.
Modus tollendo ponens : Если либо A, либо B является истинным и A не истинно, то B истинно.
Решаемая задача представляется в виде утверждений (аксиом) f1, F2. . . Fn исчисления предикатов первого порядка. Цель задачи Bтакже записывается в виде утверждения, справедливость которого следует установить или опровергнуть на основании аксиом и правил вывода формальной системы. Тогда решение задачи (достижение цели задачи) сводится к выяснению логического следования (выводимости) целевой формулы B из заданного множества формул (аксиом) f1, F2. . . Fn. Такое выяснение равносильно доказательству общезначимости (тождественно-истинности) формулы
f1& F2&. . . & Fn - B
или невыполнимости (тождественно-ложности) формулы
Из практических соображений удобнее использовать доказательство от противного, то есть доказывать невыполнимость формулы. На доказательстве от противного основано и ведущее правило вывод
Страницы: << < 7 | 8 | 9 | 10 | 11 > >>