AULA 16
15 Novembro 2016, 10:30 • Fernando Ferreira
Descrição do algoritmo de satisfação de Horn. Mais um exemplo.
O método da resolução para mostrar que uma sentença em FNC não é tt-satisfazível. Resolventes de duas cláusulas (disjuntivas). Alguns exemplos.