GRAMMATICA PER QUERY SU DOCUMENTI MATEMATICI
MATHEMATICAL QUERY LANGUAGE (MathQL) 

<query> := <list>                              (* clausola iniziale *)

<list> := ( <list> )                           (* parentesizazione *)
       |  <list> UNION <list>                  (* unione *)
       |  <list> INTERSECT <list>              (* intersezione *)
       |  <list> DIFF <list>                   (* differenza *)
       |  SELECT <rvar> IN <list> WHERE <bool> (* selezione *)
       |  EXISTS <rvar> IN <list> WHERE <bool> (* esistenziale *)
       |  USE <list> POSITION <svar>           (* unione lista backward *)
       |  USEDBY <list> POSITION <svar>        (* unione lista forward *)
       |  CONTRUCTORS <list>                   (* unione costruttori della 
						  lista oggetti*)
       |  PATTERN <pattern>                    (* espansione del pattern *)
       |  INTHEORY <list> ITEMTYPE <svar>      (* unione oggetti lista teorie *)
       |  THEORYREFTO <list>                   (* unione teorie che fanno 
                                                 riferimento a lista oggetti *)
       |  <list> OFTYPE <svar>		       (* unione oggetti in base a 
                                                  classi *)
       |  <list> OFSUPERTYPE <svar>	       (* unione oggetti in base a 
                                                  classi e loro superclassi *)
       |  <list> OFSUBTYPE <svar>	       (* unione oggetti in base a 
                                                  classi e loro sottoclassi *)

<bool> := ( <bool> )                           (* parentesizzazione *)
       |  <bool> AND <bool>                    (* congiunzione *)
       |  <bool> OR <bool>                     (* disgiunzione *)
       |  NOT <bool>                           (* negazione *)
       |  TRUE                                 (* vero *)
       |  FALSE                                (* falso *)
       |  <string> IS <string>                 (* case sensitive matching *)
       
<pattern> := <"-quoted-constant-string>        (* pattern costante *)
          
<string> := <'-quoted-constant-string>         (* costante letterale *)
         |  CONCLUSION | HYPOTHESIS | BODY     (* costanti simboliche *)
         |  MAINCONCLUSION | MAINHYPOTHESIS
         |  <rvar>                             (* variabile *)
	 |  <svar>			       (* variabile *)
	 |  <function> <rvar>                  (* applicazione di funzione *)
	 
<function> := NAME			       (* URIREF -> nome_oggetto *)
	   |  <property>

<property> := THEORY                           (* URIREF -> valore_Proprieta' *)
           |  TITLE			       (* URIREF -> valore_Prop_DC *)
           |  CONTRIBUTOR
           |  CREATOR
           |  PUBLISHER
           |  SUBJECT
           |  DESCRIPTION
           |  DATE
           |  TYPE
           |  FORMAT
           |  IDENTIFIER
           |  LANGUAGE
           |  RELATION
           |  SOURCE
           |  COVERAGE
           |  RIGHTS
	   |  INSTITUTION
	   |  CONTACT
	   |  FIRSTVERSION
	   |  MODIFIED
           |  <refineprop> <property>

<refineprop> := SUB			       (* proprieta' e sotto-proprieta'
                                                  di *) 
             |  SUPER			       (* proprieta' e super-proprieta'
                                                  di *)

<rvar> := <not-reserved-identifier>            (* variabile per risorse *)
<svar> := $ <not-reserved-identifier>          (* variabile per stringhe *)

- le stringhe sono "case sensitive" 
- la funzione non definita sull'argomento restituisce la stringa nulla
- le <rvar> si presuppongono essere istanziate come URI references costituite
  da un URI e da un fragment identifier opzionalecomplete; esse identificano 
  risorse 
- ogni binding lega una variabile libera (nuova) 
- Precedenza operatori:
  NOT (+)  DIFF
  AND      INTERSECT
  OR  (-)  UNION
- Possibili tipi di RELATION e DEPENDENCE sono rappresentati dalle loro
  subproperties
- FUTURO: thesauri di parole e sinonimi per ricerche testuali, ordinamenti sui 
  risultati, caratteri jolly. Una volta reperito l'oggetto si possono 
  visualizzare le info associate. 
- FUTURO: in output numeri ad esempio a fini statistici, aggiungendo anche 
  operatori aritmetici e di confronto (< = >). Es. Quante proofs di un certo 
  teorema ci sono? 
- L'ordinamento di default e' quello alfabetico crescente in base al nome 
  delle rvar
- Note su <pattern>
  Contiene un'espressione regolare per selezionare delle "reference" 
  (cioe` delle uri eventualmente seguite da un fragment identifier)
  L'espressione regolare contiene i seguenti costrutti:

  costrutto        semanticamente fa match con                       
  ?                un singolo carattere diverso da / # :             
  *                la piu' lunga sottostringa che non contiene / # : 
  **               la piu' lunga sottostringa che non contiene # :
  altro carattere  solo se' stesso

  costrutto        puo' appareire in
  ?                "body"
  *                dovunque
  **               "body" e "fragment"
  altro carattere  dovunque

  "body"     parte compresa fra le occorrenze di ":/" e "#1" escluse
  "fragment" parte successiva all'occorrenza "#1"
- FUTURO: operatore di ordinamento sul risultato finale della query.
  <query> SORTEDBY <order> <function>   (* unione lista ordinata secondo
                                           ordine e valore funzione *)
  <order>    := DESC                           (* ordinamento decrescente *)
	     |  ASC			       (* ordinamento crescente *)     
  DTD:
  <!ENTITY % order '(ascendant|descendant)'>
  <!ELEMENT Query %queryexpr;>
  <!ELEMENT SortBy (Query, SortField)>
  <!ELEMENT SortField %functexpr;>
  <!ATTLIST SortField 
            order %order; #IMPLIED>
- RILASSAMENTO degli operatori UNION e INTERSECT. Operatori fuzzy con 
  introduzione di pesi associati ai risultati.