HOW TO DEFINE TERMS IN MIZAR EFFECTIVELY

• Authors: Kornilowicz Artur
• Languages of publication: EN

Abstracts

EN

This paper explains how proofs written in Mizar can evolve if some dedicated mechanisms for defining terms are used properly, and how to write articles to fully exploit the potential of these mechanisms. In particular, demonstrated examples show how automatic expansion of terms and terms identification allow to write compact, yet readable proofs.

Keywords

EN

AUTOMATION; FORMAL PROOFS; MIZAR

Discipline

• LIBRARY_&_INFORMATION_SCIENCE: LIBRARY & INFORMATION SCIENCE

• Publisher: Sciendo
• Journal: Studies in Logic, Grammar and Rhetoric
• Year: 2009
• Issue: 18(31)
• Pages: 67-77
• Document type: ARTICLE

Contributors

author

Kornilowicz Artur

• Artur Kornilowicz, Institute of Computer Science, University of Bialystok, Poland

Identifiers

CEJSH db identifier

11PLAAAA10165