Calcolo deduttivo per JAPE
La versione 7.1 di jape ed le versioni Lab_*.jt del
calcolo deduttivo sono disponibili nella directory
/local/eserc/MATDISCR nei laboratori SW1 e SW2.
La verifica del lavoro verrà effettuata in laboratorio SW1, in
orari opportunamente prenotati. La prossima avverrà il 7 febbraio
2005, alle ore 9: è disponibile la prenotazione in
rete.
(risultati
delle verifiche)
Tre esempi di verifiche
- In quindici minuti, dimostrare
- la conseguenza che (~P)&(~Q) segue da ~(P|Q)
- l'equivalenza relativa allo pseudocomplemento
- l'equivalenze "unità" e "counità" relative al
quantificatore esistenziale, facendo attenzione a non aggiungere
condizioni al contorno.
Salvare in un file con estensione "jp" le dimostrazioni richieste e
quelle di proprietà che si è dovuto invocare nel processo.
Il nome del file deve essere il cognome del candidato concatenato con i
caratteri "_a" o "_u" per indicare i caratteri usati ("_a" per ASCII,
"_u" per UNICODE).
- In quindici minuti, dimostrare
- la funtorialità per la negazione
- la proprietà di DeMorgan per la congiunzione
- le proprietà (A4) e (A5) del Calcolo di Hilbert, facendo
attenzione a non aggiungere condizioni al contorno.
Salvare in un file con estensione "jp" le dimostrazioni richieste e
quelle di proprietà che si è dovuto invocare nel processo.
Il nome del file deve essere il cognome del candidato concatenato con i
caratteri "_a" o "_u" per indicare i caratteri usati ("_a" per ASCII,
"_u" per UNICODE).
- In un'ora dimostrare
- almeno 10 conseguenze del pannello "Regole derivate"
- almeno 6 conseguenze del pannello "Funtorialità"
- almeno 10 equivalenze del pannello "Equivalenze"
- almeno 3 conseguenze del pannello "Calcolo di Hilbert"
Salvare in un file con estensione "jp" le dimostrazioni richieste e
quelle di proprietà che si è dovuto invocare nel processo.
Il nome del file deve essere il cognome del candidato concatenato con i
caratteri "_a" o "_u" per indicare i caratteri usati ("_a" per ASCII,
"_u" per UNICODE).
Soluzioni: 1,
2.