Questo sito utilizza cookie di terze parti per inviarti pubblicità in linea con le tue preferenze. Se vuoi saperne di più clicca QUI 
Chiudendo questo banner, scorrendo questa pagina, cliccando su un link o proseguendo la navigazione in altra maniera, acconsenti all'uso dei cookie. OK

Combinazione di procedure di decisione tramite riscrittura

L'anteprima di questa tesi è scaricabile in PDF gratuitamente.
Per scaricare il file PDF è necessario essere iscritto a Tesionline.
L'iscrizione non comporta alcun costo. Mostra/Nascondi contenuto.

Cio` non da` ancora un metodo di decisione, in quanto E e` infinito, e non e` possibile sapere se un termine e` o meno in forma normale. Si rende dunque necessario un procedimento ulteriore. Con un formalismo noto in letteratura e riadattato al nostro problema si mostra come ogni termine della nostra teoria bisortata possa venire scomposto univocamente in una parte che chiamiamo ‘head’ (che contiene cioe` soltanto simboli di una certa sorta), e in una restante parte ‘alien’ (che contiene almeno un cambio di sorta al suo interno). Questo procedimento, che consente di applicare le regole di T1 e T2 alla head dei termini, e` detto di astrazione e risulta molto utile nella dimostrazione dei due lemmi preliminari e della proposizione finale. Quest’ultima fornisce le condizioni pratiche di applicabilita` del nostro metodo: e` sufficiente avere in ingresso un insieme S di termini ground di T˜ internamente chiuso rispetto alle regole date (questo insieme si ottiene in un numero finito di passi), per poter decidere se due termini sono equivalenti. La decidibilita` della teoria unione si ottiene come corollario. La tesi si articola in cinque capitoli e un’appendice. Il primo capitolo e` questa stessa introduzione, il secondo e` una panoramica sui sistemi di riscrittura, sul completamento standard di Knuth-Bendix-Huet e sul completamento ordinato, tutti strumenti logici adoperati nel quarto capitolo che consta della dimostrazione vera e propria del teore- ma. Il terzo capitolo fornisce una trattazione dettagliata delle ipotesi (tra cui la gia` menzionata costruibilita`), e di come e dove esse vengono adoperate all’interno della dimostrazione del teorema. Il quinto capitolo riassume e conclude il lavoro svolto, e illustra possibili sviluppi e applicazioni. Infine, l’appendice A riporta la dimostra- zione della stretta corrispondenza tra la teoria unione e la nuova teoria a due sorte introdotta. 3

Anteprima della Tesi di Jacopo Mantovani

Anteprima della tesi: Combinazione di procedure di decisione tramite riscrittura, Pagina 4

Tesi di Laurea

Facoltà: Scienze Matematiche, Fisiche e Naturali

Autore: Jacopo Mantovani Contatta »

Composta da 71 pagine.

 

Questa tesi ha raggiunto 371 click dal 20/03/2004.

Disponibile in PDF, la consultazione è esclusivamente in formato digitale.