[Prev][Next][Index]
Proving "partitioned by"
Michal,
Jim Horning forwarded your query concerning the example on page 141 of the
Larch book to me. He guessed correctly that the example was constructed using
Version 2.4 of LP, and that Version 3.1 of LP behaves somewhat differently.
To finish the proof of the "partitioned by" in LP, Version 3.1, you should
type "resume by =>" before typing "complete". The reason for this change is as
follows. When lp2.4 was instructed to prove a deduction rule of the form
when forall x P(x, y) yield Q(y)
it introduced P(x, yc) as a new hypothesis and attempted to prove Q(yc) as a
subgoal. By contrast, when lp3.1 is instructed to prove a deduction rule of
the form
when \A x P(x, y) yield Q(y)
it attempts to prove \A x P(x, y) => Q(y) as a subgoal; if you then type
"resume by =>", lp3.1 introduces P(x, yc) as a new hypothesis and attempts to
prove Q(yc). The reasons for the change in behavior from lp2.4 to lp3.1 were
(a) the lp3.1 formulation was impossible in lp2.4, which allowed explicit
quantifiers only in deduction rules (and not in formulas), and
(b) the lp3.1 formulation does not preclude a proof by induction (e.g., on y),
as did the lp2.4 formulation.
Steve Garland