Title Page
CONTENTS OF PREVIOUS ISSUES
1 9 9 6
No. 1 / Winter
QED Initiative
(QED Manifesto, etc)
Mechanization of Reasoning
(Raport on a Book)
The Centenary
of LvovWarsaw School
(G. Falkenberg J. Jadacki)
No. 2 / Spring
Descartes, Leibniz  Anniversaries
Formalized Mathematics
(A story by J. Harrison)
Formalizing Mathematics
by Reformulations
(M. Kerber)
A Browsable Format
for Proof Presentation
(J. Grundy's interactive paper)
Leibniz and Knowledge Engineering
(W. Marciszewski)
A Dialog on Logic and Rhetoric
(J. Woleński et al)

What concern is it of yours?
An Introductory Comment on Mizar MSE
i.e. MultiSorted [firstorder logic with]
Equality (while Mizar is the lucky star to shine over the project).
Teaching Freshman Logic with Mizar MSE
 by H. James Hoover and Piotr Rudnicki.
"We like to share our experience of using a proofchecker in teaching
introductory logic to first year science students who plan to enroll into
computing science."
A System of Suppositional Logic
Embodied in the Proof Checker Mizar MSE
 by Witold Marciszewski.
ASCII, TeXformatted, 40K
TeX, zipcondensed, 15K
TeX, arjcondensed, 21K
Jan Łukasiewicz and Stanisław Ja¶kowski are credited with being the first
who remarked that practicizing mathematicians do not appeal to logic
theories but make use of other methods of proof. The idea of creating
a new kind of logic to match the mathematical practice has been materialized
both in Gentzen's calculi (1934) and in Ja¶kowski's suppositional calculus
(1934 too). The latter has been developed up to the stage of the
proofchecker Mizar MSE.
Mizar MSE Introduction to Logic  by Marcin
Mostowski
ASCII, TeXformatted, 190K
TeX, zipcondensed, 52K
TeX, arjcondensed, 60K
PS, zipcondensed 113K.
This is a concise textbook but in two respects it goes far beyond a typical
course of logic. (i) It presents the proofchecker Mizar MSE as applied to
the study of logic (ii) in the context of a discussion on the algorithmic
processing of logical formulas. This is why it is published here as an
original contribution to the area of computerasisisted reasoning. The choice of topics
and examples makes it attractive also for those interested in the humanities
and philosophy.
Software for Downloading
Mizar MSE  version for MS DOS.
Original Site  University in Bialystok, Bialystok, PL.
Maintained by Roman Matuszewski.
msebial.exe 88 K
msebial.zip 80 K
Mizar MSE  version for both MS DOS and Unix.
Original site  University of Alberta, CA. Maintained by
Piotr Rudnicki. (Instruction for Unix is to be added later.)
msealbe.exe 85 K
msealbe.zip 79 K

To the top
of this page
Title Page
