Romeo

Harvester of Sorrow

User info:

Registered: Oct 2003
Posts: 212 (0.03 al dì)
Location: Qua
Corso: Lavoro!
Anno: Nessuno
Time Online: 3 Days, 8:31:01: [...]
Status: Offline

Post actions:

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

Attachment: cugini.zip
This has been downloaded 109 time(s).

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

Last edited by Romeo on 14-10-2005 at 12:58

Flavia

Regina degli avatar

User info:

Registered: Sep 2002
Posts: 3228 (0.40 al dì)
Location: Bergamo
Corso: TI.COM
Anno: Finito! :D
Time Online: 25 Days, 9:12:10 [...]
Status: Offline

Post actions:

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.

Romeo

Harvester of Sorrow

User info:

Registered: Oct 2003
Posts: 212 (0.03 al dì)
Location: Qua
Corso: Lavoro!
Anno: Nessuno
Time Online: 3 Days, 8:31:01: [...]
Status: Offline

Post actions:

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

Romeo

Harvester of Sorrow

User info:

Registered: Oct 2003
Posts: 212 (0.03 al dì)
Location: Qua
Corso: Lavoro!
Anno: Nessuno
Time Online: 3 Days, 8:31:01: [...]
Status: Offline

Post actions:

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

GinoPilotino

.grande:maestro.

User info:

Registered: Dec 2002
Posts: 1403 (0.17 al dì)
Location: Segrate
Corso: TI.COM
Anno: Secondo
Time Online: 13 Days, 8:59:42 [...]
Status: Offline

Post actions:

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

Flavia

Regina degli avatar

User info:

Registered: Sep 2002
Posts: 3228 (0.40 al dì)
Location: Bergamo
Corso: TI.COM
Anno: Finito! :D
Time Online: 25 Days, 9:12:10 [...]
Status: Offline

Post actions:

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.

GinoPilotino

.grande:maestro.

User info:

Registered: Dec 2002
Posts: 1403 (0.17 al dì)
Location: Segrate
Corso: TI.COM
Anno: Secondo
Time Online: 13 Days, 8:59:42 [...]
Status: Offline

Post actions:

mi fate sentire ignorante

Flavia

Regina degli avatar

User info:

Registered: Sep 2002
Posts: 3228 (0.40 al dì)
Location: Bergamo
Corso: TI.COM
Anno: Finito! :D
Time Online: 25 Days, 9:12:10 [...]
Status: Offline

Post actions:

Originally posted by GinoPilotino
mi fate sentire ignorante

__________________
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.

GinoPilotino

.grande:maestro.

User info:

Registered: Dec 2002
Posts: 1403 (0.17 al dì)
Location: Segrate
Corso: TI.COM
Anno: Secondo
Time Online: 13 Days, 8:59:42 [...]
Status: Offline

Post actions:

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

Romeo

Harvester of Sorrow

User info:

Registered: Oct 2003
Posts: 212 (0.03 al dì)
Location: Qua
Corso: Lavoro!
Anno: Nessuno
Time Online: 3 Days, 8:31:01: [...]
Status: Offline

Post actions:

Originally posted by Flavia

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

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

luna

.grande:maestro.

User info:

Registered: Apr 2003
Posts: 4565 (0.58 al dì)
Location: Rozzano
Corso:
Anno: Ormai finito!
Time Online: 102 Days, 14:49:55 [...]
Status: Offline

Post actions:

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