Cláusula de Horn

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa
NoFonti.svg
Este artigo ou se(c)ção cita uma ou mais fontes fiáveis e independentes, mas ela(s) não cobre(m) todo o texto (desde Março de 2013).
Por favor, melhore este artigo providenciando mais fontes fiáveis e independentes e inserindo-as em notas de rodapé ou no corpo do texto, conforme o livro de estilo.
Encontre fontes: Googlenotícias, livros, acadêmicoScirusBing. Veja como referenciar e citar as fontes.

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 é \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 [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.
com exatamente um literal positivo é dita ; 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 \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[editar | editar código-fonte]

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. a b Ernest Davis, New York University, Computer Science Department, Artificial Intelligence, Horn clause logic [em linha]