deniok: (Рыжий)
Контрприменяю правило введения импликации в сукцедент секвенции, затем контрприменяю правило введения импликации в антецедент секвенции, затем опять контрприменяю правило введения импликации в сукцедент секвенции, и мы у цели: оба листа дерева поиска вывода суть аксиомы.

Упражнение на вывод типов: вывод какой тавтологии пропозициональной логики я строю в исчислении секвенций?
deniok: (Default)
А вот, кстати, что у нас в CS Клубе будет в конце сентября. Джон Хариссон прочитает 5 лекций про автоматическое доказательство теорем. Я считаю, что это замечательно.

Profile

deniok: (Default)
deniok

April 2017

S M T W T F S
      1
23 45678
9101112131415
16171819202122
23242526272829
30      

Syndicate

RSS Atom

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 27th, 2017 02:31 am
Powered by Dreamwidth Studios