8.5.14 Conclude

Prev Up Next Page 339 of 800 Search internet

The conclude operator A conclude C tries to prove C using the argumentation A. To do so, it adapts A to C and does unification. As an example of use, consider this:

Prop lemma M1.8j : #x imply #x end lemma

prepare proof indentation,proof of M1.8j : line L01 : Premise >> Prop ; line L06 : MP ponens ( MP ponens A2 At At At ponens A1 At At ) ponens ( A1 conclude #x imply #y imply #x ) >> #x imply #x qed

Compared to the proof given earlier, we have replaced A1 At at #y by A1 conclude #x imply #y imply #x. The latter tells the system to use A1 to prove #x imply #y imply #x which may be easier to comprehend than A1 At at #y.

Prev Up Next Page 339 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05