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.
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.