Re: Plain logical reasoning in Mizar

[Grzegorz Bancerek <bancerek@math.uwb.edu.pl>]

On Sat, 13 Nov 1999, Freek Wiedijk wrote:

> Markus:
> 
> >Is it possible to do plain logical reasoning in Mizar?  For example,
> >derive basic propositional tautologies such as A --> A, A & B --> B & A,
> >etc.
> 
> I don't know whether schemes allow one to do this.  I suppose so.  Did
> you try that?

Of course, you may do it by scheme:

sch1 {A[]}:
 A[] implies A[]
proof
 assume A[];
 hence A[];
end;

===============================================================
Grzegorz Bancerek               e-mail: bancerek@mizar.org 
                                        (bancerek@math.uwb.edu.pl)
Dept. of Applied Logic          http://math.uwb.edu.pl/~bancerek/
Institute of Computer Science   fax. +48 (85) 745-7073
University of Bialystok         tel. +48 (85) 745-7559 (office)
15-267 Bialystok, Poland             +48 (85) 719-1984 (home)