Formalizzazione Logica Predicativa

[asterix07]

Buonasera a tutti. Dovrei formalizzare il seguente problema per poi passarlo ad un dimostratore automatico.

Per il furto in casa de Ricchis i sospetti si sono ristretti a 4 persone: Aldo, bruno e senza occhiali; Baldo, bruno e con gli occhiali; Carlo, biondo e con gli occhiali; Dario, biondo e senza occhiali. La polizia ha accertato che il furto è stato commesso da una sola persona, che si è avvalsa di un unico complice. Le deposizioni dei 4 sospetti sono le seguenti:
Aldo: “il colpevole è bruno e porta gli occhiali”
Baldo: “il colpevole è biondo e non porta gli occhiali”
Carlo: “il colpevole porta gli occhiali ed il suo complice è Aldo”
Dario: “il colpevole è bruno ed il suo complice è Carlo”.
Si sa che le due affermazioni del colpevole sono false, mentre una sola affermazione del complice è falsa. Gli altri hanno detto la verità. Chi sono, rispettivamente, il colpevole e il suo complice?

Per il momento ho effettuato la seguente formalizzazione:

Aldo, bruno e senza occhiali;

Bruno(Aldo) ∧ ┐ Occhiali(Aldo)

Baldo, bruno senza occhiali;

Bruno(Baldo) ∧ Occhiali(Baldo)

Carlo Biondo, con gli occhiali;

┐ Bruno(Carlo) ∧ Occhiali(Carlo)

Dario biondo, senza occhiali

┐ Bruno(Dario) ∧ ┐ Occhiali(Dario)

Dichiarazioni di carlo nel caso in cui sia colpevole,onesto,complice:

Onesto(Carlo) → ∀x (Colpevole(x) → Occhiali(x) ∧ Complice(Aldo))
Colpevole(Carlo) → ┐ ∀x (Colpevole(x) → Occhiali(x) ∧ Complice(Aldo))
Complice(Carlo) → ∀x (Colpevole(x) → Occhiali(x) ∧ ┐ Complice(Aldo))

Dichiarazioni di aldo nel caso in cui sia colpevole,onesto,complice:

Onesto(Aldo) → ∀x (Colpevole(x) → Bruno(x) ∧ Occhiali(x))
Onesto(Dario) → ∀x (Colpevole(x) → Bruno(x) ∧ Complice(Carlo))
Complice(Aldo) → ∀x (Colpevole(x) → ┐ Bruno(x) ∧ Occhiali(x)) ∨ (Complice(Aldo) → ∀x (Colpevole(x) → Bruno(x) ∧ ┐ Occhiali(x)))

Dichiarazioni di baldo nel caso in cui sia colpevole,onesto,complice:

Onesto(Baldo) → ∀x (Colpevole(x) → ┐ Bruno(x) ∧ ┐ Occhiali(x))
Colpevole(Baldo) → ┐ ∀x (Colpevole(x) → ┐ Bruno(x) ∧ ┐ Occhiali(x))
(Complice(Baldo) → ∀x (Colpevole(x) → Bruno(x) ∧ ┐ Occhiali(x))) ∨ (Complice(Baldo) → ∀x (Colpevole(x) → ┐ Bruno(x) ∧ Occhiali(x)))

Dichiarazioni di dario nel caso in cui sia colpevole,onesto,complice:

Onesto(Dario) → ∀x (Colpevole(x) → Bruno(x) ∧ Complice(Carlo))
Colpevole(Dario) → ┐ ∀x (Colpevole(x) → Bruno(x) ∧ Complice(Carlo))
(Complice(Dario) → ∀x (Colpevole(x) → Bruno(x) ∧ ┐ Complice(Carlo))) ∨ (Complice(Dario) → ∀x (Colpevole(x) → ┐ Bruno(x) ∧ Complice(Carlo)))

Ora conoscendo la soluzione a priori, pongo come congettura:
Colpevole(Baldo) ∧ Complice(Carlo)

Cosi facendo il dimostratore dovrebbe darmi esito positivo, ma la cosa non avviene. Sicuramente c'è un errore oppure manca qualche clausola nella formalizzazione del problema. Qualcuno è in grado di aiutarmi? Grazie

[hamming_burst]

Ciao,
scusa la curiosità, ma di che dimostratore automatico parli? Tipo Coq o Isabelle cioè quelli chiamati "interactive theorem prover"?

[asterix07]

Il proover che devo utilizzare io è SPASS (Automated Theorem Prover for First-Order Logic).
Una volta datogli in input il problema formalizzato cerca verificare la soluzione tramite la congettura, restituendo anche la procedura da lui svolta.