Logica matematica/Calcolo delle proposizioni/La risoluzione: differenze tra le versioni
Contenuto cancellato Contenuto aggiunto
Nessun oggetto della modifica |
m Correggo sintassi in formula matematica secondo mw:Extension:Math/Roadmap |
||
Riga 9:
==== Clausola ====
Una ''clausola'' del calcolo proposizionale <math>\mathcal L</math> è una disgiunzione di letterali <math>L_1 \
==== Sussunzione di clausole ====
Riga 17:
==== Forma clausale ====
Una ''formula'' del calcolo proposizionale <math>\mathcal L</math> è detta in ''forma normale congiuntiva'' o in ''forma clausale,'' oppure si dice che essa è un ''insieme di clausole'', sse è in forma normale negativa e inoltre ha la forma <math>C_1 \
}}
Poiché la disgiunzione è commutativa, una clausola generica può essere scritta come segue:
:<math>A_1 \
dove gli <math>A_i</math> e <math>B_j</math> sono atomi. Se <math>n=m=0</math>, si ha la ''clausola vuota'' e si scrive <math>\{\}</math>, oppure <math>\Box</math>. Nel seguito, una clausola verrà indicata anche come l'insieme dei suoi letterali, cioè mediante <math>\{L_1,...,L_p\}</math>.
Riga 27:
Se <math>n=1</math>, cioè se una clausola ha la forma:
:<math>A_1\
si dice che è una ''clausola definita''.
| |||