Markus Wenzel wrote: > > 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. On the second thought: When we claim that we do "logic" it is usually meta-logic. Could you look to the articles LUKASI_1 or PROCAL_1? Do they fit your needs? Andrzej