[logica per applicazioni] problema con spasseditor Clicca QUI per vedere il messaggio nel forum |
rik |
ciao a tutti
sto provando a fare degli esercizi per prepararmi per l'appello di lunedi ma ho un problema .. utilizzato lo spass editor riesco a creare problemi inserendo assiomi bla, bla, bla.. ma se provo a aprire un dfg della libreria tptp mi carica solo le dichiarazioni delle funzioni ma non mi carica gli assiomi ne congettura?? perchpè? succede anche a voi? bisogna impostare qualcosa prima? .. spero che qulcuno possa darmi una mano |
Polsy |
i file della libreria tptp che hanno un meno (del tipo PUZ001-1) sono formalizzati direttamente in clausole, per cui lo spass editor non vede formule (assiomi o congetture) da visualizzare, mentre quelli col più (tipo PUZ001+1) hanno la dichiarazione delle formule, però per farle leggere dall'interfaccia devi prima togliere gli spazi e gli a capo all'interno delle singole formule (e mi pare anche all'interno della dichiarazione di funzioni e predicati) |
rik |
cakkio .. davvero comodo!! :-D
cmq grazie .. sarei impazzito!
tu per caso hai seguito il corso di quest'anno? io mi sto preparando con le video lezioni, xò ho letto che quest'anno il capitolo 4 è facoltativo .. sai che genere di problemi vanno portati? |
rik |
.. mi viene un'altro dubbio .. ma per l'esame va bene anche un esercizio già formalizzato con clausole? |
Polsy |
Mi sono preparata con le videolezioni anch'io, non avendo seguito non sono la fonte più autorevole... comunque da quanto ho capito devi portare un problema senza l'uguaglianza dal momento che non ha fatto il quarto capitolo, però se glie ne porti uno con l'uguaglianza va bene lo stesso e considera che tu abbia studiato anche la parte facoltativa. |
rik |
a costo di passare per ignorante (meglio qua che davanti al prof!!) per problema con eguaglianza cosa si intende?
un problema con una clausola del genere "p(x)= a" per esempio è già da considerarsi con uguaglianza? o è qlc di + complicato? |
Polsy |
è come l'esempio che hai fatto tu, se uno dei letterali è della forma A=B allora il problema è con l'uguaglianza e serve la superposition per risolverlo.
Nella descrizione dei problemi di tptp c'è una voce del tipo
Number of atoms : 24 ( 5 equality)
che ti dice quante uguaglianze ci sono nel problema (in questo caso 5) |
rik |
sper che qlc possa rispondermi anche se è sabato ..
dal sito del prof " Ovviamente, gli studenti che non preparassero la parte (facoltativa per l'a.a. 2006-2007) relativa alle regole di paramodulazione/sovrapposizione dovranno scegliere per l'esame un problema che non coinvolga il predicato di identità"
.. identità è lo stesso di uguaglianza? oppure se ho un problema con uguaglianza posso lasciare perdere il capitolo 4? |
Polsy |
identità = uguaglianza |
rik |
ok .. allora il problema che avevo scelto nn va bene .. |
FabryProg |
Bell'editor ... peccato che con linux nn va' :-| |
FabryProg |
Errata corrige:
Non e' linux ma il fatto di inserire i vari spazi....
:shock: Vallo a capire! Ma scrivere un howto? |
Woland |
dimentivcavo... io parlo di Logica matematica per la Magistrale in Informatica |
yeah |
Direi che ti sei risposto da solo ;)
Guarda le prime righe del secondo link :) |
Woland |
quindi per rendere un po' più esplicita la tua osservazione, correggetemi se sbaglio, per la MAGISTRALE il link buono è il primo e l'esame è orale? |
|
|
|