Cláusula de Horn
Origem: Wikipédia, a enciclopédia livre.
Na 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 é uma cláusula definida; uma cláusula de Horn sem literais positivos é às vezes dita cláusula objetivo, especialmente na 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):
Em Prolog isto aparece como:
u :- p, q, ..., t
Tal fórmula pode ser reescrita na forma seguinte, a qual é mais comum na programação lógica e em outras áreas:
A relevância das cláusulas de Horn para demonstrações de teoremas através da resolução de primeira ordem, é que a resolução de duas cláusulas de Horn é um cláusula de Horn. Além disso, a resolução de uma cláusula objetivo e uma cláusula definida é também uma cláusula objetivo. Em demonstrações automática de teoremas, isso pode levar a uma maior eficiência na demosntração de um teorema (representado como uma cláusula objetivo). Com efeito, Prolog é uma linguagem de programação baseada nas cláusulas de Horn (o Prolog também inclui construtores tais como o operador cut que não pode ser facilmente expressa na lógica clássica).
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 para satisfazer uma conjunção de cláusulas de Horn, é um problema P-completo, às vezes chamado HORNSAT. Esse é a versão P do problema de satisfatibilidade booleana, um problema NP-completo fundamental.
Uma pesquisa 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 nas cláusulas de Horn melhoram o entendimento humano de problemas complexos.
[editar] Veja também
[editar] Ligações Externas
O nome "Cláusula de Horn" veio do lógico Alfred Horn, quem primeiro chamou a atenção para a significância cláusulas em 1951, no artigo "On sentences which are true of direct unions of algebras", Journal of Symbolic Logic, 16, 14-21.
