No. 3   -   S u m m e r   1 9 9 6    
http://www.pip.com.pl/MathUniversalis/3/index.html   --   ISSN 1426-3513



MATHESIS
u n i v e r s a l i s


In this Issue
Mizar MSE System - A Software for Logic




No.3   Contents
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