Clauza de corn

O clauză Horn este un monom disjunctiv cu cel mult un literal pozitiv [1] . Studiat de Alfred Horn în 1951 în legătură cu rolul lor important în teoria modelelor și algebra universală . Ulterior, au devenit baza pentru limbajul de programare logic Prolog , în care programul este direct un set de clauze Horn, și au găsit, de asemenea, aplicații importante în logica constructivă și teoria complexității computaționale .

Construcție și definiții

Pentru literalele pozitive , clauzele Horn pot lua una dintre următoarele forme [1] : $P,L_{i},i\in \{1,2,\dots n\)$

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

O clauză Horn cu exact un literal pozitiv este o clauză definită ; în algebra universală , anumite propoziții sunt cvasi-identități . O clauză Horn fără literale pozitive este uneori numită țintă sau interogare, în special în programarea logică . Formula lui Horn este o conjuncție a propozițiilor lui Horn, adică o formulă în formă normală conjunctivă , ale cărei propoziții sunt toate ale lui Horn. O clauză Horn dublă este o clauză cu cel mult un literal negativ.

Un exemplu de clauză Horn (definită):

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

Această formulă poate fi convertită într-o formulă echivalentă cu implicația [1] :

(p \wedge q \wedge \cdots \wedge t) \rightarrow u

sau [1] :

(p\rightarrow u)\wedge (q\rightarrow u)\wedge \cdots \wedge (t\rightarrow u)

Aplicații

Propozițiile corn pot fi fie formule propoziționale , fie formule de ordinul întâi , în funcție de dacă sunt luate în considerare literale propoziționale sau literale de ordinul întâi.

Clauzele Horn sunt legate de demonstrarea teoremei prin rezoluții de ordinul întâi , deoarece rezoluția a două clauze Horn este o clauză Horn. Mai mult, rezoluția scopului și a clauzei definitive este și o clauză Horn. În demonstrarea automată a teoremei , aceasta poate fi mai eficientă în demonstrarea unei teoreme prezentate ca scop.

Rezoluția obiectivului cu o clauză specifică pentru obținerea unui nou scop stă la baza regulii de inferență în rezoluția SLD , utilizată pentru implementarea programarii logice și a limbajului de programare Prolog . În programarea logică, o clauză definită este utilizată ca procedură de reducere a obiectivelor. De exemplu, clauza din exemplul de mai sus funcționează ca o procedură: "to show , show , and " . $\neg p\lor \neg q\vee \cdots \vee \neg t\vee u$ $u$ $p$ $q$ $\cdots$ $t$

Pentru a sublinia această aplicare inversă a disjunctului, se folosește adesea operatorul : $\sageata stanga$

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

În Prolog , aceasta este scrisă astfel:

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

Propozițiile Horn propoziționale sunt de asemenea de interes în teoria complexității computaționale , unde problema HORNSAT de a găsi un set de valori de adevăr care îndeplinesc conjuncția clauzelor Horn este P-complet . Aceasta este o variantă de clasa P pentru SAT , cea mai importantă problemă NP-completă . Problema satisfacabilității clauzelor Horn de ordinul întâi nu este rezolvabilă.

Note

↑ 1 2 3 4 Ricardo Caferra. Logica pentru informatică și inteligență artificială. - John Wiley & Sons, 2013. - 537 p. — ISBN 978-1-118-60426-7 .

Literatură

Alfred Horn. Despre propoziții care sunt adevărate pentru uniunile directe ale algebrelor // Journal of Symbolic Logic . - 1951. - T. 16 .

Link -uri

Alex Saharov. Clauza Horn (engleză) pe site-ul Wolfram MathWorld .