Re: [isabelle] need help



The correct way to formalise your system is by expressing the axiom in the form

 [| B x False; S x |] ==> False

in the first place. Then it looks like you would have nothing to do. As I mentioned earlier, we do not attempt to create complex formulas in the assumptions. In a formal sequent calculus this is simply impossible: the available rules only allow formulas to be broken down, not built up. (When used to construct a backward proof of course.)

Larry Paulson


On 1 Jul 2008, at 15:16, Erich Kummerfeld wrote:

The trick I'm trying to accomplish with the first problem actually ties into the second problem I'm having. Basically I'm trying to solve [| B x False; S x |] ==> False by transforming it into [| B x False & S x |] ==> False and then using the axiom I mentioned earlier. Neither of these steps appears to
work though and that's my confusion.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.