Hornklausul

En hornsats är en disjunktiv monomial med högst en positiv bokstavlig [1] . Studerades av Alfred Horn 1951 i samband med deras viktiga roll i modellteori och universell algebra . Därefter blev de grunden för det logiska programmeringsspråket Prolog , där programmet direkt är en uppsättning Horn-satser, och fann även viktiga tillämpningar inom konstruktiv logik och beräkningskomplexitetsteori .

Konstruktion och definitioner

För positiva bokstaver kan Horn-satser ha en av följande former [1] : ${\displaystyle P,L_{i},i\in \{1,2,\dots n\))$

$L_{1}$
${\displaystyle \neg L_{1}\vee \neg L_{2}\vee \dots \vee \neg L_{n))$
${\displaystyle P\vee \neg L_{1}\vee \neg L_{2}\vee \dots \vee \neg L_{n))$

En Horn-sats med exakt en positiv bokstavlig sats är en bestämd sats ; i universell algebra är vissa satser kvasi-identiteter . En Horn-sats utan positiva bokstaver kallas ibland ett mål eller en fråga, särskilt i logisk programmering . Horns formel är en konjunktion av Horns satser, det vill säga en formel i konjunktiv normalform , vars alla satser är Horns. En dubbelhornssats är en sats med högst en negativ bokstav.

Ett exempel på en (definitiv) Horn-sats:

\neg p\lor \neg q\vee \cdots \vee \neg t\vee u

Denna formel kan konverteras till en ekvivalent formel med implikation [1] :

(p \wedge q \wedge \cdots \wedge t) \högerpil u

eller [1] :

(p\högerpil u)\wedge (q\högerpil u)\wedge \cdots \wedge (t\högerpil u)

Applikationer

Hornsatser kan vara antingen propositionsformler eller första ordningens formler , beroende på om propositionella bokstaver eller första ordningens literaler övervägs.

Hornsatser är relaterade till satsbevisande genom första ordningens upplösningar , eftersom upplösningen av två Hornsatser är en Hornsats. Dessutom är upplösningen av målet och den bestämda klausulen också en Horn-sats. I automatisk satsbevisning kan detta vara mer effektivt för att bevisa ett sats som presenteras som ett mål.

Målupplösning med en specifik klausul för att erhålla ett nytt mål är grunden för slutledningsregeln i SLD-upplösning , som används för att implementera logisk programmering och programmeringsspråket Prolog . I logisk programmering används en bestämd klausul som en målminskningsprocedur. Till exempel fungerar klausulen från exemplet ovan som en procedur: "to show , show , , och ". $\neg p\lor \neg q\vee \cdots \vee \neg t\vee u$ $u$ $sid$ $q$ $\cdots$ $t$

För att betona denna omvända tillämpning av disjunkten, används ofta operatorn : $\vänster pil$

u\leftarrow (p\land q\land \cdots \land t)

I Prolog skrivs detta som:

u :- p, q, ..., t.

Propositionella Horn-satser är också av intresse i beräkningskomplexitetsteori , där HORNSAT-problemet med att hitta en uppsättning sanningsvärden som uppfyller hornsatsernas konjunktion är P-komplett . Detta är en klass P-variant för SAT , det viktigaste NP-kompletta problemet. Problemet med tillfredsställelse av Horn-satser av första ordningen är inte lösbart.

Anteckningar

↑ 1 2 3 4 Ricardo Caferra. Logik för datavetenskap och artificiell intelligens. - John Wiley & Sons, 2013. - 537 sid. — ISBN 978-1-118-60426-7 .

Litteratur

Alfred Horn. På meningar som är sanna för direkta föreningar av algebror // Journal of Symbolic Logic . - 1951. - T. 16 .

Länkar

Alex Sacharov. Horn Clause (engelska) på Wolfram MathWorld- webbplatsen .