.dsy:it. (http://www.dsy.it/forum/)
- Logica matematica (http://www.dsy.it/forum/forumdisplay.php?forumid=246)
-- Log Mat x Informatica Magistrale (http://www.dsy.it/forum/showthread.php?threadid=39542)

Log Mat x Informatica Magistrale

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!