*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Elim resolution*From*: "Chris Capel" <pdf23ds at gmail.com>*Date*: Sun, 11 Jan 2009 19:19:50 -0600*In-reply-to*: <737b61f30901101510x8a7620fh5296ad6cec8dfaa5@mail.gmail.com>*References*: <737b61f30901101510x8a7620fh5296ad6cec8dfaa5@mail.gmail.com>

I'm reading "Introduction to Isabelle", which has a very nice few chapters on the low-level user-visible parts of Isabelle. I'm surprised it's not linked from the Documentation page on the main site, even if it does have a long section on shell interaction. None of the other documents come close to the level of detail as to how Isabelle really works, and none leave me feeling as if I really understand what I'm doing when I'm executing a proof. It's nice that even though I'm not a mathematician (by any means), I was able to read a few Wikipedia articles for background and understand almost all of it. Anyway, I'm a bit slow with all of this, being new to formal math, and I'm having trouble understanding how part of elim resolution is justified logically. Take the example from ITI 5.3 and 6.1: [| P | P ==> P |] ==> P | P --> P To prove this, we'd like to apply elim resolution (erule) to the only subgoal with disjE, which reads [| Q | R; Q ==> S; R ==> S |] ==> S First disjE needs to be lifted: [| P | P ==> ?Q | ?R; [| P | P; ?Q |] ==> ?S; [| P | P; ?R |] ==> ?S |] ==> (P | P ==> ?S) I follow up to this point. Here the book skips right to [| P ==> P; P ==> P |] ==> P | P --> P. I understand how it was unified, and I understand how the first subgoal, "P | P ==> ?Q | ?R" before unification, was discharged automatically as part of elim resolution, but I don't understand how the first assumption "P | P" from the two remaining subgoals can be eliminated. How is that justified? To restate, the book says that elim resolution replaces subgoal phi_i of the proof with lifted assumptions psi'_2 ... psi'_m from the resolution rule, *except with the assumption of psi'_1 deleted* (assuming psi'_1 was solved by assumption). How is that last part justified? Unless I'm missing something, the book skips that detail. Chris Capel -- "What is it like to be a bat? What is it like to bat a bee? What is it like to be a bee being batted? What is it like to be a batted bee?" -- The Mind's I (Hofstadter, Dennet)

**Follow-Ups**:**Re: [isabelle] Elim resolution***From:*Lawrence Paulson

**Re: [isabelle] Elim resolution***From:*Christian Doczkal

- Previous by Date: Re: [isabelle] Problems in isabelle installation
- Next by Date: Re: [isabelle] Problems in isabelle installation
- Previous by Thread: Re: [isabelle] Problems in isabelle installation
- Next by Thread: Re: [isabelle] Elim resolution
- Cl-isabelle-users January 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list