Tesi

Last changes : 2011/04/27 19:52 / RSS
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, Slides


Codice Proof-of-Concept

sample usage:

$ make
g++ *.cpp *.cc -o SATheta
$ 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