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.^[1]

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]

1. uma regra tem um literal positivo, e pelo menos um literal negativo. Sua forma é ${\displaystyle \neg P_{1}\lor \neg P_{2}\lor \cdots \neg P_{k}\lor Q,}$ que é logicamente equivalente a ${\displaystyle (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 ^{[Nota 1]}
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.

$${\displaystyle \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:

$${\displaystyle (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 ^[2] 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

Notas e referências

Notas

1. Na fonte consultada, a frase é todo mundo é ancestral de si mesmo, o que está em desacordo com o uso normal de ancestral em português.

Referências

1. Ernest Davis, New York University, Computer Science Department, Artificial Intelligence, Horn clause logic [em linha]
2. Twan Brouwers & Hans Morélis. "An evaluation of the effect of the brain-oriented organized knowledge map (Bookmap) for improving school results", 2003

• Portal da matemática