rik

User info:

Registered: Jan 2006
Posts: 110 (0.02 al dì)
Location:
Corso: specialistica
Anno:
Time Online: 1 Day, 22:38:15 [...]
Status: Offline

Post actions:

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

.arcimaestro.

User info:

Registered: Dec 2003
Posts: 477 (0.06 al dì)
Location:
Corso: Info phd
Anno:
Time Online: 17 Days, 17:11:50 [...]
Status: Offline

Post actions:

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

User info:

Registered: Jan 2006
Posts: 110 (0.02 al dì)
Location:
Corso: specialistica
Anno:
Time Online: 1 Day, 22:38:15 [...]
Status: Offline

Post actions:

cakkio .. davvero comodo!!
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

User info:

Registered: Jan 2006
Posts: 110 (0.02 al dì)
Location:
Corso: specialistica
Anno:
Time Online: 1 Day, 22:38:15 [...]
Status: Offline

Post actions:

.. mi viene un'altro dubbio .. ma per l'esame va bene anche un esercizio già formalizzato con clausole?

Polsy

.arcimaestro.

User info:

Registered: Dec 2003
Posts: 477 (0.06 al dì)
Location:
Corso: Info phd
Anno:
Time Online: 17 Days, 17:11:50 [...]
Status: Offline

Post actions:

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

User info:

Registered: Jan 2006
Posts: 110 (0.02 al dì)
Location:
Corso: specialistica
Anno:
Time Online: 1 Day, 22:38:15 [...]
Status: Offline

Post actions:

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

.arcimaestro.

User info:

Registered: Dec 2003
Posts: 477 (0.06 al dì)
Location:
Corso: Info phd
Anno:
Time Online: 17 Days, 17:11:50 [...]
Status: Offline

Post actions:

è 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

User info:

Registered: Jan 2006
Posts: 110 (0.02 al dì)
Location:
Corso: specialistica
Anno:
Time Online: 1 Day, 22:38:15 [...]
Status: Offline

Post actions:

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

.arcimaestro.

User info:

Registered: Dec 2003
Posts: 477 (0.06 al dì)
Location:
Corso: Info phd
Anno:
Time Online: 17 Days, 17:11:50 [...]
Status: Offline

Post actions:

identità = uguaglianza

rik

User info:

Registered: Jan 2006
Posts: 110 (0.02 al dì)
Location:
Corso: specialistica
Anno:
Time Online: 1 Day, 22:38:15 [...]
Status: Offline

Post actions:

ok .. allora il problema che avevo scelto nn va bene ..

FabryProg

User info:

Registered: Oct 2006
Posts: 116 (0.02 al dì)
Location: Novara
Corso: Informatica (Magistrale)
Anno: matricola magistrale?
Time Online: 11:09:01: [...]
Status: Offline

Post actions:

Bell'editor ... peccato che con linux nn va' :-|

FabryProg

User info:

Registered: Oct 2006
Posts: 116 (0.02 al dì)
Location: Novara
Corso: Informatica (Magistrale)
Anno: matricola magistrale?
Time Online: 11:09:01: [...]
Status: Offline

Post actions:

Errata corrige:

Non e' linux ma il fatto di inserire i vari spazi....

Vallo a capire! Ma scrivere un howto?

Woland

User info:

Registered: Jul 2005
Posts: 51 (0.01 al dì)
Location:
Corso:
Anno:
Time Online: 22:46:44 [...]
Status: Offline

Post actions:

scusate non ho ancora capito se l'esame è scritto o orale, qualcuno mi potrebbe chiarire?

Qui si dice che è orale

http://homes.dsi.unimi.it/~ghilardi/ls/lpa.html

Qui che è scritto

http://homes.dsi.unimi.it/~logica/l...ndex.html#TESTI

Inoltre qual è il sito di riferimento del corso a questo punto?

Woland

User info:

Registered: Jul 2005
Posts: 51 (0.01 al dì)
Location:
Corso:
Anno:
Time Online: 22:46:44 [...]
Status: Offline

Post actions:

dimentivcavo... io parlo di Logica matematica per la Magistrale in Informatica

yeah

.grande:maestro.

User info:

Registered: Nov 2003
Posts: 1644 (0.21 al dì)
Location: Cologno Monzese
Corso: Informatica Magistrale
Anno: II
Time Online: 12 Days, 21:36:41 [...]
Status: Offline

Post actions:

Direi che ti sei risposto da solo
Guarda le prime righe del secondo link

__________________
?