Proving syllogisms using inference rules TRANS, MUT and EX.

Line Proposition Rule used
Click "start" to generate list.

Choose the syllogism you want to prove (use the menus).

Premise 1:
Premise 2:
Conclusion:
Negated Conclusion: --

Click on the buttons in order to construct a proof of the argument

Explanation:
If the above argument is provable, the combination of the premises and the negated conclusion leads to a contradiction. Click on the rule buttons in order to construct a proof (if possible).

TRANS:
a(X,Y) & a(Y,Z) -> a(X,Z)
a(X,Y) & e(Y,Z) -> e(X,Z)
MUT:
i(X,Y) -> i(Y,X)
e(X,Y) -> e(Y,X)
EX:
a(X,Y) -> i(X,Y)
e(X,Y) -> o(X,Y)