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. Uma cláusula de Horn com exatamente um literal positivo é dita uma cláusula definida (ou regra); 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.

A seguinte fórmula é um exemplo de cláusula de Horn (definida):

$\neg p \or \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 ("An evaluation of the effect of the brain-oriented organized knowledge map (Bookmap) for improving school results", Twan Brouwers & Hans Morélis, 2003) 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

Ligações externas

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.