skolemizzare
Clicca QUI per vedere il messaggio nel forum |
| pumpkin |
Se ho una formula di questo tipo:
(A and B) or (C and D) come posso andare avanti nella skolemizzazione per trovare le clausole?
Poi sapete cosa intende spass quando inserisce il letterale SKP0 maiuscolo (quelli in minuscolo dovrebbero essere le variabili)? |
| Logan12584 |
misà che hai sbagliato a skolemizzare perchè devono essere concatenzioni di formule quindi può essere a o b e a o c e non come hai scritto tu con l'or...ma potrei dire cazzate...
comunque di certo so che se hai A o B
in clausole diventa -> A,B
se hai a e b diventa
-> A
-> B |
| Logan12584 |
| skp0 non so cosa sia ma sicuramente attraverso le opzioni si può togliere, ti consiglio di farlo |
| yeah |
Puoi usare il metodo non strutturale (con le leggi distributive), oppure quello strutturale, che sulla dispensa è spiegato solo per il proposizionale
(A and B) or (C and D)
In questo caso usa le leggi distributive e al primo passo ottieni:
((A and B) or C) and ((A and B) or D))
((A or C) and (B or C)) and ((A or D) and (B or D))
Da cui:
A v C, B v C, A v D, B v D
skc -> costante di skolem
skf -> funzione di skolem (simbolo di)
quindi direi che skp potrebbe essere un simbolo di predicato, ma non sono sicuro al 100%
Hai disabilitato le rinomine (CNFRenaming=0)? Dopo averlo fatto te li butta fuori ancora? |
| Logan12584 |
| ah già è vero ... infatti, concordo! |
| pumpkin |
| Intanto grazie per le risposte...per quanto riguarda skp0 disabilitando le rinomine non spunta più...cmq adesso cerco di capire bene come funziona...per quanto riguarda la skolemizzazione vi faccio sapere....grazie |
|
|
|
