Re: Problems with Mizar have been resolved

[Grzegorz Bancerek <bancerek@math.uw.bialystok.pl>]

On Mon, 27 Apr 1998, Vedasystem wrote:

> Now I am going to use the Mizar system for checking a proof
> in the theory of context-free grammars.
> 
> Does anyone know about Mizar activity in this area? 

There is the article LANG1 entitled "Context-free Grammar - Part I"
available under URL:

   http://mizar.uw.bialystok.pl/JFM/Vol4/lang1.html

in which a context-free grammar is introduced as a Mizar structure GrammarStr
including 3 fields:
 carrier - the set of all symbols (terminal and non-terminal),
 Rules - the set of rules treated as a relation between
         symbols and finite sequences of symbols,
 InitialSym - an initial symbol.
The relation of derivability of a symbol sequence from another one is 
investigated in the article.

In the article DTCONSTR (On defining functions on trees) the context-free
grammar without initial symbol (DTConstrStr in Mizar notation) is used
to define the set of all parse trees of the grammar. Schemes of 
defining functions on that set by induction is presented, too. The terminal 
language of a grammar and an example: Peano naturals is given there.

DTConstrStr is used in the article SCM_COMP
to define arithmetic expressions as binary trees. See also BINTREE1 where
"binary DTConstrStr" is introduced.

In this manner, the free manysorted algebra over a manysorted signature S 
is constructed by usage of context-free grammar related to the signature S
and a (manysorted) set of variables, see MSAFREE. 


Grzegorz Bancerek