Re: [isabelle] need help
The correct way to formalise your system is by expressing the axiom in
[| 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.)
On 1 Jul 2008, at 15:16, Erich Kummerfeld wrote:
The trick I'm trying to accomplish with the first problem actually
the second problem I'm having. Basically I'm trying to solve [| B x
S x |] ==> False by transforming it into [| B x False & S x |] ==>
then using the axiom I mentioned earlier. Neither of these steps
work though and that's my confusion.
This archive was generated by a fusion of
Pipermail (Mailman edition) and