Процедуры формального вывода в дедуктивных системах

Процедура формального вывода в дедуктивных системах, или цепочка вывода, представляет собой последовательность формул, начинающуюся с аксиом, в которой каждая последующая формула выводится на основе совокупности предшествующих формул и аксиом. В формальных системах с малым числом ПВ обычно имеется большое число аксиом, и наоборот. Исходная постановка решаемой задачи представляется в виде утверждений (аксиом) — Ру, р2,. ..,Р — ИП первого порядка. Цель задачи В также записывается в виде утверждения, справедливость которого следует установить или отвергнуть на основании аксиом и ПВ формальной системы. Тогда поиск решения задачи (достижение цели задачи) сводится к выяснению логического следования (выводимости) целевой формулы В из заданного множества формул (аксиом) —Fl, Такое выяснение равносильно доказательству общезнач-ности (истинности) формулы Ру Р - В или невыпол- [c.149]

Справочник химика 21

Химия и химическая технология