Fondamenti di Informatica, 14 Febbraio 2013

Non e' ammesso l'uso di alcun testo, appunti o calcolatrici. Le risposte vanno scritte nel foglio di bella copia. Si raccomanda la massima SINTETICITA'. L'eccessiva verbosita' verra' considerata negativamente.
Occorre essersi prenotati sul portale studenti del nostro ateneo. Se cio' non e' stato fatto, comunicatelo immediatamente al docente o all'assistente in aula.

I risultati verranno indicati nella pagina web del corso. Date ed orari degli orali, sul Forum.

Esercizio 1
(a) Descrivere il sistema formale del Calcolo dei Predicati (Logica dei Predicati del primo ordine) nella sua versione alla Hilbert o in deduzione naturale.

(b) Scrivere, nel linguaggio dell'Aritmetica di Peano, la formula ben formata P(x,y,z) corrispondente alla seguente relazione sui naturali: x e' un multiplo del quoziente della divisione di y e z
Dire inoltre se e' vera la seguente affermazione:

(n,m,p)∈R se e solo se PA|- P(n,m,p)

Perche?
(ricordiamo che, se q e' un numero naturale, q e'il termine che lo rappresenta nel linguaggio di PA)

(c) Ricopiare la seguente dimostrazione (in deduzione naturale per la logica proposizionale con operatori →, ¬, ∨ e ⊥) di
D, D→A, B→ (¬D ∨ C), A → (B∨C) |-- C
riempiendo le parti mancanti (indicate con sequenze di '?').
Indicare inoltre le regole nelle quali vengono scaricate le ipotesi (e quali sono le ipotesi scaricate) e il nome delle regole utilizzate nella deduzione.


                                                               ????   D
                                                              -----------
               ????    ??         ????????          [B]            ⊥
              ------------      --------------------------     ---------
  ?????             A                    (¬D)∨C                    C         ???
 ----------------------------    -------------------------------------------------
           B∨C                                           ??                           [C]
       ------------------------------------------------------------------------------------                                            
                                                 ??

Esercizio 2
(a) Descrivere il sistema formale della Logica di Hoare

(b) Scrivere un programma URM che calcoli (n div 2), dove n e' l'input e div e' la divisione intera.

(c) Supponiamo di vedere il modello computazionale delle URM, senza l'istruzione J(-,-,-), come un linguaggio di programmazione, e di voler utilizzare una logica di Hoare per darne la semantica assiomatica.
Fornire le regole e/o gli assiomi che descrivono la semantica delle istruzioni Z(n) e T(n,m).
Dire inoltre se, aggiungendo l'istruzione J(-,-,-), l'assioma

-----------------------
{A} J(n,m,p) {A}

risulterebbe valido e se descriverebbe correttamente il comportamento di tale istruzione.

Esercizio 3
Dimostrare che la rappresentazione di (n mod B) si ottiene prendendo la cifra piu' a destra della rappresentazione in notazione posizionale, in base B, di n