Tesi

Last changes : - / RSS
// 2011/04/27 19:51 / 193.204.187.254
// 2011/04/27 19:52 / 193.204.187.254
'''Titolo''': Theta-Sussunzione tra clausole di Horn: riduzione di un problema NP-Completo a un problema di Soddisfacibilità Booleana.

'''Abstract''': l'efficienza delle procedure di dimostrazione nella logica del prim'ordine è un problema rilevante nel caso gli agenti deduttivi vengano usati in ambienti reali, sia da soli sia come componente di un sistema più grande (ad es. in sistemi di apprendimento). Questa tesi propone un nuovo algoritmo di theta-sussunzione basato su una Karp-riduzione polinomiale dell'input in istanze del problema della Soddisfacibilità Booleana.

[Tesi|/repository/tesi/tesi.pdf], [Slides|/repository/tesi/slides.pdf]


[Codice Proof-of-Concept|/repository/tesi/SATheta-1.1.tar.gz]

sample usage:

pasquale@dell:~/stuff/sat/SATheta-1.1$ make
$ make
g++ *.cpp *.cc -o SATheta
pasquale@dell:~/stuff/sat/SATheta-1.1$ printf "a(X) :- b(Y).\na(X) :- b(a).\n" | ./SATheta /dev/stdin
$ printf "a(X) :- b(Y).\na(X) :- b(a).\n" | ./SATheta /dev/stdin
c time required: 0
c
c generated by SATheta 1.1
c

p cnf 4 6
1 0
-2 0
-1 -3 0
-2 -4 0
1 3 0
2 4 0