Mizar syntax

-- AdamNaumowicz - 2015-09-16

A number of updates to the grammar

-- GrzegorzBancerek - 2012-11-18

New syntax of postqualification; multipredicate format

-- GrzegorzBancerek - 13 Jun 2009

Adjective with arguments, no predicative synonyms/antonyms for adjective formulae, canceled registrations.

-- GrzegorzBancerek - 12 Dec 2007

Redefinition-Block cannot repeat (it is intention, not practice(?)). In Identify-Registration, the intention is to use Loci after "when". In Predicate-Definition [ "correctness" ... ] changed to Correctness-Conditions.

-- MichaelNedzelsky - 13 Apr 2007

Thanks to Adam Grabowski, the Mizar grammar has been corrected ("identify" rule was added).

Also the name of xml grammar file has been changed from mizar.xml to syntax.xml in order to avoid confusion with the Mizar.xml file, which is already in the Mizar distribution.

-- MichaelNedzelsky - 27 Oct 2006

The optional label has been added at the beginning of the Iterative-Equality production rule.

-- MichaelNedzelsky - 26 Oct 2006

The following rules were changed in order to support predefined mode "set", functor brackets "{", "[", "}", "]" and predicate "=":

Mode-Symbol, Left-Functor-Bracket, Right-Functor-Bracket, Predicate-Symbol.

-- MichaelNedzelsky - 23 Oct 2006

The following rules were changed:

Definitional-Block, Attribute-Definition, Cluster-Registration, Functorial-Registration.

The nonterminal Canceled-Registration was added to the grammar.

-- GrzegorzBancerek - 17 Oct 2006

Initial posting of xml files.

  • syntax.xml: Mizar syntax according to grammar.dtd

TopicClassification Select one...

ImplementationDate? N/A
Topic attachments
I Attachment Action Size Date Who Comment
elsedtd grammar.dtd manage 1.7 K 2006-10-17 - 12:19 GrzegorzBancerek DTD for grammars
xslxsl grammar2ntxt.xsl manage 8.0 K 2006-10-17 - 12:26 GrzegorzBancerek XML grammar to plain text transformation stylesheet
xslxsl grammar2thtml.xsl manage 13.0 K 2006-10-17 - 12:22 GrzegorzBancerek XML grammar to HTML with tables transformation stylesheet
xmlxml mizar-grammar.xml manage 45.4 K 2012-11-18 - 14:00 GrzegorzBancerek  
xmlxml syntax.xml manage 44.4 K 2015-09-16 - 00:03 AdamNaumowicz An updated version of the Mizar grammar
Topic revision: r20 - 2015-09-16 - 00:10:47 - AdamNaumowicz
Mizar TWiki
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback