!!!! SORRY FOR NOT HAVING COMPLETED THE TRANSLATION INTO ENGLISH AS YET !!!
-- ---------------------------------------------------------------------------

-- Prolog CLAUSE FILES USED TO PERFORM MAP EXPRESSION RECOGNITION (extension .pro):

mapEqualities -- il riconoscitore di formule ed espressioni mappali
mapEqExpand -- espande formule ed espressioni mappali riconosciute come benformate
	-- i principali predicati Prolog in questi due file sono:
	--		mapeq/1,2 -- riconosce gli enunciati mappali
	--			    -- (si tratta sempre di uguaglianze travestite)
	--		mapeq/3 -- riconosce gli enunciati mappali e li espande
	--			    -- i tre argomenti sono: equazione, contesto, espansione
	--		mapeq_meta/1,2 -- riconosce gli schemi di enunciato mappale
	--			    -- (si tratta sempre di uguaglianze travestite)
	--		mapeq_meta/3 -- riconosce gli schemi di enunciato mappale e li espande
	--		mapEq/3 -- riconosce gli enunciati mappali o i relativi schemi
	--			    -- (si tratta sempre di uguaglianze travestite)
	--		mapXpr/3 -- riconosce le espressioni  mappali o i relativi schemi
	--		mapxpr/1,2 -- riconosce le espressioni  mappali
	--		mapxpr/3 -- riconosce le espressioni mappali e le espande
	--			    -- i tre argomenti sono: espressione, contesto, espansione
	--		letter/4 -- il riconoscitore di lettere con pedice
	--		mapConfig/0 -- configura il linguaggio
	--			    -- e carica un po' di abbreviazioni ed assiomi
	--		matchNames/2 -- abbina i valori indefiniti in una lista di 
	--			    -- nomi di file ai nomi di default
	--		true/1	-- ha successo per una volta

nstallDefs -- installa uno o piu` file di definizioni
	-- i suoi principali predicati Prolog sono:
	--		installDefs(Infiles) -- carica, trasformandole ed 
	--			-- effettuando tutti i controlli sintattici del caso,
	--			-- abbreviazioni da uno o piu` files
	--		sameVars/2 -- test di "stessita`" tra variabili
	--		varsin/2 -- (che in molti Prolog gia` c'e`)
	-- 			-- l'individuazione di tutte le variabili che 
	-- 			--			compaiono in un termine Prolog
	--		isDef/2 -- definisce utilities per il semantic attachment

nstallAxs -- installa uno o piu` file di assiomi
	-- i suoi principali predicati Prolog sono:
	--		installAxs(Theory,Infiles) -- carica, abbinando ciascuno al
	--			-- nome della teoria (per default il nome del file 
	--			-- d'origine), assiomi mappali da uno o piu` file
	--		mkObj/2 -- riflette una formula con metavariabili di operatore
	--			--			sul livello oggetto

stubDefs -- definizioni usa-e-getta, e un'utile convenzione che rende le
	--		abbreviazioni di espressioni utilizzabili anche come
	--		abbreviazioni di formule
	-- i suoi principali predicati Prolog sono:
	--		rightSide/4 -- serve per i meccanismi definitori impliciti
	--				--	(relatori derivati da operatori o da teorie)
	--		namePrefix/3 -- scinde un identificatore in un prefisso ed un
	--				--	suffisso intercalati da un "_"

priorities -- fissa le priorita` degli operatori, che verranno poi installate
	--			tramite la setOps/0, le installa anche

letter -- utilities di analisi lessicale e sintattica:
	--	riconoscimento di lettere con pedice (letter/4)
	--	determinazione delle taglie di termini (size/3)
	--	determinazione delle variabili distinte in un termine (varsin/2)
	--	ridenominazione delle variabili in un termine (rename/2)
	--	coincidenza di variabili (sameVar/2)
	--	sostituzione di nomi di default ad effettivi mancanti (matchNames/2)

varsin -- contiene un predicato varsin/2 che puo` sostituire quello (piu`
	-- efficiente) di "nstallDefs" in ambienti Prolog dove quello non
	-- funzioni
  
-- ---------------------------------------------------------------------------

-- Prolog TOOLS USED FOR PREDICATIVE FORMULA HANDLING (extension .pro):

quantified -- schema generale di traduzione di formule diadiche del prim'ordine nel
	--	calcolo mappale, basato su quasi-proj coniugate;
	-- riconoscitore/normalizzatore di formule diadiche del prim'ordine
	--	(basato su sintassi, almeno per il momento, piuttosto cruda)
	-- i suoi principali predicati Prolog sono:
	--		translquant/5 -- supporta la traduzione di formule predicative
	--				--	in espressioni mappali
	--		quantifmla/3 -- riconosce e normalizza le formule predicative
	--				--	diadiche
	--		varlist/1 -- riconosce una lista che rappresenta variabili indiv.
	--		incrlist/2 -- verifica che una lista sia strettam. crescente,
	--				--	e in caso contrario, dopo un avvertimento,
	--				--	provvede a riordinarla
	--		addmerge/3 -- effettua la fusione di due liste crescenti in una
	--				--	nuova lista crescente formata da tutti
	--				--	e soli gli elementi delle due
	--		submerge/3 -- effettua differenza ed intersezione di due liste
	--				--	crescenti in due nuove lista crescenti

-- ---------------------------------------------------------------------------

-- Prolog TOOLS USED FOR MAP EXPRESSION HANDLING (extension .pro):

mapEqExpand -- see above

printlaws	-- stampa la lista degli assiomi, regole definizioni di una singola
			--	teoria; l'invocaz. si puo` fare in tre modi:
			--		printlaws(ThName,OuFile)
			--		printlaws(ThName) (sottinteso il file user),
			--		printlaws (sottinteso il calcolo ed il file user)
		-- stampa l'elenco di tutte le teorie che sono state caricate, se
			--	viene invocata printtheories

echo		-- trascrive in fomato LaTeX la lista degli assiomi o 
			--	delle definizioni estratte da un file caricabile
			--	con installDefs o con installAxs  
		-- il suo principale predicato Prolog e`:
			--	prettyecho/1 -- dove il parametro e` il nome del file

pretty	-- pretty printer guidato da una lista di precedenze di operatori
			--	(per esempio quelle fornite nel file prionew) e da
			--	regole su come trascrivere i simboli in LaTeX

ugly -- [...DA COMPLETARE...]

diagnose -- predicati per la gestione dei diagnostici

error	-- elenco dei diagnostici

-- ------------------------------------------------------------------------

-- FILES containing VERSIONS OF MAP CALCULUS
-- (these will be converted into Prolog clauses, which will define primitive
-- symbols as well as secondari constructs of `idiolects' of map calculus)

defAs0A -- simboli della dotazione iniziale (scelta n.1)
defAs0B -- simboli della dotazione iniziale (scelta n.2)
defAs0C -- simboli della dotazione iniziale (scelta n.3, come in [TG87])

defAs1 -- costrutti mappali secondari (prima serie):
		--	pur non essendo primitivi saranno fondamentali
		--	(inclusi alcuni variadici come unione, intersezione, 
		--	prodotto di liste)
defFoAs0 -- simboli secondari (seconda serie):
		--	alcuni banali, ma fondamentali, travestim. ddell'uguaglianza
defFoAs1 -- simboli secondari (terza serie):
		--	alcuni connettivi proposizionali, monadici diadici variadici

defProps -- caratterizzazione di alcune proprieta` di mappe

defGraphIsom -- caratterizzazione di isomorfismo tra due grafi 

defAttrs -- caratterizzaz. di entita`, attributi, chiavi, segnaposto, ecc.

defProj -- (quasi-)proiezioni, caratterizzaz. delle operaz. sulle tuple

defInd -- definizione di alcune teorie basilari, culminanti nell'induzione

defALL -- mare magnum di tutte quante le definizioni

defPlH   -- caratterizzazione di entita` "segnaposto" (ma e` migliore quella in defAttrs) 

defCardUniv -- caratterizzazione di diverse possibili cardinalita` del dominio del discorso

defAndrea -- selezione di definizioni effettuata per Andrea Formisano

defErnst -- selezione di definizioni effettuata per Ernst Doberkat

defStar -- file di definizioni per espressioni regolari

defMonoid -- file di definizioni includente quella di monoide

defTMP -- file di definizioni in prova

logicalA -- assiomi logici mappali compatibili con la scelta defAs0A

logicalB -- (!!ancora da scrivere!!) 
		--	assiomi logici mappali compatibili con la scelta defAs0B

logicalC -- assiomi logici mappali desunti dal Tarski-Givant
		--	(compatibili con la scelta defAs0B)

regular -- assiomi logici sui linguaggi regolari

ax_graphIsom -- assiomi su un isomorfismo fra due grafi

axGraphIsom -- assiomi su vari isomorfismi tra grafi
		--	(variante, basata su defGraphIsom, di ax_graphIsom)

ax_tenseLogic -- assiomi sulla logica del passato e del futuro

ax_HdTl -- assiomi su proiezioni coniugate in un universo privo di individui

ax_sets -- assiomi di una teoria equazionale degli insiemi senza individui

ax_sets_ur -- assiomi di una teoria equazionale degli insiemi dotata di individui

ax_nats -- assiomi sui numeri naturali (da completare)

ax_plh -- assiomi su un predicato subdiagonale segnaposto in una lista di altri predicati

ax_nested -- es. illustrativo di come i file di assiomi si possano includere uno nell'altro

	ax_key -- assiomi su alcuni attributi che formano una (super)chiave

ax_ER -- rappresentazione mappale di un semplice schema Entita`-Relazione
 
axErnst -- variante di "ax_key" e di "ax_plh", preparata per Ernst Doberkat

	ax_HdTl_r -- variante del precedente ax_HdTl, inclusa in axErnst
	ax_plH0 -- porzione inclusa in axErnst

-- ------------------------------------------------------------------------

-- IN ORDER TO LAUNCH THE SYSTEM CONSTITUITED BY THE ABOVE-LISTED FILES
-- (or of any more personal and eccentric dialect):

-- * create file containing personal definitions (if needed),
--		taking as models the above-listed def* files 

-- * create file containing logical and proper axioms,
--		taking as models the above-listed ax* files

-- * launch the Prolog program 'VIA',
--		and then proceed into configuration 

-- ------------------------------------------------------------------------