helm/dtd/maththeory.dtd

   1 <?xml encoding="ISO-8859-1"?>
   2
   3 <!--*****************************************************************-->
   4 <!-- DTD FOR THEORY OBJECTS AT LEVEL OF CIC XML FILES:               -->
   5 <!-- First draft: May 10 2000, Claudio Sacerdoti Coen, Irene Schena  -->
   6 <!--*****************************************************************-->
   7
   8 <!-- manca il semplice enunciato -->
   9 <!-- mancano i link ad altre teorie? (corrispondenti a Require?) -->
  10 <!-- una teoria "vuota" e' una teoria? -->
  11 <!ENTITY % mathstructure '(THEOREM|LEMMA|COROLLARY|AXIOM|FACT|DEFINITION|
  12                            VARIABLE|SECTION)*'>
  13
  14 <!ELEMENT Theory (%mathstructure;)>
  15 <!ATTLIST Theory
  16           uri CDATA #REQUIRED>
  17
  18 <!ELEMENT THEOREM EMPTY>
  19 <!ATTLIST THEOREM
  20           id  IDREF #REQUIRED
  21           uri CDATA #REQUIRED>
  22
  23 <!ELEMENT LEMMA EMPTY>
  24 <!ATTLIST LEMMA
  25           id     IDREF #REQUIRED
  26           uri    CDATA #REQUIRED
  27           target IDREF #REQUIRED>
  28
  29 <!ELEMENT COROLLARY EMPTY>
  30 <!ATTLIST COROLLARY
  31           id     IDREF #REQUIRED
  32           uri    CDATA #REQUIRED
  33           target IDREF #REQUIRED>
  34
  35 <!ELEMENT AXIOM EMPTY>
  36 <!ATTLIST AXIOM
  37           id  IDREF #REQUIRED
  38           uri CDATA #REQUIRED>
  39
  40 <!ELEMENT FACT EMPTY>
  41 <!ATTLIST FACT
  42           id  IDREF #REQUIRED
  43           uri CDATA #REQUIRED>
  44
  45 <!ELEMENT DEFINITION EMPTY>
  46 <!ATTLIST DEFINITION
  47           uri CDATA #REQUIRED>
  48
  49 <!ELEMENT VARIABLE EMPTY>
  50 <!ATTLIST VARIABLE
  51           uri CDATA #REQUIRED>
  52
  53 <!ELEMENT SECTION (%mathstructure;)>
  54 <!ATTLIST SECTION
  55           uri CDATA #REQUIRED>
  56
  57 <!--
  58  VINCOLI DI VALIDITA' NON ESPRIMIBILI NEL DTD:
  59   Siano V una variabile e T,T' due fatti/definizioni/teoremi/lemmi/corollari
  60
  61    - per visualizzare T dipendente da T' dove T' e T sono definiti nella stessa
  62      (da definirsi) teoria/sezione, debbo visualizzare anche T'?
  63    - per visualizzare T dipendente da T' dove anche T' e' visualizzato, debbo
  64      visualizzare T necessariamente dopo T'?
  65    + consistenza fra la dipendenza dei lemmi e dei corollari dal loro target
  66      e quella effettiva data dal livello degli oggetti
  67    + tutte le URI debbono essere relative e discendenti (= non contenti "..")
  68    +? ogni lemma deve precedere (strettamente?) il suo target
  69    +? ogni corollario deve seguire (strettamente?) il suo target
  70    + se T/V dipende da V, allora V deve essere visualizzata
  71    + se T/V dipende da V, allora V deve essere visualizzata prima di T
  72     PROBLEMA: NON ABBIAMO INFORMAZIONI SULLA DIPENDENZA DI V DA V!!!
  73 -->