Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

((А^В)^А)^А является тавтологией и секвенция ^ ((А^В)^А)^А имеет вывод в G Описанную процедуру поиска контрпримера представим в виде следующего алгоритма. В процедуре поиск {search) алгоритм просматривает все листья строящегося дерева вывода слева направо. Для каждого листа, не являющегося атомарной формулой, вызывается процедура раскрытия формулы {expand). Процедура expand строит поддерево, выбирая подходящее правило вывода, чтобы исключить из неатомарной формулы главную связку. Алгоритм продолжает работу до тех пор, пока каждый лист станет атомарной формулой. После того как все листья составлены из секвенций только с атомарными формулами делается заключение: если все листья аксиомы, то контрпримера нет и исходная секвенция выводима, иначе контрпример существует и секвенция не выводима. Запишем этот алгоритм в виде привычном для компьютерщика [34]: Procedure Search procedure search(r —>Л\ sequent; var T : tree}; begin let T be the one-node tree labeled with Г while not all leaves ofT are finished do To:=T; for each leafnode of To (in lexicographic order of tree addresses) do if not finished(node.) then expand(node, T) endif endfor endwhile; if all leaves are axioms then write (T is a proof ofF^A) else write {Г —>A isfalsifiable) endif end Procedure Expand procedure expand(node : tree-address; var T: tree); begin 135