ENHANCED PROCESSING OF ADJECTIVES IN MIZAR

• Authors: Naumowicz Adam
• Languages of publication: EN

Abstracts

EN

As adjectival notions are ubiquitous in informal mathematics, their important role must also be reflected in formal attempts to reconstruct the existing body of mathematical texts. In this paper we describe an enhancement of the Mizar proof checker which enables a more complete automation of notions encoded as adjectives. The proposed improvement concerns the Equalizer - Mizar's module responsible for handling equality, where adjective registrations can be re-used by matching them with classes of equal terms in order to add extra information to inference steps.

Keywords

EN

ADJECTIVES; MIZAR; PROOF AUTOMATION

Discipline

• LIBRARY_&_INFORMATION_SCIENCE: LIBRARY & INFORMATION SCIENCE

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

Contributors

author

Naumowicz Adam

• Adam Naumowicz, Institute of Computer Science, University of Bialystok, Poland

Identifiers

CEJSH db identifier

11PLAAAA10167