.dsy:it. - Logica matematica - Log Mat x Informatica Magistrale

Il progetto dsy.it è l'unofficial support site dei corsi di laurea del Dipartimento di Scienze dell'Informazione e del Dipartimento di Informatica e Comunicazione della Statale di Milano. E' un servizio degli studenti per gli studenti, curato in modo no-profit da un gruppo di essi. I nostri servizi comprendono aree di discussione per ogni Corso di Laurea, un'area download per lo scambio file, una raccolta di link e un motore di ricerca, il supporto agli studenti lavoratori, il forum hosting per Professori e studenti, i blog, e molto altro...
In questa sezione è indicizzato in textonly il contenuto del nostro forum

.dsy:it. Archive > Didattica > Corsi G - M > Logica matematica

Log Mat x Informatica Magistrale
Clicca QUI per vedere il messaggio nel forum

zacguyot

Raga,

qualcuno sarebbe così gentile da darmi 2 semplici informazioni?

1. Per la parte "Il teorema di Herbrand" ho visto che sulle slides viene data solo la definizione e poi dice skolemizzare , astrarre proposizionalmente e testare l'insoddisfacibilità con un SAT-solver. Qui il prof, all'esame, oltre a chiedere la definizione chiede altro?

2. Per il progetto da fare in Spass, ci sono indicazioni particolari da parte del prof? qualcuno mi sa dare qualche dettaglio in +? devo fare un progetto simile ad uno di quelli della libreria TPTP e saper commentare l'output facendo capire che si conoscono regole di risoluzione usate dal dimostratore?

grazie!