Dsy Network>  www | forum | my | didattica | howto | wiki | el goog | stats | blog | dona | rappresentanti
Homepage
 Register   Calendar   Members  Faq   Search  Logout 
.dsy:it. : Powered by vBulletin version 2.3.1 .dsy:it. > Didattica > Corsi G - M > Logica matematica > Spass
Pages (2): [1] 2 »   Last Thread   Next Thread
Author
Thread    Expand all | Contract all    Post New Thread    Post A Reply
Collapse
XXXX
.consigliere.

User info:
Registered: Jan 2007
Posts: 135 (0.02 al dì)
Location:
Corso: informatica
Anno:
Time Online: 21:43:17 [...]
Status: Offline

Post actions:

Edit | Report | IP: Logged
 Spass

Ciao..qualcuno ha degli appunti su spass?
Grazie mille....:-D
03-07-2007 10:37
Click Here to See the Profile for XXXX Click here to Send XXXX a Private Message Find more posts by XXXX Add XXXX to your buddy list Printer Friendly version Email this Article to a friend Reply w/Quote
Collapse
dtag
.simpatizzante.

User info:
Registered: Mar 2006
Posts: 13 (0.00 al dì)
Location:
Corso: TICOM
Anno:
Time Online: 3:33:44 [...]
Status: Offline

Post actions:

Edit | Report | IP: Logged

Aggiungo a questo thread una domanda inerente SPASS...

Qual'è il significato dell'asterisco (*), nell'output generato dal prover?

Grazie :-D
05-07-2007 17:56
Click Here to See the Profile for dtag Click here to Send dtag a Private Message Find more posts by dtag Add dtag to your buddy list Printer Friendly version Email this Article to a friend Reply w/Quote
Collapse
XXXX
.consigliere.

User info:
Registered: Jan 2007
Posts: 135 (0.02 al dì)
Location:
Corso: informatica
Anno:
Time Online: 21:43:17 [...]
Status: Offline

Post actions:

Edit | Report | IP: Logged

indica i letterali massimali :o)

qualcuno sa perche usando l'interfaccia d spass a volte nn mi salva..quindi mi ritrovo a scrivere programmi..e alla fine nn riesco a vedere il risultato...:?:?:?
06-07-2007 20:44
Click Here to See the Profile for XXXX Click here to Send XXXX a Private Message Find more posts by XXXX Add XXXX to your buddy list Printer Friendly version Email this Article to a friend Reply w/Quote
Collapse
dtag
.simpatizzante.

User info:
Registered: Mar 2006
Posts: 13 (0.00 al dì)
Location:
Corso: TICOM
Anno:
Time Online: 3:33:44 [...]
Status: Offline

Post actions:

Edit | Report | IP: Logged

Originally posted by XXXX
indica i letterali massimali :o)

qualcuno sa perche usando l'interfaccia d spass a volte nn mi salva..quindi mi ritrovo a scrivere programmi..e alla fine nn riesco a vedere il risultato...:?:?:?


Grazie... con una lettura più attenta delle dispense avevo trovato la risposta [pag. 42] . :-D

Intendi l'interfaccia java o la gui? La prima non l'ho provata, mentre con la seconda avevo problemi anche io con il salvataggio (su Debian/Linux). Ho "risolto" usando SPASS da terminale e salvando il copia/incolla del risultato in un file di testo.

Last edited by dtag on 07-07-2007 at 20:59
07-07-2007 20:52
Click Here to See the Profile for dtag Click here to Send dtag a Private Message Find more posts by dtag Add dtag to your buddy list Printer Friendly version Email this Article to a friend Reply w/Quote
Collapse
XXXX
.consigliere.

User info:
Registered: Jan 2007
Posts: 135 (0.02 al dì)
Location:
Corso: informatica
Anno:
Time Online: 21:43:17 [...]
Status: Offline

Post actions:

Edit | Report | IP: Logged

intendo l'interfaccia java...
mmm..la gui nn l'ho provata..come si fa? :razz:

ma tu hai gia fatto qualche esercizio della libreria tptp?magari possiamo confrontare i risultati o fare qualche esercizio...
08-07-2007 11:12
Click Here to See the Profile for XXXX Click here to Send XXXX a Private Message Find more posts by XXXX Add XXXX to your buddy list Printer Friendly version Email this Article to a friend Reply w/Quote
Collapse
dtag
.simpatizzante.

User info:
Registered: Mar 2006
Posts: 13 (0.00 al dì)
Location:
Corso: TICOM
Anno:
Time Online: 3:33:44 [...]
Status: Offline

Post actions:

Edit | Report | IP: Logged

Originally posted by XXXX
intendo l'interfaccia java...
mmm..la gui nn l'ho provata..come si fa? :razz:

ma tu hai gia fatto qualche esercizio della libreria tptp?magari possiamo confrontare i risultati o fare qualche esercizio...


In windows la gui viene installata con SPASS in automatico. Per i sistemi *nix, installi prima il prover da sorgenti o pacchetto precompilato e poi utilizzi l'interfaccia sviluppata da Mauro Mereu che trovi qui.

L'interfaccia java non l'ho utilizzata perchè mi sembra non venga utilizzata durante l'esame.

Gli esercizi che ho preso in considerazione in vista dell'orale di giovedì sono i PUZ senza identità perchè non porto la parte facoltativa. I file .dfg sono qui.

Last edited by dtag on 09-07-2007 at 12:45
09-07-2007 12:37
Click Here to See the Profile for dtag Click here to Send dtag a Private Message Find more posts by dtag Add dtag to your buddy list Printer Friendly version Email this Article to a friend Reply w/Quote
Collapse
XXXX
.consigliere.

User info:
Registered: Jan 2007
Posts: 135 (0.02 al dì)
Location:
Corso: informatica
Anno:
Time Online: 21:43:17 [...]
Status: Offline

Post actions:

Edit | Report | IP: Logged

grazie mille...
in poche parole si puo prendere un esercizio svolto e poi commentarlo all'esame ...:)
09-07-2007 12:41
Click Here to See the Profile for XXXX Click here to Send XXXX a Private Message Find more posts by XXXX Add XXXX to your buddy list Printer Friendly version Email this Article to a friend Reply w/Quote
Collapse
dtag
.simpatizzante.

User info:
Registered: Mar 2006
Posts: 13 (0.00 al dì)
Location:
Corso: TICOM
Anno:
Time Online: 3:33:44 [...]
Status: Offline

Post actions:

Edit | Report | IP: Logged

Originally posted by XXXX
grazie mille...
in poche parole si puo prendere un esercizio svolto e poi commentarlo all'esame ...:)


Si, parti da un problema da cui ti chiede la teoria...
09-07-2007 12:45
Click Here to See the Profile for dtag Click here to Send dtag a Private Message Find more posts by dtag Add dtag to your buddy list Printer Friendly version Email this Article to a friend Reply w/Quote
Collapse
XXXX
.consigliere.

User info:
Registered: Jan 2007
Posts: 135 (0.02 al dì)
Location:
Corso: informatica
Anno:
Time Online: 21:43:17 [...]
Status: Offline

Post actions:

Edit | Report | IP: Logged

:o)

un'ultima cosa
ma ad esempio nella formula

formula(
lives(agatha),
pel55_2_1 ).

pel55_2_1 si puo togliere? in tutte le formule è presente una cosa simile..
09-07-2007 12:54
Click Here to See the Profile for XXXX Click here to Send XXXX a Private Message Find more posts by XXXX Add XXXX to your buddy list Printer Friendly version Email this Article to a friend Reply w/Quote
Collapse
dtag
.simpatizzante.

User info:
Registered: Mar 2006
Posts: 13 (0.00 al dì)
Location:
Corso: TICOM
Anno:
Time Online: 3:33:44 [...]
Status: Offline

Post actions:

Edit | Report | IP: Logged

Originally posted by XXXX
:o)

un'ultima cosa
ma ad esempio nella formula

formula(
lives(agatha),
pel55_2_1 ).

pel55_2_1 si puo togliere? in tutte le formule è presente una cosa simile..


Ho notato che ci sono per alcuni problemi due formalizzazioni: ad esempio, PUZ001-1 e PUZ001+1. Quelli con il - non vengono accettati da SPASS perchè formalizzati in clausole; quelli con il + sono in formule ma bisogna togliere "spazi" e "a capo". Leggi questo thread.
Io uso direttamente i file .dfg. Faccio male? :?
Questi dovrebbero essere ottenuti dai file con estesione .p con il comando da terminale (parlo di s.o. *nix) "tptp2X -f dfg file.p", come indicato nella sezione "Comments" del file stesso.

Consiglio: ho assistito ad un orale dove una ragazza portando l'esercizio "di zia Agatha", già trattato ad esercitazione, è stata criticata dal prof...

Last edited by dtag on 09-07-2007 at 13:25
09-07-2007 13:06
Click Here to See the Profile for dtag Click here to Send dtag a Private Message Find more posts by dtag Add dtag to your buddy list Printer Friendly version Email this Article to a friend Reply w/Quote
Collapse
XXXX
.consigliere.

User info:
Registered: Jan 2007
Posts: 135 (0.02 al dì)
Location:
Corso: informatica
Anno:
Time Online: 21:43:17 [...]
Status: Offline

Post actions:

Edit | Report | IP: Logged

si ma ne ho preso uno a caso d esercizio..pero ho notato che in quasi tutti alla fine d una formula c'è "pel55_2_1 "...e cosi via...

si so che certi spass nn li prende...
anche io pensavo d usare direttaemnte i file .dfg...
bhoooooooooo
09-07-2007 13:18
Click Here to See the Profile for XXXX Click here to Send XXXX a Private Message Find more posts by XXXX Add XXXX to your buddy list Printer Friendly version Email this Article to a friend Reply w/Quote
Collapse
dtag
.simpatizzante.

User info:
Registered: Mar 2006
Posts: 13 (0.00 al dì)
Location:
Corso: TICOM
Anno:
Time Online: 3:33:44 [...]
Status: Offline

Post actions:

Edit | Report | IP: Logged

Alcuni dubbi...

Ho notato che in certi problemi di SPASS la Risoluzione viene portata a termine anche se il problema di unificazione termina in fallimento (tipo X=f(X)), come mai?
Le regole Obv e MRR implicano la riduzione di più clausole (non mostrate nell'output di SPASS) ad una sola (mostrata nel listato), giusto?
Il significato del + che compare in alcune clausole (es: f(X,Y)*+ g(X,Y)-> )?

Grazie :-D

Last edited by dtag on 09-07-2007 at 21:17
09-07-2007 16:32
Click Here to See the Profile for dtag Click here to Send dtag a Private Message Find more posts by dtag Add dtag to your buddy list Printer Friendly version Email this Article to a friend Reply w/Quote
Collapse
XXXX
.consigliere.

User info:
Registered: Jan 2007
Posts: 135 (0.02 al dì)
Location:
Corso: informatica
Anno:
Time Online: 21:43:17 [...]
Status: Offline

Post actions:

Edit | Report | IP: Logged

quello della risoluzione nn lo so ..nn ho mai visto esempi cosi..prova a farmi vedere...

La regola MMR è giusta

+ = l'inferenza viene applicata solo ai letterali che ce l'hanno..serve insieme all'* per ridurre il numero d inferenze applicabili e prevale il + sull'* (cosi ha detto a lezione)

ma tu sapresti risolvere qst

∀X (animale(X) → ∀Y (pianta(Y) → mangia(X,Y)) ∨ ∀Y1 (animale(Y1) ∧ (piu_piccolo(Y1,X) ∧ ∃Z (pianta(Z) ∧ mangia(Y1,Z))) → mangia(X,Y1)))

devo fare la skolemizzazione..ma nn mi esce lo stesso risultato d spass ..boh
10-07-2007 11:30
Click Here to See the Profile for XXXX Click here to Send XXXX a Private Message Find more posts by XXXX Add XXXX to your buddy list Printer Friendly version Email this Article to a friend Reply w/Quote
Collapse
dtag
.simpatizzante.

User info:
Registered: Mar 2006
Posts: 13 (0.00 al dì)
Location:
Corso: TICOM
Anno:
Time Online: 3:33:44 [...]
Status: Offline

Post actions:

Edit | Report | IP: Logged

Originally posted by XXXX

ma tu sapresti risolvere qst

∀X (animale(X) → ∀Y (pianta(Y) → mangia(X,Y)) ∨ ∀Y1 (animale(Y1) ∧ (piu_piccolo(Y1,X) ∧ ∃Z (pianta(Z) ∧ mangia(Y1,Z))) → mangia(X,Y1)))

devo fare la skolemizzazione..ma nn mi esce lo stesso risultato d spass ..boh


E' il PUZ031-1 per caso? Così ad occhio...
Trasformerei le implicazioni così: (A -> B) in (notA V B);
Poi passerei il tutto in f.n.prenessa;
Skolemizzerei eliminando il quantificatore esistenziale (rinomino Z con una costante c);
Farei f.n.congiuntiva;
Infine passerei alle clausole;

Last edited by dtag on 10-07-2007 at 19:53
10-07-2007 19:41
Click Here to See the Profile for dtag Click here to Send dtag a Private Message Find more posts by dtag Add dtag to your buddy list Printer Friendly version Email this Article to a friend Reply w/Quote
Collapse
XXXX
.consigliere.

User info:
Registered: Jan 2007
Posts: 135 (0.02 al dì)
Location:
Corso: informatica
Anno:
Time Online: 21:43:17 [...]
Status: Offline

Post actions:

Edit | Report | IP: Logged

si..
pero mi sa che è troppo lungo e incasinato... ne vorrei uno piu semplice :(
10-07-2007 19:48
Click Here to See the Profile for XXXX Click here to Send XXXX a Private Message Find more posts by XXXX Add XXXX to your buddy list Printer Friendly version Email this Article to a friend Reply w/Quote
All times are GMT. The time now is 00:59.    Post New Thread    Post A Reply
Pages (2): [1] 2 »   Last Thread   Next Thread
Show Printable Version | Email this Page | Subscribe to this Thread | Add to Bookmarks

Forum Jump:
Rate This Thread:

Forum Rules:
You may not post new threads
You may not post replies
You may not post attachments
You may not edit your posts 		HTML code is OFF
vB code is ON
Smilies are ON
[IMG] code is ON
 

Powered by: vBulletin v2.3.1 - Copyright ©2000 - 2002, Jelsoft Enterprises Limited
Mantained by dsy crew (email) | Collabora con noi | Segnalaci un bug | Archive | Regolamento | Licenze | Thanks | Syndacate
Pagina generata in 0.046 seconds (80.19% PHP - 19.81% MySQL) con 26 query.