yourdomain.com

Такая ситуация. Есть задача: построить выводы секвенций в ИС:
(б) (A->B),(B->C)|-(A->C)
Нужно использовать 15 формул. Правила вывода:
Г₁ |- A; Г ₂ |- B
________________________________
Г₁, Г₂ |- (A&B)
и т.д.


Я не могу понять: как их использовать и что куда откуда следует.
Сверху вниз или снизу вверх в правилах вывода идет... не следствие... а вывод что ли.
А когда я решаю. мне как эти правила применять? Снизу вверх или сверху вниз?
А почему? И зачем при решении все это дело записывать снизу вверх, это же неудобно!

walkrunm писал(а):Source of the post
(б) (A->B),(B->C)|-(A->C)

Это значит что у вас есть два утверждения A->B и B->C и из них выводится A->C

Г₁ |- A; Г ₂ |- B
________________________________
Г₁, Г₂ |- (A&B)

Это значит что если у вас есть вывод А из набора посылок Г1 и вывод B из набора Г2 то из объединения
Г1,Г2 можно вывести (A&B) - в общем то очевидно.

То что над чертой это набор выводов а под чертой новый вывод который из них вытекает.

Если вы пишете снизу вверх то вы идете от цели пытаясь разбить ее на кусочки, если пишете сверху вниз - то идете от мелких утверждений к вашей теореме - используются оба подхода. Возьмите классический учебник по логике - там все это расписано с прекрасными примерами. Вкурить не видев ни разу вывода в таком духе непросто.

Я бы рекомендовал Клини С. К. "Математическая логика" там неспешно с примерами все рассказывается.

Есть еще система HOL в которой такие доказательства сами собой получаются, но разбираться с ней... В общем не рекомендую если мало времени, но если хотите наоборот разобраться в деталях - очень даже хорошая документация и программа. Если разберетесь в HOL то логика вам точно не страшна)

Формулы надо оформлять ом, конъюнкция пишется \&: , дизъюнкция \vee: , вывод \vdash: .

Нужно указать систему аксиом. Нужно явно указать правила вывода. Только потом сможете построить вывод. Чтобы понять, как доказывать, просто посмотрите определение вывода формулы.
Если все равно непонятно, можете скачать Игошина, теорию и задачник, там все очень подробно расписано с примерами.

walkrunm писал(а):Source of the post
Такая ситуация. Есть задача: построить выводы секвенций в ИС:
(б) (A->B),(B->C)|-(A->C)
Нужно использовать 15 формул. Правила вывода:
Г₁ |- A; Г ₂ |- B
________________________________
Г₁, Г₂ |- (A&B)
и т.д.


Я не могу понять: как их использовать и что куда откуда следует.
Сверху вниз или снизу вверх в правилах вывода идет... не следствие... а вывод что ли.
А когда я решаю. мне как эти правила применять? Снизу вверх или сверху вниз?
А почему? И зачем при решении все это дело записывать снизу вверх, это же неудобно!

тут импликация A->B = не-А V B

Из-за нее вывод довольно длинноват будет.