|
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 Lvov-Warsaw 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. Multi-Sorted [first-order 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 proof-checker 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, TeX-formatted, 40K
TeX, zip-condensed, 15K
TeX, arj-condensed, 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
proof-checker Mizar MSE.
Mizar MSE Introduction to Logic -- by Marcin
Mostowski
ASCII, TeX-formatted, 190K
TeX, zip-condensed, 52K
TeX, arj-condensed, 60K
PS, zip-condensed 113K.
This is a concise textbook but in two respects it goes far beyond a typical
course of logic. (i) It presents the proof-checker 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 computer-asisisted 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.
mse-bial.exe 88 K
mse-bial.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.)
mse-albe.exe 85 K
mse-albe.zip 79 K
|
To the top
of this page
Title Page
|
