.dsy:it. (http://www.dsy.it/forum/)
- Filez (http://www.dsy.it/forum/forumdisplay.php?forumid=72)
-- [SPASS] Esercizio del 12/10/05 (http://www.dsy.it/forum/showthread.php?threadid=22064)

[SPASS] Esercizio del 12/10/05

Posto la mia soluzione dell'esercizio assegnato da Ghilardi per imparare a usare SPASS: "Dimostrare che 2 fratelli hanno gli stessi cugini".
Allego un file zippato contenente il file .dfg, che è l'estensione dei file presi in input da SPASS, un identico file .txt per chi volesse dare un'occhiata al codice ma non ha ancora installato SPASS, e un file .doc con le formule scritte in una sintassi un po più leggibile rispetto alla notazione prefissa di SPASS

Suggerimento: per formule che hanno un gran numero di parentesi (ad esempio nel mio file c'è un assioma con un totale di 100 parentesi ), invece di contarle una ad una per vedere se le avete chiuse tutte, copiate la formula in questione in Word. Poi fate "Sostituisci ( con (",e vi dirà quante volte ha fatto la sostituzione, il che corrisponde al numero di parentesi aperte. Poi fate "Sostituisci ) con )" e se il numero è uguale avete una quasi sicurezza di aver chiuso tutto dico "quasi" perchè magari avete aperto 35 parentesi e ne avete chuise altrettante, ma magari non nei posti giusti

__________________
All have said their prayers
Invade their nightmares
To see into my eyes
You'll find where murder lies

Off-Topic:

Comunque ripeto, tu quest'anno mi fai paura!

__________________
I ragazzi che si amano si baciano in piedi contro le porte della notte, e la gente che passa li punta con il dito, ma i ragazzi che si amano non ci sono per nessuno ed è la loro ombra soltanto che trema nella notte.
Stimolando la rabbia dei passanti, la loro rabbia il loro disprezzo le risa la loro invidia.
I ragazzi che si amano non ci sono per nessuno.
Essi sono altrove, molto più lontano della notte, molto più in alto del giorno, nell'abbagliante splendore del loro amore.

Off-Topic:
faccio paura anche a me

__________________
All have said their prayers
Invade their nightmares
To see into my eyes
You'll find where murder lies

Ok, ho provato che l'esercizio funziona anche con una formalizzazione dell'essere cugini molto più semplice.
Per provare, sostituite "l'assioma dei cugini" con questa formula:

SPASS
formula(forall([x,z],equiv(or(or(or(fratello(padre
(x),padre(z)),fratello(padre(x),madre(z))),fratell
o(madre(x),padre(z))),fratello(madre(x),madre(z)))
,cugino(x,z)))). % name({*Assioma dei cugini*})

SINTASSI TRADIZIONALE
∀x,z (fratello(padre(x),padre(z)) ∨ fratello(padre(x),madre(z)) ∨ fratello(madre(x),padre(z)) ∨ fratello(madre(x),madre(z)) ↔ cugino(x,z))

Cioè, due persone si definiscono cugini non quando hanno un nonno in comune, ma quando un genitore di uno e un genitore dell'altro sono fratelli. entrambe le definizioni producono lo stesso risultato, ma quella che sto postando ora è indubbiamente più semplice da formalizzare.

PS: abituatevi a usare la notazione prefissa di SPASS invece dello SPASSEDITOR, perchè Ghilardi userà principalmente quella.

__________________
All have said their prayers
Invade their nightmares
To see into my eyes
You'll find where murder lies

complimenti. non c'ho capito una mazza perchè non ho seguito ancora una lezione comunque sia mi sembra un bel lavoro!

Io l'ho fatto così

begin_problem(null).

list_of_descriptions.
name({*null*}).
author({*null*}).
status(unknown).
description({*null*}).
date({*null*}).
end_of_list.

list_of_symbols.
functions[(p,1),(m,1)].
predicates[(F,2),(C,2)].
end_of_list.

list_of_formulae(axioms).
formula(forall([x,y],implies(and(equal(p(x),p(y)),
equal(m(x),m(y))),F(x,y)))).
formula(forall([x,z],implies(or(or(or(F(p(x),p(z))
,F(m(x),p(z))),F(p(x),m(z))),F(m(x),m(z))),C(x,z))
)).
formula(exists([x,y],F(x,y))).
formula(exists([x,z],C(x,z))).
end_of_list.

list_of_formulae(conjectures).
formula(exists([y,z],C(y,z))). % name({*Stessi cugini*})
end_of_list.

end_problem.

__________________
I ragazzi che si amano si baciano in piedi contro le porte della notte, e la gente che passa li punta con il dito, ma i ragazzi che si amano non ci sono per nessuno ed è la loro ombra soltanto che trema nella notte.
Stimolando la rabbia dei passanti, la loro rabbia il loro disprezzo le risa la loro invidia.
I ragazzi che si amano non ci sono per nessuno.
Essi sono altrove, molto più lontano della notte, molto più in alto del giorno, nell'abbagliante splendore del loro amore.

mi fate sentire ignorante

Originally posted by GinoPilotino
mi fate sentire ignorante

Off-Topic:
Tu SEI ignorante Gino! Io voglio cambiare compagno di newseraggio! Scherzo ovviamente

__________________
I ragazzi che si amano si baciano in piedi contro le porte della notte, e la gente che passa li punta con il dito, ma i ragazzi che si amano non ci sono per nessuno ed è la loro ombra soltanto che trema nella notte.
Stimolando la rabbia dei passanti, la loro rabbia il loro disprezzo le risa la loro invidia.
I ragazzi che si amano non ci sono per nessuno.
Essi sono altrove, molto più lontano della notte, molto più in alto del giorno, nell'abbagliante splendore del loro amore.

tutto ciò è altamente offensivo e irriverente.
per punizione verrò puntuale alle lezioni e agli appuntamenti

Originally posted by Flavia

Off-Topic:
Tu SEI ignorante Gino! Io voglio cambiare compagno di newseraggio! Scherzo ovviamente

Off-Topic:
gino non è ignorante!
Comunque la tua soluzione flavia è esattamente uguale alla seconda che ho postato io sei sempre disattenta

__________________
All have said their prayers
Invade their nightmares
To see into my eyes
You'll find where murder lies

Off-Topic:
Flavy,visto che l'area filez è un po' nascosta,non è il caso di splittare il thread nel forum di Logica invece che qui?

__________________
"Solamente il cuore ti permette di vedere chiaramente.L'essenziale e' invisibile agli occhi"
bisogna vivere "alla giornata", senza crearsi troppe aspettative. quello che viene sarà un "di più" ed è da mettere nel salvadanaio.
Sono troppo una grilla petulante by Nous