Ребята, я тут пытаюсь понять(дня 2 уже) как работает modus ponens для вывода формул( http://ru.wikipedia.org/wiki/Modus_ponens )
На словах всё понятно. Читаю пример(даже написано какие правила нужно применять), но не могу понять как это делается(что к чему относится).
Вот пример: http://ompldr.org/vZDU3OQ/ponens.png
Первые 8 строк это правила и сам ponens написанные формально. Первые 2 шага ещё понятны, но потом тёмный лес. Не понимаю какая часть формулы к какому правилу относится. Объясните если не сложно.