Hornklausul - Horn clause
I matematisk logik og logisk programmering er en Horn-klausul en logisk formel for en bestemt regellignende form, som giver den nyttige egenskaber til brug i logisk programmering, formel specifikation og modelteori . Hornklausuler er opkaldt efter logikeren Alfred Horn , der først påpegede deres betydning i 1951.
Definition
En Horn-klausul er en klausul (en adskillelse af bogstaver ) med højst en positiv, dvs. ikke- negeret , bogstavelig.
Omvendt kaldes en adskillelse af bogstaver med højst en negeret bogstavelig dobbelt-Horn-klausul .
En Horn-klausul med nøjagtigt en positiv bogstav er en bestemt klausul eller en streng Horn-klausul ; en bestemt sætning uden negative bogstaver er en enhedsklausul , og en enhedsklausul uden variabler er en kendsgerning . En Horn-klausul uden en positiv bogstavelig er en målklausul . Bemærk, at den tomme klausul, der ikke består af bogstaver (svarende til falsk ), er en målklausul. Disse tre slags Horn-klausuler er illustreret i følgende propositioneksempel :
| Horn-klausul | Disjunktionsformular | Følgevirkning formular | Læs intuitivt som |
|---|---|---|---|
| Definitiv klausul | ¬ p ∨ ¬ q ∨ ... ∨ ¬ t ∨ u | u ← p ∧ q ∧ ... ∧ t | antag, at hvis p og q og ... og t alle holder, så holder også u |
| Faktum | u | u ← sandt | antag at du holder |
| Målklausul | ¬ p ∨ ¬ q ∨ ... ∨ ¬ t | falsk ← p ∧ q ∧ ... ∧ t | vis at p og q og ... og t holder alle nede |
Alle variabler i en klausul kvantificeres implicit universelt, idet omfanget er hele klausulen. Således for eksempel:
- ¬ menneske ( X ) ∨ dødelig ( X )
står for:
- ∀X (¬ human ( X ) ∨ dødelig ( X ))
hvilket logisk svarer til:
- ∀X ( menneske ( X ) → dødelig ( X ))
Betydning
Hornklausuler spiller en grundlæggende rolle i konstruktiv logik og beregningslogik . De er vigtige i automatiseret sætning, der viser ved første ordens opløsning , fordi resolvent af to Horn-klausuler i sig selv er en Horn-klausul, og resolvent af en målklausul og en bestemt klausul er en målklausul. Disse egenskaber ved Horn-klausuler kan føre til større effektivitet ved at bevise en sætning: målsætningen er negationen af denne sætning; se målklausul i ovenstående tabel. Intuitivt, hvis vi ønsker at bevise φ, antager vi ¬φ (målet) og kontrollerer, om en sådan antagelse fører til en modsigelse. I så fald skal φ holde. På denne måde behøver et mekanisk bevisværktøj kun at opretholde et sæt formler (antagelser) snarere end to sæt (antagelser og (under) mål).
Propositionelle Horn-klausuler er også af interesse for beregningskompleksitet . Problemet med at finde sandhedsværditildelinger for at gøre en kombination af propositionelle Horn-klausuler kendt er HORNSAT . Dette problem er P-komplet og kan løses på lineær tid . Bemærk, at det ubegrænsede Boolske tilfredshedsproblem er et NP-komplet problem.
Logisk programmering
Hornklausuler er også grundlaget for logisk programmering , hvor det er almindeligt at skrive bestemte klausuler i form af en implikation :
- ( p ∧ q ∧ ... ∧ t ) → u
Faktisk er opløsningen af en målklausul med en bestemt klausul for at producere en ny målklausul grundlaget for SLD-opløsningens inferensregel, der anvendes til implementering af det logiske programmeringssprog Prolog .
I logisk programmering opfører en bestemt klausul sig som en målreduktionsprocedure. F.eks. Opfører Horn-klausulen sig som proceduren:
- for at vise u , vise p og vise q og ... og vise t .
For at understrege denne omvendte anvendelse af klausulen skrives den ofte i omvendt form:
- u ← ( p ∧ q ∧ ... ∧ t )
I Prolog er dette skrevet som:
u :- p, q, ..., t.
I logisk programmering udføres beregning og forespørgsel ved at repræsentere negationen af et problem, der skal løses som en målklausul. F.eks. Problemet med at løse den eksistentielt kvantificerede forbindelse af positive bogstaver:
- ∃ X ( p ∧ q ∧ ... ∧ t )
repræsenteres ved at negere problemet (benægte at det har en løsning) og repræsentere det i den logisk ækvivalente form af en målklausul:
- ∀ X ( falsk ← p ∧ q ∧ ... ∧ t )
I Prolog er dette skrevet som:
:- p, q, ..., t.
Løsning af problemet svarer til at udlede en modsigelse, som er repræsenteret af den tomme klausul (eller "falsk"). Løsningen på problemet er en erstatning af udtryk for variablerne i målsætningen, som kan udvindes fra beviset for modsigelse. Brugt på denne måde svarer målklausuler til konjunktive forespørgsler i relationelle databaser, og Horn-klausullogik svarer i beregningskraft til en universel Turing-maskine .
Prolog-notationen er faktisk tvetydig, og udtrykket ”målklausul” bruges undertiden også tvetydigt. Variablerne i en målsætning kan læses som universelt eller eksistentielt kvantificerede, og afledning af "falsk" kan fortolkes enten som afledning af en modsigelse eller som udledning af en vellykket løsning på problemet, der skal løses.
Van Emden og Kowalski (1976) undersøgte model-teoretisk egenskaber Horn klausuler i forbindelse med logisk programmering, der viser, at hvert sæt af bestemte klausuler D har en unik minimal model M . En atomar formel A er logisk antydes af D hvis og kun hvis A er sandt i M . Heraf følger, at et problem P repræsenteret af en eksistentielt kvantificeret sammenholdt af positive litteraler logisk kan udledes af D hvis og kun hvis P er sandt i M . Den minimale modelsemantik i Horn-klausuler er grundlaget for den stabile model semantik i logiske programmer.