Propositional logic, esercizio tramite teorema

[raff5184]

ciao, devo svolgere il seguente esercizio tramite il "resolution theorem-proving" (non so come si chiama in italiano)

Se Mario avrà i soldi, comprerà un cellulare
Se Mario compra il cellulare, vuol dire che non è stato truffato
Se Mario non ha i soldi, non sarà truffato.
Dimostrare che Mario non viene truffato.

Io farei così, riscrivo le frasi in modo più formale. Indico soldi =s, cellulare = c e truffato = t

(imp s c)
(imp c -t)
(imp -s -t)
Devo dim che
(imp -s -t)

Ora però non so come procedere. Cioè devo mettere insieme le prime tre in modo da avere l'ultima? Ossia un' "equazione" con il simbolo di implicazione (entailment) $|=$ dove al primo membro ci sono le prime tre, legate tra loro in qualche modo e a secondo la tesi?

[Lord K]

Dunque... io procederei come segue, siccome:

[tex]\models a \rightarrow b[/tex] è equivalente a [tex]a \models b[/tex]

allora le tue proposizioni diventano:

[tex]\models s \rightarrow c[/tex]
[tex]\models c \rightarrow \neg t[/tex]
[tex]\models \neg s \rightarrow \neg t[/tex]

Dalle prime due:

[tex]\models s \rightarrow \neg t[/tex]
[tex]\models \neg s \rightarrow \neg t[/tex]

che sono equivalenti a:

[tex]s \models \neg t[/tex]
[tex]\neg s \models \neg t[/tex]

e questo consegue che:

[tex]s, \neg s \models \neg t[/tex]

da cui:

[tex]\models \neg t[/tex]

che è ciò che cercavi.

[raff5184]

grazie Lord K, non mi è chiaro solo l'ultima cosa che hai scritto, come notazione intendo. Cioè $|=a$ come si "legge", come si interpreta.

Se ho $a|=b$ posso dire a implica b ma con un solo termine?
Inoltre, il simbolo $->$ lo leggi comunque implica?

[Rggb1]

Se ho $a \models b$ io leggo "a soddisfa b". Vedi anche qui e qui.

[raff5184]

"Lord K":
allora le tue proposizioni diventano:

[tex]\models s \rightarrow c[/tex]
[tex]\models c \rightarrow \neg t[/tex]
[tex]\models \neg s \rightarrow \neg t[/tex]

C'è un altro modo per scrivere le formule? intendo partire da qualcosa del genere
[tex]s \rightarrow c[/tex]

e poi passare ad un legame tramite [tex]\models[/tex] ?