Ветвящиеся программы как доказательство невыполнимости формулы. Одноразовые ветвящиеся программы. Резолюционные доказательства. Построение ветвящейся программы по резолюционному доказательству. Построение резолюционного доказательства по одноразовой ветвящейся программе. Нижняя оценка для принципа Дирихле.