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.

della parola significa decidere se vale T1 ∪ T2 |= u = v per una coppia (u, v) di termini arbitrari costruiti sulla segnatura unione. Si tratta ancora di un problema indecidibile nel caso piu` generale, a meno di porre ipotesi piu` restrittive: ad esempio si puo` supporre che T1 e T2 siano costruibili su di una teoria comune, che chiameremo T0 (diamo dettagliata descrizione di cosa sia la costruibilita` nel paragrafo 3.1 della tesi). In questo caso, la dimostrazione di decidibilita` e` data in [8] e [2]. Scopo di questa tesi e` dare una dimostrazione alternativa a quelle introdotte da [8] e [2] e che ha, rispetto a quest’ultime, il pregio di un approccio piu` semplice e di una maggiore brevita`. Questi vantaggi sono dovuti all’uso, nello sviluppo della dimostra- zione, di un efficace strumento di calcolo quale la riscrittura ordinata che, estendendo il completamento di Knuth-Bendix-Huet, permette di trovare sempre un sistema di riscrittura canonico, se questo esiste, anche laddove il completamento standard fallisce a causa della non orientabilita` di equazioni. La dimostrazione si articola come di seguito: le segnature Σ1 e Σ2 delle due teorie non sono necessariamente disgiunte, come detto, e vi e` dunque un insieme di termini comuni che nell’unione vengono a confondersi. Al fine di eliminare questa ambiguita` abbiamo costruito una teoria a due sorte T˜ che conserva i teoremi delle due teorie originarie. Per fare cio`, ci siamo avvalsi di una mappa che fa corrispondere i termini di T1 ∪ T2 a quelli di T˜ e di due regole interne a T˜ che creano un isomorfismo tra i termini che nella teoria unione sono condivisi e che in T˜ invece sono distinti e di sorta diversa. Poi abbiamo argomentato semanticamente per operare una riduzione del problema della parola combinato al problema della parola in T˜ . Su T˜ abbiamo costruito il nostro sistema di riscrittura ordinato. Il secondo passo e` stato di orientare le equazioni di T˜ sfruttando la nozione di riscrittura ordinata (per la quale se un’equazione non e` orientabile, sicuramente lo sono tutte le sue istanze ground), e di dimostrare poi la ground-confluenza del sistema di riscrittura E ottenuto, attraverso la congiungibilita` delle sue coppie critiche estese. 2

Anteprima della Tesi di Jacopo Mantovani

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

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.