Full-text resources of CEJSH and other databases are now available in the new Library of Science.
Visit https://bibliotekanauki.pl

Results found: 4

first rewind previous Page / 1 next fast forward last

Search results

Search:
in the keywords:  MIZAR
help Sort By:

help Limit search:
first rewind previous Page / 1 next fast forward last
1

ENHANCED PROCESSING OF ADJECTIVES IN MIZAR

100%
Naumowicz A.
Studies in Logic, Grammar and Rhetoric
|
2009
|
issue 18(31)
89-101
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.
2

HOW TO DEFINE TERMS IN MIZAR EFFECTIVELY

100%
Kornilowicz A.
Studies in Logic, Grammar and Rhetoric
|
2009
|
issue 18(31)
67-77
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.
3

FORMALIZATION OF PROPOSITIONAL LINEAR TEMPORAL LOGIC IN THE MIZAR SYSTEM

100%
Giero M.
Studies in Logic, Grammar and Rhetoric
|
2010
|
issue 22(35)
7-21
EN
The paper describes formalization of some issues of propositional linear temporal logic (PLTL). We discuss encountered problems and applied solutions. The formalization was carried out in the Mizar system. In comparison with other systems, Mizar is famous for its large repository of computer checked mathematical knowledge and also for its user-friendly knowledge representation and proof language.
4

COMBINING MIZAR AND TPTP SEMANTIC PRESENTATION AND VERIFICATION TOOLS

100%
Urban J., Sutcliffe G., Trac S., Puzis Y.
Studies in Logic, Grammar and Rhetoric
|
2009
|
issue 18(31)
121-136
EN
This paper describes a combination of several Mizar-based tools (the MPTP translator, XSL style sheets for Mizar), and TPTP-based tools (IDV, AGInT, SystemOnTPTP, GDV) used for visualizing, analyzing, and independent verication of Mizar proofs. The combination delivers to the readers of the Mizar Mathematical Library (MML) an easy, powerful, and almost playful way of exploring the semantics and the structure of the library. The key factors for the relative easiness of having these functionalities are the choice of XML as both internal and external interface of Mizar, and the existence of a TPTP representation of MML articles. This shows the great added value that can be obtained by cooperation of several quite diverse (and quite often separately developed) projects, provided that they are based on the same communication standards.
first rewind previous Page / 1 next fast forward last
JavaScript is turned off in your web browser. Turn it on to take full advantage of this site, then refresh the page.