Re: Turing-completezza linguaggi logici

Messaggioda Dirk_Pitt » 14/01/2012, 12:22

hamming_burst ha scritto:[mini-OT]
curiosità: ma che corso universitario sarebbe dove si studiano queste argomentazioni: Computabiltiy (e famiglia) o Logica (e famiglia)?

mi pare entrambe, ma vedendo l'ulimo link proposto si parla di inferenza e dimostrazioni logiche, cosa che, almeno io, ho studiato in un corso di Semantica, ma su un modello apposito ad argomentazioni sui linguaggi; per questo la domanda :-)

[/mini-OT]


AI.
Il link l ho trovato con una visità in profondità fino alla quinta pagina di google :)
Ultima modifica di Dirk_Pitt il 14/01/2012, 12:34, modificato 1 volta in totale.
Dirk_Pitt
Starting Member
Starting Member
 
Messaggio: 6 di 38
Iscritto il: 01/05/2008, 21:53

Re: Turing-completezza linguaggi logici

Messaggioda Dirk_Pitt » 14/01/2012, 12:27

Deckard ha scritto:
Dirk_Pitt ha scritto:No, scusa ho scritto in modo confuso; mi riferivo all'entailment. Non capisco in che modo fissare il numero di letterali per clausola incida sulla complessità, o meglio, lo capisco ma in ogni caso la complessità deve dipendere anche dal numero di clausole, e non solo dalla loro lunghezza, o sbaglio?.

Sinceramente non ho capito di cosa stai parlando. Cosa intendi per complessità in questo contesto?

In ogni caso, se applico la risoluzione a due clausole di n ed m letterali, quante clausole si generano al max? Dato che si genera una clausola per ogni coppia di letterali complementari, e il numero di tali coppie è al massimo min(n,m) direi che è proprio questo il numero cercato. È corretto?

Di nuovo, non capisco di cosa tu stia parlando. Stai utilizzando quindi il calcolo con risoluzione e fattorizzazione? Cosa intendi per letterali complementari?
Ti pregherei di spiegare un po' più precisamente ciò che chiedi. Soprattutto di definire il contesto in cui operi: è pieno di calcoli logici e varianti, condizione necessaria ma non sufficiente per risponderti è sapere di che cosa tu stia parlando.

Con uno studio un pò + approfondito (ma nemmeno tanto, mea culpa) mi sono risposto da solo. Dato che l'inferenza logica equivale alla in-soddisfacibilità, e 2SAT è polinomiale, allora anche l'inferenza in teorie cnf con solo 2 letterali è polinomiale.

La risoluzione è la regola di derivazione corretta e completa utilizzata ad esempio nel Davis-Putnam; i letterali complementari sono quelli ''semplificati'' dalla regola.

Ad ogni modo, per ritornare un'ultima volta sulla questione di prima: quello che volevo spiegarti è che per poter affermare che ad es. il linguaggio del primo ordine è equivalente al modello della macchina di Turing è necessario introdurre la rappresentabilità delle funzioni nel linguaggio perché altrimenti come faccio a dire che il linguaggio "calcola" una funzione? Il linguaggio del primo ordine non calcola funzioni, al massimo le può rappresentare con delle formule.


Purtroppo su questa cosa la mia mente è nel buio totale, non mi dispiacerebbe caprine un pò di + ma non so + dove cercare.
Dirk_Pitt
Starting Member
Starting Member
 
Messaggio: 7 di 38
Iscritto il: 01/05/2008, 21:53

Precedente

Torna a Informatica

Chi c’è in linea

Visitano il forum: Nessuno e 1 ospite