/*
	Universita' di Genova
	DISI - Dipartimento di Informatica e Scienze dell'Informazione
	---------------------------------------------------------------
	
	LaB: merge of Boole and Lawvere deductive calculi
	
	---------------------------------------------------------------
	giugno 2004 - febbraio 2005
	---------------------------------------------------------------
	
	v. 2.0.5.beta
	(con quantificatori)
	questa versione introduce l'applicazione delle regole derivate
	e introduce l'uso dell'esemplificazione e di teorie
	Aggiunge inoltre la possibilita' di esemplificare regole
	derivate, sia a ritroso -- come in programmazione logica --
	che in avanti -- tipico del passo 'per definizione'.
	
	Nel menu' merge, compare anche la caratterizzazione di
	equivalenza logica.
	La presente versione di LaB utilizza i seguenti simboli:
	
	equivalenza: l=| (<L minuscola><uguale><pipe>)
	conseguenza: l=
	
	simbolo di disgiunzione: | (<pipe>)
	
	forma del sequente: FORMULA <L minuscola> FORMULA

	sostituzione: [ \ ] (<quadra> TERMINE <backslash> VARIABILE <quadra>)
*/


/*-----------Enviroment variables----------------------*/
INITIALISE interpretpredicates true
MENU Edit
 CHECKBOX applyconjectures
   "Unproven theorems may be applied"
 INITIALLY
   false
 CHECKBOX showallproofsteps
   "Expand all proof branches" 
 INITIALLY
   true
END

/*------------Definizione Sintassi------------*/
CLASS BAG G H N O L M
CLASS FORMULA A B C D E F P Q R S T U V Z a b c d e f g h i j k o p q r s t 
CLASS VARIABLE u v w x y z m n

INFIX		110T		<=>
INFIX		110T		=>
INFIX		110T		&
INFIX		110T		 |
PREFIX	120		~

LEFTFIX	110		! .
LEFTFIX	110		? .

/*JUXTFIX	300*/
SUBSTFIX	400 [ t \ x ]
PREFIX 10 =
PREFIX 10 =|

CONSTANT  ff tt

BIND    x SCOPE P IN ? x . P
BIND    x SCOPE P IN ! x . P


/*--------- Def. di SEQUENT -----------*/

SEQUENT IS BAG l BAG

/*----------- Def passaggio da l=| a l= ----------*/
RULE "E-def" FROM A l= B AND B l= A INFER A l=| B

/*----------- Def passaggio da l= a l=| ----------*/
RULE "C-car" FROM A l=| B INFER tt l= A <=> B

/*--------- Tattiche applicative -----------*/

/*dispatcher: esegue equivTactic o conseqTactic in base al tipo di sequent 
  e termina jape in caso di sequent illegali*/
TACTIC dispatcher (equivTactic,conseqTactic) IS
(WHEN
	(LETGOAL (=|_P) equivTactic)
	(LETGOAL (=_P) conseqTactic)
	(ALERT(espressione illegale)) /* */ 
)

/*SxoDx: applica Dx rule se la selezione e' a dx o Sx rule se la selezione e' a sx*/
TACTIC  SxoDx(Sx, Dx, rule) IS
(LAYOUT "%s" (1)
	(WHEN
		(LETHYPSUBSTSEL  _P (WITHSUBSTSEL Sx) rule)
		(LETCONCSUBSTSEL _P (WITHSUBSTSEL Dx) rule)
		(LETHYP          _P (Sx _P) rule)
		(LETCONC         _P (Dx _P) rule)
	)
)

/*checkSel: controlla la selezione dell'utente, se la selezione e' corretta fallisce,
  se la selezione e' errata avvisa l'utente e termina con successo
  *** Si noti che dal momento questa tattica viene normalmente utilizzata in un blocco ALT
  il suo fallimento determina l'esecuzione della tattica successiva, mentre il suo successo
  determina la fine dell'esecuzione.***
  msgSel: e' ausiliaria*/
TACTIC checkSel IS
(WHEN
	(LETARGSEL Z FAIL)
	(LETARGSEL (=|_P) msgSel)
	(LETARGSEL (=_P) msgSel)  
	(LETCONC (=|_P) (WHEN
						(LETARGSEL _P FAIL)
						msgSel
					)) 
	(LETCONC (=_P) (WHEN
						(LETARGSEL _P FAIL)
						msgSel
					)) 
	FAIL 
)
TACTIC msgSel IS
(ALERT(selezione non corretta))


/*applyE: esegue le operazioni di default per l'applicazione di
un'equivalenza (con sostituzione)*/
TACTIC applyE(rule) IS
(ALT
 checkSel
 (dispatcher
	(ALT
		rule
		(SxoDx "sostituzione inversa a sinistra" "sostituzione inversa a destra" rule)
		(SxoDx "sostituzione a sinistra" "sostituzione a destra" rule)
	)
	
	(ALT
		(SxoDx "sostituzione inversa per equivalente a sinistra" "sostituzione inversa per equivalente a destra" rule)
		(SxoDx "sostituzione per equivalente a sinistra" "sostituzione per equivalente a destra" rule)
	)
  )
)

/*applyC: esegue le operazioni di default per l'applicazione di una conseguenza (ex onlyC)*/
TACTIC applyC(rule) IS
(dispatcher
	(ALERT(comando non valido su EQUIVALENZE))
	rule
)

/*Compl e ApplicaC: passaggio per transitiva automatico*/
TACTIC Compl(Rule) IS (ALT (PROVE Rule "riflessiva")
                           (PROVE (SEQ "transitiva" Rule))
                           Rule)  
TACTIC ApplicaC(Rule) IS 
 (ALT	Rule
	(SEQ transitiva Rule)
        (LETGOALPATH G "transitiva"
		(GOALPATH (SUBGOAL G 1)) Rule (GOALPATH G) NEXTGOAL))

TACTIC instance(rule) IS (ALT
				(WITHSELECTIONS rule)
				(rule))

/*co2im: trasforma un conseguenza della forma A l= B in una della forma tt l= A=>B*/
TACTIC co2im IS
			(SEQ
			 (LAYOUT "%s" (1) "transitiva") 
			 "&-in" 
			 "tt-in" 
			 "riflessiva" 
			 "=>-out" 
			)
			
/*im2coSingle: trasforma una conseguenza della forma tt l= A=>B in una della forma A l= B*/
TACTIC im2coSingle IS
			(SEQ
			 "=>-in"
			 (LAYOUT "%s" (1) "transitiva") 
			 "&-out2"
			 "riflessiva"
			)

/*im2co: applica im2coSingle a una congiunzione n-aria di implicazioni, utilizzata per spezzare gli antecedenti multipli nelle in-line inference*/
TACTIC im2co IS
			(ALT
				(
					(LETGOALPATH G "&-in"
						(GOALPATH (SUBGOAL G 1))
				   		im2co
				   		(GOALPATH G) NEXTGOAL
					)
					im2co
				)
				im2coSingle
			)

/*applyInLineInference: applica un'in-line inference ad n antecedenti
applyILI: e' ausiliaria e non e' da usarsi direttamente*/
TACTIC applyInLineInference(Rule) IS (applyC (applyILI Rule))
TACTIC applyILI(Rule) IS 
				(SEQ 
					 co2im 
					 (LAYOUT "%s" (0) (LETGOALPATH G "transitiva"
						(GOALPATH (SUBGOAL G 1)) Rule (GOALPATH G) NEXTGOAL
					 ))
					 im2co
				)

/*applyAsAnExample: applica un'esemplificazione a 1,2,3,4,5,6 variabili
applyAsAProperty: applica un'esemplificazione usando
'applyAsAnExample' su un conseguente generico prodotto mediante
'transitiva' 
applyAA*: sono ausiliarie e non sono da usarsi singolarmente*/

TACTIC applyAsAProperty(Rule) IS (applyC (applyAAAP Rule))
TACTIC applyAAAP(Rule) IS
        (ALT 
             (LAYOUT (Rule) (1) (SEQ transitiva (applyAAEAll Rule) ("riflessiva")))
             (SEQ transitiva (applyAAEAll Rule))
        )

TACTIC applyAsAnExample(Rule) IS (applyC (applyAAEAll Rule))
TACTIC applyAAEAll(Rule) IS 
	(ALT
		(applyAAE Rule)
		(LAYOUT (Rule) (0) 
			(LETGOALPATH G "transitiva"
			(GOALPATH (SUBGOAL G 1)) (applyAAEwithAntecedents Rule) (GOALPATH G) NEXTGOAL)
		)
		(applyAAE Rule)
		
	)
TACTIC applyAAE(Rule) IS
            (ALT
                (applyAAEwithSpecific esempio Rule)
                (applyAAEwithSpecific "2esempi" Rule)
                (applyAAEwithSpecific "3esempi" Rule)
         		(applyAAEwithSpecific "4esempi" Rule)
         		(applyAAEwithSpecific "5esempi" Rule)
                (applyAAEwithSpecific "6esempi" Rule)
            )        

TACTIC applyAAEwithSpecific(Example, Rule) IS
	(PROVE(SEQ (LAYOUT (Rule) () 
		(LETGOALPATH G "transitiva" 
            	(GOALPATH (SUBGOAL G 1)) (Example) (GOALPATH G) NEXTGOAL)) Rule))

TACTIC applyAAEwithAntecedents(Rule) IS
	(SEQ co2im (applyAAE Rule))
	
	
/*-------- REGOLE ----------*/

/* Introduzione di una teoria: bottone per marcare come assioma una conseguenza */
RULE	"Axiom"				INFER  P l= Q


/*SOSTITUTIVE*/
/*per equivalenze*/
RULE    "sostituzione a destra"(P, OBJECT x)
  FROM  Q l=| P AND S l=| R[ Q \ x ] INFER   S l=| R[ P \ x ]
RULE    "sostituzione inversa a destra"(P, OBJECT x)
  FROM  P l=| Q AND S l=| R[ Q \ x ]  INFER  S l=| R[ P \ x ]
RULE    "sostituzione a sinistra"(P, OBJECT x)
  FROM  Q l=| P AND R[ Q \ x ] l=| S  INFER   R[ P \ x ] l=| S
RULE    "sostituzione inversa a sinistra"(P, OBJECT x)
  FROM  P l=| Q AND R[ Q \ x ] l=| S  INFER   R[ P \ x ] l=| S

/*per conseguenze*/ 
RULE "sostituzione inversa per equivalente a destra"(P, OBJECT x)
  FROM P l=| Q AND D l= R[Q\x] INFER D l= R[P\x]
RULE "sostituzione per equivalente a destra"(P, OBJECT x)
  FROM Q l=| P AND D l= R[Q\x] INFER D l= R[P\x]
RULE "sostituzione inversa per equivalente a sinistra"(P, OBJECT x)
  FROM P l=| Q AND R[Q\x] l= D INFER R[P\x] l= D
RULE "sostituzione per equivalente a sinistra"(P, OBJECT x)
  FROM Q l=| P AND R[Q\x] l= D INFER R[P\x] l= D

 
/*---------- Definizioni di Boole ---------*/
RULE "E-transitiva"(Q) FROM P l=| Q AND Q l=| R INFER P l=| R

RULE "~ e' l=|-funzionale"(P,Q) FROM P l=| Q INFER ~P l=| ~Q
RULE "& e' l=|-funzionale"(P,Q,R,S) FROM P l=| Q AND R l=| S INFER P&R l=| Q&S
RULE "=> e' l=|-funzionale"(P,Q,R,S) FROM P l=| Q AND R l=| S INFER P=>R l=| Q=>S
RULE "<=> e' l=|-funzionale"(P,Q,R,S) FROM P l=| Q AND R l=| S INFER P<=>R l=| Q<=>S
RULE "| e' l=|-funzionale"(P,Q,R,S) FROM P l=| Q AND R l=| S INFER P | R l=| Q | S
RULE "? e' l=|-funzionale"(P,Q) FROM P l=| Q INFER ?x. P l=| ?x. Q
RULE "! e' l=|-funzionale"(P,Q) FROM P l=| Q INFER !x. P l=| !x. Q

/*---------- Definizioni di Lawvere ---------*/
RULE	riflessiva				INFER P l= P
RULE    transitiva(T) FROM P l= T AND T l= R	INFER P l= R
RULE    passante(t,OBJECT x) FROM P l= Q	INFER P[t\x] l= Q[t\x]
RULE    motore	FROM ~P l= Q 		INFER ~Q l= P
RULE	"&-in"(E,F)	FROM R l= E AND R l= F	INFER R l= E&F
RULE	"&-out1"(F)	FROM R l= P&F		INFER R l= P
RULE	"&-out2"(E)	FROM R l= E&Q		INFER R l= Q
RULE	"=>-in"(U,V)	FROM R&U l= V	INFER R l= U=>V
RULE	"=>-out"(U,V)	FROM R l= U=>V         	INFER R&U l= V
RULE	"tt-in"				INFER R l= tt
RULE	"ff-in"				INFER ff l= P
RULE	"~-def a destra"(P)	FROM R l= P=> ff	INFER R l= ~P
RULE	"~-def a sinistra"(P)	FROM P=> ff l= Q	INFER ~P l= Q
RULE	"<=>-def a destra"	FROM R l= (P=>Q)&(Q=>P)	INFER R l= P<=>Q
RULE	"<=>-def a sinistra"	FROM (P=>Q)&(Q=>P) l= R	INFER P<=>Q l= R
RULE	"|-out1"(A,B)  FROM A | B l= R		INFER A l= R
RULE	"|-out2"(A,B)  FROM A | B l= R		INFER B l= R
RULE	"|-in"(A,B) FROM A l= R AND B l= R	INFER A | B l= R

TACTIC "tt-out" IS (SEQ "=>-in" "transitiva" "&-out2" "riflessiva")

RULE	"!-in"	WHERE x NOTIN R FROM R l= P		INFER R  l= ! x.P
RULE	"!-out"(OBJECT x) WHERE x NOTIN R FROM R l= ! x.P	INFER R  l= P
RULE	"?-in"	WHERE x NOTIN R FROM P l= R		INFER ? x.P  l= R
RULE	"?-out"(OBJECT x) WHERE x NOTIN R FROM ? x.P  l= R	INFER P  l= R

/*---------------- AUTOMATCH ----------------*/
AUTOMATCH "E-riflessiva"
AUTOMATCH involutiva
/*AUTOMATCH "co-involutiva"
*/
AUTOMATCH riflessiva
AUTOMATCH "tt-in"
AUTOMATCH "ff-in"

AUTOMATCH "Modus Ponens"
AUTOMATCH "P&(P=>Q) l= Q"

/*------------------- HIT -------------------*/
HYPHIT ~P l=| ~Q IS "~ e' l=|-funzionale"
CONCHIT ~P l=| ~Q IS "~ e' l=|-funzionale"

HYPHIT P&R l=| Q&S IS "& e' l=|-funzionale"
CONCHIT P&R l=| Q&S IS "& e' l=|-funzionale"

HYPHIT P=>R l=| Q=>S IS "=> e' l=|-funzionale"
CONCHIT P=>R l=| Q=>S IS "=> e' l=|-funzionale"

HYPHIT P<=>R l=| Q<=>S IS "<=> e' l=|-funzionale"
CONCHIT P<=>R l=| Q<=>S IS "<=> e' l=|-funzionale"

HYPHIT P | R l=| Q | S IS "| e' l=|-funzionale"
CONCHIT P | R l=| Q | S IS "| e' l=|-funzionale"

HYPHIT ?x. P l=| ?x. Q IS "? e' l=|-funzionale"
CONCHIT ?x. P l=| ?x. Q IS "? e' l=|-funzionale"

HYPHIT !x. P l=| !x. Q IS "! e' l=|-funzionale"
CONCHIT !x. P l=| !x. Q IS "! e' l=|-funzionale"

HYPHIT	P   l= P	IS applyC riflessiva	     
HYPHIT	P&Q l= P	IS applyC (SEQ "&-out1" "riflessiva")
HYPHIT	P&Q l= Q	IS applyC (SEQ "&-out2" "riflessiva")
HYPHIT  R&P l= Q	IS applyC (Compl "=>-out")
HYPHIT	P  |  Q  l= R	IS applyC "|-in"
HYPHIT	~P  l= Q	IS applyC "~-def a sinistra"	    
HYPHIT	P<=>Q l= R	IS applyC "<=>-def a sinistra"	  
HYPHIT	ff  l= P	IS applyC "ff-in" 
HYPHIT	! x.P  l= Q	IS applyC(Compl (instance "!-out"))
HYPHIT	? x.P  l= Q	IS applyC(Compl "?-in")

CONCHIT P l= Q&R	IS applyC "&-in"
CONCHIT Q  l= Q  |  R	IS applyC (SEQ "|-out1" "riflessiva")
CONCHIT R  l= Q  |  R	IS applyC (SEQ "|-out2" "riflessiva")
CONCHIT tt l= Q=>R	IS applyC "tt-out"     
CONCHIT P l= Q=>R	IS applyC (Compl "=>-in")
CONCHIT P l= ~Q	IS applyC "~-def a destra"
CONCHIT P l= Q<=>R	IS applyC "<=>-def a destra"
CONCHIT P l=! x.Q	IS applyC(Compl "!-in")
CONCHIT P l=? x.Q	IS applyC(Compl (instance "?-out"))

/*---------------- MENU -----------------*/
MENU "Lawvere"  IS
	ENTRY "riflessiva" IS applyC riflessiva
	ENTRY "transitiva" IS applyC transitiva
	ENTRY "passante" IS applyC(instance "passante")
	SEPARATOR
	ENTRY "motore" IS applyC motore
	SEPARATOR
	ENTRY "&-in" IS applyC "&-in"
	ENTRY "|-in" IS applyC(Compl "|-in")
	ENTRY "=>-in" IS applyC(Compl "=>-in")
	ENTRY "tt-in" IS applyC "tt-in"
	ENTRY "ff-in" IS applyC "ff-in"
	ENTRY "!-in" IS applyC(Compl "!-in")
	ENTRY "?-in" IS applyC(Compl "?-in")
	SEPARATOR
	ENTRY "&-out1" IS applyC(Compl "&-out1")
	ENTRY "&-out2" IS applyC(Compl "&-out2")
	ENTRY "|-out1" IS applyC(Compl "|-out1")
	ENTRY "|-out2" IS applyC(Compl "|-out2")
	ENTRY "=>-out" IS applyC(Compl "=>-out")
	ENTRY "!-out" IS applyC(Compl (instance "!-out"))
	ENTRY "?-out" IS applyC(Compl (instance "?-out"))
	SEPARATOR
	ENTRY "~-def a sinistra" IS applyC "~-def a sinistra"
	ENTRY "~-def a destra" IS applyC "~-def a destra"
	ENTRY "<=>-def a sinistra" IS applyC "<=>-def a sinistra"
	ENTRY "<=>-def a destra" IS applyC "<=>-def a destra"
END

MENU "merge" IS
	ENTRY "E-def" 
SEPARATOR
	ENTRY "C-car" 
END

MENU "Boole" IS 
  ENTRY "E-riflessiva" IS applyE "E-riflessiva"
  ENTRY "E-transitiva" IS applyE "E-trasitiva"
SEPARATOR
	ENTRY "involutiva" IS applyE "involutiva"
SEPARATOR
	ENTRY "associativa di &" IS applyE "associativa di &"
	ENTRY "commutativa di &" IS applyE "commutativa di &"
	ENTRY "assorbimento di &" IS applyE "assorbimento di &"
	ENTRY "distributiva di & su |" IS applyE "distributiva di & su |"
  	ENTRY "elemento neutro per &" IS applyE "elemento neutro per &"
  	ENTRY "De Morgan per &" IS applyE "De Morgan per &"
  	ENTRY "De Morgan per tt" IS applyE "De Morgan per tt"
SEPARATOR
  ENTRY "pseudocomplemento" IS applyE "pseudocomplemento"
SEPARATOR
	ENTRY "conservazione per ?" IS applyE "conservazione per ?"
	ENTRY "unita' per ?" IS applyE "unita' per ?"
	ENTRY "counita' per ?" IS applyE "counita' per ?"
	ENTRY "alfa-conversione per?" IS applyE "alfa-conversione per ?"
	ENTRY "Beck-Chevalley per ?" IS applyE "Beck-Chevalley per ?"
	ENTRY "De Morgan per ?" IS applyE "De Morgan per ?"
SEPARATOR
	ENTRY "Funzionalita'"
	ENTRY "per ~" IS "~ e' l=|-funzionale"
	ENTRY "per &" IS "& e' l=|-funzionale"
	ENTRY "per =>" IS "=> e' l=|-funzionale"
	ENTRY "per <=>" IS "<=> e' l=|-funzionale"
	ENTRY "per ?" IS "? e' l=|-funzionale"
SEPARATOR
	ENTRY "Definizione"
	ENTRY " per ~" IS applyE "~-def"
	ENTRY " per <=>" IS applyE "<=>-def"
END

MENU "d. Boole" IS 
	ENTRY "associativa di |" IS applyE "associativa di |"
	ENTRY "commutativa di |" IS applyE "commutativa di |"
	ENTRY "assorbimento di |" IS applyE "assorbimento di |"
	ENTRY "distributiva di | su &" IS applyE "distributiva di | su &"
	ENTRY "elemento neutro per |" IS applyE "elemento neutro per |"
	ENTRY "De Morgan per |" IS applyE "De Morgan per |"
	ENTRY "De Morgan per ff" IS applyE "De Morgan per ff"
SEPARATOR
	ENTRY "conservazione per !" IS applyE "conservazione per !"
	ENTRY "counita' per !" IS applyE "counita' per !"
	ENTRY "unita' per !" IS applyE "unita' per !"
	ENTRY "alfa-conversione per !" IS applyE "alfa-conversione per !"
	ENTRY "Beck-Chevalley per !" IS applyE "Beck-Chevalley per !"
	ENTRY "De Morgan per !" IS applyE "De Morgan per !"
SEPARATOR
	ENTRY "Funzionalita'"
	ENTRY "per |" IS "| e' l=|-funzionale"
	ENTRY "per !" IS "! e' l=|-funzionale"
END

/*---------------- PANNELLI -----------------*/
CONJECTUREPANEL "Lemmi"
  THEOREM	"Modus Ponens"	IS (P=>Q)&P  l= Q
  THEOREM	Scambio	IS P&Q  l= Q&P
  THEOREM	"P&(P=>Q) l= Q" IS P&(P=>Q) l= Q
  THEOREM	IS (P&Q)&R  l= P&(Q&R)
  THEOREM	IS P&(Q&R)  l= (P&Q)&R
  THEOREM	IS (P&Q) => R  l= P => (Q => R)
  THEOREM	IS P => (Q => R)  l= (P&Q) => R
  THEOREM	IS P  l= ~~P
  THEOREM	IS ~~P  l= P
  THEOREM	IS P&~P  l= ff
  THEOREM	IS Q  l= P => Q
  THEOREM	IS ~P  l= P => Q
  THEOREM	IS (~P) | Q  l= P => Q
  THEOREM	IS P & ~Q  l= ~(P => Q)
  THEOREM	zot	IS (P & ~Q) => ff  l= P => Q
  THEOREM	IS ~(P   |   (~P))  l= ff
  THEOREM	"Terzo Escluso"	IS tt  l= P   |   (~P)
  THEOREM	IS P=>Q  l= (~P)   |   Q
  THEOREM	IS ~(P  |  Q)  l= (~P)&(~Q)
  THEOREM	IS (P  |  Q)=>R  l= (P=>R)&(Q=>R)
  THEOREM	IS (P=>R)&(Q=>R)  l= (P  |  Q)=>R
  THEOREM	IS (P=>Q)&(P=>R)  l= P=>(Q&R)
  THEOREM esempio(P) IS ! x.P(x)			l= P(t)
  THEOREM "2esempi"(P) IS ! x.! y.P(x,y)			l= P(t,s)
  THEOREM "3esempi"(P) IS ! x.! y.! z.P(x,y,z)		l= P(t,s,r)
  THEOREM "4esempi"(P) IS ! x.! y.! z.! w.P(x,y,z,w)	l= P(t,s,r,p)
  THEOREM "5esempi"(P) IS ! x.! y.! z.! w.! u.P(x,y,z,w,u)	l= P(t,s,r,p,q)
  THEOREM "6esempi"(P) IS ! x.! y.! z.! w.! u.! v.P(x,y,z,w,u,v)	l= P(t,s,r,p,q,k)
  THEOREM IS		P(t)	l= ? x.P(x)
  BUTTON "Apply" IS Apply ApplicaC COMMAND
END

CONJECTUREPANEL Equivalenze IS
THEOREM "E-riflessiva" P l=| P
THEOREM "involutiva"(P) ~~P l=| P
/*THEOREM "co-involutiva"(P) IS P l=| ~~P
*/
THEOREM "associativa di &"(P,Q,R) P&(Q&R) l=| (P&Q)&R
THEOREM "commutativa di &"(P,Q) P&Q l=| Q&P
THEOREM "assorbimento di &"(P,Q) P&(Q | P) l=| P
THEOREM "distributiva di & su |"(P,Q,R) P&(Q | R) l=| (P&Q) | (P&R)
THEOREM "elemento neutro per &"(P) P & tt l=| P
THEOREM "De Morgan per &"(P,Q) ~(P & Q) l=| ~P | ~Q
THEOREM "De Morgan per tt" ~tt l=| ff
THEOREM "pseudocomplemento"(P,Q) P => Q l=| ~P | Q
THEOREM "~-def"(P) ~P l=| P => ff
THEOREM "<=>-def"(P,Q) P <=> Q l=| (P => Q) & (Q => P)
THEOREM "associativa di |"(P,Q,R) IS P | (Q | R) l=| (P | Q) | R
THEOREM "commutativa di |"(P,Q) IS P | Q l=| Q | P
THEOREM "assorbimento di |"(P,Q) IS P | (Q & P)   l=| P
THEOREM "distributiva di | su &"(P,Q,R) IS P | (Q & R)   l=| (P | Q) & (P | R)
THEOREM "elemento neutro per |"(P) IS P | ff  l=| P
THEOREM "De Morgan per |"(P,Q) IS ~ (P | Q)     l=| (~P)&(~Q)
THEOREM "De Morgan per ff" IS ~ ff     l=| tt
THEOREM "conservazione per ?"(P,Q) (? x. (P | Q)) l=| (? x .P) | (? x.Q)
THEOREM "unita' per ?"(P) P & (? x. P) l=| P
THEOREM "counita' per ?"(P) WHERE x NOTIN P IS (? x.P) l=| P
THEOREM "alfa-conversione per ?"(P) 
  IS ? x. P(x) l=| ? y. P(y)
THEOREM "Beck-Chevalley per ?"(P,Q) WHERE x NOTIN Q 
  IS ? x.(P & Q) l=| (? x. P) & Q
THEOREM "De Morgan per ?"(P) ~(? x. P) l=| (! x. ~P)
THEOREM "conservazione per !"(P,Q) IS (! x.(P & Q))   l=| (! x. P) & (! x. Q)
THEOREM "counita' per !"(P) IS P | (! x.P)   l=| P
THEOREM "unita' per !"(P) WHERE x NOTIN P 
        IS (! x.P)       l=| P
THEOREM "alfa-conversione per !"(P) 
        IS ! y.P(y) l=|  ! x. P(x)
THEOREM "Beck-Chevalley per !"(P,Q) WHERE x NOTIN Q
        IS (! x.( P | Q )) l=| (! x. P) | Q
THEOREM "De Morgan per !"(P) IS ~(! x. P)     l=| ? x. ~P
BUTTON "Apply" IS apply applyE COMMAND
END

CONJECTUREPANEL "Equivalenze utili"
THEOREMS proposizionali(P,Q,R) ARE
P & P l=| P AND
P | P l=| P AND
P & ~P l=| Q & ~ Q AND
P | ~P l=| Q | ~Q AND
(~Q)=>(~P) l=| P => Q AND
P => (~Q) l=| Q => (~P) AND
P => (Q=> R) l=| (P&Q)=> R AND
P => (Q=> R) l=| Q=>(P=> R) AND
P=>(Q&R) l=| (P=>Q)&(P=>R) AND
(P | Q)=>R l=|(P=>R)&(Q=>R) AND
R=>(P | Q) l=|(R=>P)|(R=>Q) AND
~(P=>Q) l=| P&(~Q) AND
(P=>Q)&P l=| P&Q AND
(~P)|(P&Q) l=| P=>Q AND
P<=>Q l=| (P&Q) | ((~P)&(~Q)) AND
~(P<=>Q) l=| (P&(~Q)) | ((~P)&Q) AND
~P l=| P=>(Q&~Q) AND
tt=>P  l=|  P AND
P=>P  l=|  tt AND
P | ~P  l=|  tt AND
P&~P  l=|  ff AND
P<=>P  l=|  tt AND
P<=>~P  l=|  ff AND
(P=>Q)&P  l=|  P&Q
END
THEOREM WHERE x NOTIN P IS P=>(!x.Q) l=| !x.(P=>Q)
THEOREM WHERE x NOTIN P IS (?x.Q)=>P l=| !x.(Q=>P)
THEOREM WHERE x NOTIN P IS P=>(?x.Q) l=| ?x.(P=>Q)
THEOREM WHERE x NOTIN P IS (!x.Q)=>P l=| ?x.(Q=>P)
BUTTON "Apply" IS apply applyE COMMAND
END

CONJECTUREPANEL "Funtorialita'"
THEOREMS connettivi(P,Q,R) ARE
 P=>Q		 l= (R & P)=>(R & Q) AND
 P=>Q		 l= (R   |   P)=>(R   |   Q) AND
 P=>Q		 l= (R => P)=>(R => Q) AND
 P=>Q		 l= (Q => R)=>(P => R) AND
 P=>Q		 l= ~Q => ~P 
END
THEOREMS quantificatori(OBJECT x,P,Q) ARE
 ! x.(P=>Q)	l= (! x.P)=>(! x.Q) AND
 ! x.(P=>Q)	l= (? x.P)=>(? x.Q)
END
BUTTON "Apply" IS Apply ApplicaC COMMAND
BUTTON "Apply as a Rule" IS Apply applyInLineInference COMMAND
END

CONJECTUREPANEL "Regole derivate"
THEOREMS proposizionali(P,Q,R,S) ARE
 (P & ~Q) => ff  l= P => Q AND
 (~Q)=>(~P) l= P => Q AND
 P => (~Q) l= Q => (~P) AND
 P => (Q=> R) l= Q=>(P=> R) AND
 ((P&Q)=>R)&(P=>Q)	l= P=>R AND
 (P=>R)&(Q=>S)	l= (P&Q)=>(R&S) AND
 (P=>R)&(Q=>S)	l= (P|Q)=>(R|S) AND
 tt => ~P  l= P => Q AND
 tt => Q  l= P => Q AND
 tt => (P=> Q)  l= P => Q AND
 (P=>(R=>Q))&(P=>R) l= (P=>Q) 
END
THEOREM IS	Q => P(t)		l= Q => ? x.P(x)
BUTTON "Apply" IS Apply ApplicaC COMMAND
BUTTON "Apply as a Rule" IS Apply applyInLineInference COMMAND
END

CONJECTUREPANEL "Calcolo di Hilbert"
	THEOREM "(A1)" IS	tt l=	P => (Q=>P)
	THEOREM "(A2)" IS	tt l=	(P=>(Q=>R)) => ((P=>Q)=>(P=>R))
	THEOREM "(A3)" IS	tt l=	(~P=>~Q)=>((~P=>Q) => P)
	THEOREM "(A4)" IS	tt l=	(! x.P(x)) => P(t)
	THEOREM "(A5)" WHERE x NOTIN P IS tt l=	(! x.(P=>Q)) => (P =>(! x.Q))
	BUTTON "Apply" IS Apply ApplicaC COMMAND
END