[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
rigorous and formal proof
This below is the answer of Claus Zinn for my question concerning
difference between "rigorous" and "formal" proof.
-- Roman Matuszewski
(romat@mizar.org)
==================================================================
The difference between 'rigorous and 'formal' proofs is not that easy,
I guess. It may even be they that the english usage for these terms refer
to the same. One attempt would be:
- rigorous and formal proofs both are written in a formal
language
- the rigorous proof is written in a language above inference
level, independant of some calculus.
E.g., a MIZAR proof is a rigourous proof.
- the formal proof is written in a language at inference level
and the language depends only on the calculi used.
E.g. the resolution graph returned by OTTER is a proof in a
formal language.
Note that, as far as I understand MIZAR, the rigorous proof written
in the MIZAR language is never translated into a formal proof; because
MIZAR verifies the proof step by step; and for each step a formal
proof is found.
As a matter of fact, neither formal nor even rigorous proofs, as
defined above, can be find in mathematical textbooks. Mathematicians
have a different understanding of what a rigorous proof is: they say,
for example, that Landau gives a rigorous treatment in his book
'grundlagen der analysis' on analysis.
All the best,
Claus
--
/---------------------------------------------------------------------\
| Claus W. ZINN | F-A-University of Erlangen-Nuremberg |
| ================= | IMMD8 (Dept. of Artificial Intelligence) |
| | Am Weichselgarten 9 |
| STANDARD | 91058 Erlangen, F.R. of Germany |
| DISCLAIMER | Mail: zinn@immd8.informatik.uni-erlangen.de |
| | Phone: (+49) 9131 85-2-9911 |
| | Fax: (+49) 9131 85-2-9905 |
| |
| http://www8.informatik.uni-erlangen.de/IMMD8/staff/Zinn/ |
\---------------------------------------------------------------------/