Cláusula de Horn

Em lógica, uma cláusula de Horn é uma cláusula (disjunção de literais) com no máximo um literal positivo.

O nome "Cláusula de Horn" é uma homenagem ao lógico Alfred Horn, que foi quem primeiro chamou a atenção para o valor destas cláusulas, em 1951, no artigo "On sentences which are true of direct unions of algebras", Journal of Symbolic Logic, 16, 14-21.

Uma cláusula de Horn pode ser de quatro tipos diferentes:

1. uma regra tem um literal positivo, e pelo menos um literal negativo. Sua forma é $\neg P_{1}\lor \neg P_{2}\lor \cdots \neg P_{k}\lor Q,$ que é logicamente equivalente a $(P_{1}\land P_{2}\land \cdots P_{k})\rightarrow Q.$ Exemplo: todo homem é mortal, ou seja, X não é um homem ou X é mortal;
2. um fato ou unidade é um literal positivo sem nenhum literal negativo. Por exemplo, Sócrates é um homem, todo mundo é parente de si mesmo
3. um objetivo negado não tem nenhum literal positivo, e pelo menos um literal negativo. Em programação, a base de dados consiste de regras e fatos, e um objetivo negado corresponde à negação do fato que se deseja provar, por exemplo, para se encontrar um descendente masculino de Isabel, o objetivo a ser provado é X é homem e Isabel é ancestral de X, então o objetivo negado será X não é homem ou Isabel não é ancestral de X
4. a cláusula nula não tem nenhum literal positivo e nenhum literal negativo. Na programação, ela aparece no final de uma demonstração.

Uma cláusula de Horn com exatamente um literal positivo é dita cláusula definitiva; uma cláusula de Horn sem literais positivos é às vezes dita cláusula objetivo (ou fato), especialmente no contexto da programação lógica. Uma fórmula de Horn é uma fórmula na forma normal conjuntiva cujas cláusulas são todas de Horn; em outras palavras, é uma conjunção de cláusulas de Horn. Uma cláusula de Horn dual é uma cláusula com no máximo um literal negativo. As cláusulas de Horn têm um papel essencial na programação lógica e são importantes na lógica construtiva.

$$\neg p\lor \neg q\vee \cdots \vee \neg t\vee u$$

Em Prolog isto se escreve como:

 u :- p, q, … , t

Usando a lógica clássica proposicional, tal fórmula pode ser reescrita ainda, de forma equivalente, da seguinte forma:

$$(p\wedge q\wedge \cdots \wedge t)\rightarrow u$$

A relevância das cláusulas de Horn para demonstrações de teoremas através do princípio da resolução reside no fato de que a resolução de duas cláusulas de Horn é uma cláusula de Horn. Além disso, a resolução de uma cláusula objetivo e uma cláusula definida dá origem a uma nova cláusula objetivo, e resoluções deste gênero dão base à programação lógica e à linguagem de programação Prolog. No contexto da demonstração automática de teoremas, resoluções envolvendo cláusulas de Horn podem ser usadas para a definição de algoritmos eficientes para a verificação de teoremas (representados como uma cláusulas objetivos).

As cláusulas de Horn são também de interesse no estudo da complexidade computacional, onde o problema de encontrar um conjunto de valorações para as variáveis de modo a satisfazer uma conjunção de cláusulas de Horn é um problema P-completo, às vezes chamado HORNSAT. Este problema é a versão P do problema de satisfatibilidade booleana, um problema NP-completo fundamental.

Vale a pena mencionar ainda que um estudo recente mostrou que diagramas baseados em cláusulas de Horn podem ter um efeito positivo na compreensão do conhecimento científico complexo por parte de estudantes de nível secundário.

Ver também

• Forma Normal Conjuntiva