Spass
Clicca QUI per vedere il messaggio nel forum |
| XXXX |
Ciao..qualcuno ha degli appunti su spass?
Grazie mille....:-D |
| dtag |
Aggiungo a questo thread una domanda inerente SPASS...
Qual'è il significato dell'asterisco (*), nell'output generato dal prover?
Grazie :-D |
| 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...:?:?:? |
| dtag |
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. |
| 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... |
| dtag |
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. |
| XXXX |
grazie mille...
in poche parole si puo prendere un esercizio svolto e poi commentarlo all'esame ...:) |
| dtag |
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... |
| 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.. |
| dtag |
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... |
| XXXX |
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 |
| dtag |
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 |
| XXXX |
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 |
| dtag |
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; |
| XXXX |
si..
pero mi sa che è troppo lungo e incasinato... ne vorrei uno piu semplice :( |
| dtag |
Originally posted by XXXX
si..
pero mi sa che è troppo lungo e incasinato... ne vorrei uno piu semplice :(
E' quello che ho scelto anche io.. :D |
| dtag |
Guardi per favore la "Given clause 42"? La [Res: 25.1,19.2] non termina in fallimento?
Oppure fa per caso una rinomina della variabile U nella seconda clausola in modo da renderla disgiunta dalla prima? :? |
| XXXX |
ma tu che opzioni metti?
ora guardo |
| dtag |
Originally posted by XXXX
ma tu che opzioni metti?
ora guardo
-Splits=0 -Sorts=0 -Docproof=1 |
| XXXX |
se t va lo possiamo vedere tutto dall'inizio cosi vediamo se abbiamo capito...ora guardo la given
io pero ho un dubbio..se metti quelli opzioni,poi nel risultato in spass esce
Reductions: RFMRR=1 RBMRR=1 RObv=1 RUnC=1 RTaut=1 RSST=1 RSSi=1 RFSub=1 RBSub=1 RCon=1
e noi nn abbiamo farro Rcon o runc e robv no? nn dobbiamo disattivarle?
se le disattivo nn si ferma piu...
c'è qualcosa che nn torna..a me nn da la given clause 42 :/ |
| dtag |
mmm... quindi tu dici che dobbiamo dissattivarle? io semplicemente non le consideravo... :D
c'è qualche maestro di SPASS che sa la risposta? :D
Tu hai account skype, icq o jabber? Se si mandami contatto via messaggio privato ci sentiamo domani primo pomeriggio. Io ora mollo perchè sono un po' fuso...
[Della parte di Ranise so ancora poco o niente, tu? :sad:] |
| XXXX |
dai allora c sentiamo domani nel primo pome...mollo anche io..
no d ranise zero quasi..giusto qualcosa sull'universo d herbrand ..
tu le dispense del prof le sai tutte bene?
cmq si bisogna disattivare le opzioni che nn abbiamo mai fatto..poi nn so.. :cry::cry::cry: |
| dtag |
| La mia conoscenza sulle dispense ha un punto di minimo su LPO, KBO e Letterali Massimali... |
| XXXX |
| ti ho mandato un msg privato...:-D |
| holylaw |
ma non c'e' una guida online di spass da qualche parte?
|
| holylaw |
| cosa vuol dire equiv?? |
| c3ru |
equiv(a,b)
a=b
p.s. qualcuno mi sa dire che ca**o di formato ci vuole per l'esempio in spass? se porto un file PUZ paro paro di come c'è nella libreria (con clause e tutto il resto) gli va bene? |
|
|
|
