Cláusula de Horn - Horn clause
Em lógica matemática e programação lógica , uma cláusula de Horn é uma fórmula lógica de uma forma semelhante a uma regra particular que lhe dá propriedades úteis para uso em programação lógica, especificação formal e teoria do modelo . As cláusulas de Horn são nomeadas em homenagem ao lógico Alfred Horn , que primeiro apontou seu significado em 1951.
Definição
Uma cláusula de Horn é uma cláusula (uma disjunção de literais ) com no máximo um literal positivo, isto é , não legado .
Por outro lado, uma disjunção de literais com no máximo um literal negado é chamada de cláusula de Horn dual .
Uma cláusula de Horn com exatamente um literal positivo é uma cláusula definida ou uma cláusula de Horn estrita ; uma cláusula definida sem literais negativos é uma cláusula unitária , e uma cláusula unitária sem variáveis é um fato ; Uma cláusula de Horn sem um literal positivo é uma cláusula de objetivo . Observe que a cláusula vazia, que consiste em nenhum literal (que é equivalente a false ), é uma cláusula de objetivo. Esses três tipos de cláusulas de Horn são ilustrados no seguinte exemplo proposicional :
| Cláusula de tipo de chifre | Forma de disjunção | implicação forma | Leia intuitivamente como |
|---|---|---|---|
| Cláusula definida | ¬ p ∨ ¬ q ∨ ... ∨ ¬ t ∨ u | u ← p ∧ q ∧ ... ∧ t | supor que, se p e q e ... t tudo espera, em seguida, também u detém |
| Facto | você | u ← verdade | suponha que você segura |
| Cláusula de meta | ¬ p ∨ ¬ q ∨ ... ∨ ¬ t | falso ← p ∧ q ∧ ... ∧ t | mostre que p e q e ... e t todos se mantêm |
Todas as variáveis em uma cláusula são universalmente quantificadas implicitamente, com o escopo sendo a cláusula inteira. Assim, por exemplo:
- ¬ humano ( X ) ∨ mortal ( X )
apoia:
- ∀X (¬ humano ( X ) ∨ mortal ( X ))
que é logicamente equivalente a:
- ∀X ( humano ( X ) → mortal ( X ))
Significado
As cláusulas de Horn desempenham um papel básico na lógica construtiva e na lógica computacional . Eles são importantes na prova automatizada de teoremas por resolução de primeira ordem , porque o resolvente de duas cláusulas de Horn é ele mesmo uma cláusula de Horn, e o resolvente de uma cláusula de objetivo e uma cláusula definida é uma cláusula de objetivo. Essas propriedades das cláusulas de Horn podem levar a uma maior eficiência de provar um teorema: a cláusula objetivo é a negação desse teorema; consulte a cláusula de meta na tabela acima. Intuitivamente, se quisermos provar φ, assumimos ¬φ (o objetivo) e verificamos se tal suposição leva a uma contradição. Nesse caso, então φ deve se manter. Dessa forma, uma ferramenta de prova mecânica precisa manter apenas um conjunto de fórmulas (suposições), ao invés de dois conjuntos (suposições e (sub) objetivos).
As cláusulas de Horn proposicionais também são de interesse na complexidade computacional . O problema de encontrar atribuições de valor de verdade para tornar verdadeira uma conjunção de cláusulas de Horn proposicionais é conhecido como HORNSAT . Este problema é P-completo e pode ser resolvido em tempo linear . Observe que o problema de satisfatibilidade booleana irrestrita é um problema NP-completo .
Programação lógica
As cláusulas de Horn também são a base da programação lógica , onde é comum escrever cláusulas definidas na forma de uma implicação :
- ( p ∧ q ∧ ... ∧ t ) → u
Na verdade, a resolução de uma cláusula de objetivo com uma cláusula definida para produzir uma nova cláusula de objetivo é a base da regra de inferência de resolução SLD , usada na implementação da linguagem de programação lógica Prolog .
Na programação lógica, uma cláusula definida se comporta como um procedimento de redução de metas. Por exemplo, a cláusula de Horn escrita acima se comporta como o procedimento:
- para mostrar u , mostrar p e mostrar q e ... e mostrar t .
Para enfatizar esse uso reverso da cláusula, muitas vezes ela é escrita na forma reversa:
- u ← ( p ∧ q ∧ ... ∧ t )
No Prolog, isso é escrito como:
u :- p, q, ..., t.
Na programação lógica, a computação e a avaliação da consulta são realizadas representando a negação de um problema a ser resolvido como uma cláusula objetivo. Por exemplo, o problema de resolver a conjunção quantificada existencialmente de literais positivos:
- ∃ X ( p ∧ q ∧ ... ∧ t )
é representado negando o problema (negando que ele tenha uma solução) e representando-o na forma logicamente equivalente de uma cláusula de objetivo:
- ∀ X ( falso ← p ∧ q ∧ ... ∧ t )
No Prolog, isso é escrito como:
:- p, q, ..., t.
Resolver o problema equivale a derivar uma contradição, que é representada pela cláusula vazia (ou "falsa"). A solução do problema é a substituição das variáveis da cláusula objetivo por termos, o que pode ser extraído da prova de contradição. Usadas dessa forma, as cláusulas de objetivo são semelhantes às consultas conjuntivas em bancos de dados relacionais, e a lógica da cláusula de Horn é equivalente em poder computacional a uma máquina de Turing universal .
A notação Prolog é realmente ambígua, e o termo “cláusula de objetivo” às vezes também é usado de forma ambígua. As variáveis em uma cláusula de objetivo podem ser lidas como universal ou existencialmente quantificadas, e derivar "falso" pode ser interpretado como derivando uma contradição ou como derivando uma solução bem-sucedida do problema a ser resolvido.
Van Emden e Kowalski (1976) investigaram as propriedades do modelo de teoria de cláusulas de Horn no contexto de programação lógica, mostrando que cada conjunto de cláusulas definidas D tem um único modelo mínimo M . Uma fórmula atómica Um é logicamente implicada por D se e apenas se um é verdadeiro em H . Segue-se que um problema P representado por um conjunto existentially quantificada de literais positivos é logicamente implicada por D se e somente se P é verdadeiro em H . A semântica do modelo mínimo das cláusulas de Horn é a base para a semântica do modelo estável dos programas lógicos.