Horn-lauseke – määritelmä, ominaisuudet ja Prolog-sovellukset

Horn-lauseke: selkeä määritelmä, keskeiset ominaisuudet ja Prolog-sovellukset — käytännön esimerkit, teoria ja tehokkuus logiikkaohjelmoinnissa.

Horn-lauseke on logiikan disjunktio, jossa enintään yksi literali on positiivinen ja kaikki muut ovat negatiivisia. Nimi tulee Alfred Hornista, joka kuvasi ne artikkelissaan vuonna 1951.

Määrittelyt ja esimerkit

Horn-lausekkeet voidaan luokitella kolmeen alaluokkaan:

• definitiivilauseke (Horn-lauseke, jossa on täsmälleen yksi positiivinen literali);
• fakta (definitiivilauseke, jossa ei ole negatiivisia literaaleja — pelkkä positiivinen atom);
• tavoitelauseke (Horn-lauseke, jossa ei ole positiivista literalia — kaikki literaalit ovat negatiivisia).

Näitä kolmea tyyppiä havainnollistetaan seuraavassa esimerkissä:

definitiivilauseke: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t ∨ u {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u}

fakta: u {\displaystyle u}

tavoitelauseke: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t}

Ei-propositionaalinen tapaus ja kvantifiointi

Ei-propositionaalisessa (ensimmäisen kertaluvun) tapauksessa lausekkeen muuttujat ymmärretään yleensä universaalisti kvantifioiduiksi koko lausekkeen yli. Esimerkiksi lause

¬ human ( X ) ∨ mortal ( X ) {\displaystyle \neg {\text{human}}(X)\lor {\text{mortal}}(X)}

tarkoittaa

∀ X ( ¬ human ( X ) ∨ mortal ( X ) ) {\displaystyle \forall X(\neg {\text{human}}(X)\lor {\text{mortal}}(X))} }

ja tämä on loogisesti yhtäpitävä implikaation kanssa:

∀ X ( ihminen ( X ) → kuolevainen ( X ) ) . {\displaystyle \forall X({\text{human}}(X)\rightarrow {\text{mortal}}(X)). }

Ominaisuudet ja laskennallinen merkitys

Horn-lausekkeilla on keskeinen asema konstruktiivisessa ja laskennallisessa logiikassa. Niillä on useita hyödyllisiä ominaisuuksia:

• Resoluutio Horn-lausekkeiden välillä säilyttää Horn-muodon: kahden Horn-lauseen resoluutio on jälleen Horn-lause. Tämä tekee automaattisesta todistamisesta tehokkaampaa, koska avaruus mahdollisesti pysyy rajoittuneena.
• Jos resolvoidaan tavoitelause (goal clause) ja faktalauseke, tuloksena on jälleen tavoitelause — ominaisuus, jota hyödynnetään tavoiteohjatussa päättelyssä.
• Näiden ominaisuuksien ansiosta Horn-lausekkeiden todistustehtävät voidaan usein tehdä tehokkaammin kuin yleisillä lausekkeilla; esimerkiksi propositionaalisten Horn-lausekkeiden tyydyttävyystarkistus (HORNSAT) on ratkaistavissa lineaarisessä ajassa.

Propositionaalinen HORNSAT on P-luokkaan kuuluva (itse asiassa lineaariajassa ratkaistava) ongelma, kun taas yleinen Boolen tyydyttävyysongelma on NP-täydellinen. Ensimmäisen kertaluvun (ei-propositionaalisten) Horn-lausekkeiden yleinen tyydyttävyysongelma on ratkaisematon.

Yhteys logiikkaohjelmointiin ja Prologiin

Horn-lausekkeet muodostavat logiikkaohjelmoinnin teoreettisen perustan. On tavallista esittää definitiiviset lausekkeet implikaation muodossa, joka vastaa intuitionistista ohjelmallista tulkintaa:

( p ∧ q ∧ ⋯ ∧ t ) → u {\displaystyle (p\wedge q\wedge \cdots \wedge t)\rightarrow u}

Tavoitelausekkeen resoluutio definitiivisen lausekkeen kanssa uuden tavoitelausekkeen tuottamiseksi on juuri se päättelyaskel, jota käytetään logiikkaohjelmoinnin ja ohjelmointikielen Prologin SLD-resoluutioksi (Selective Linear Definite clause resolution). Tämä vastaa taaksepäin suuntautuvaa päättelyä (backward chaining): kun pyritään todistamaan tavoitetta, se jaetaan alitavoitteisiin käyttäen määrittelylausekkeita.

Esimerkiksi edellä oleva implikaatio vastaa proseduuria, joka sanoo: "voidaan näyttää u, jos voidaan näyttää p, q, … ja t". Taaksepäin suuntautuva kirjoitus on yleisesti käytetty notaatio:

u ← ( p ∧ q ∧ ⋯ ∧ t ) {\displaystyle u\leftarrow (p\land q\land \cdots \land t)}

Prologissa sama lause kirjoitetaan seuraavasti:

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

Prologin syntaksi on käytännössä monimerkityksinen esimerkiksi kvantifioinnin tulkinnassa ja negation käsittelyssä: lausekkeen muuttujat voidaan tulkita universaalisesti tai eksistentiaalisesti, ja "false"-lausekkeen johtaminen voi merkitä ristiriidan löytymistä tai onnistunutta ratkaisua haetulle ongelmalle. Lisäksi Prolog sisältää mekanismeja kuten negation-as-failure, jotka yleistävät perinteisiä Horn-lausekkeita mutta tuovat mukanaan semanttisia nyansseja.

Semantiikka: minimimalli ja stabiilit mallit

Van Emden ja Kowalski (1976) tutkivat määrällisten (definitiivilausekkeiden) joukkojen malliteoreettisia ominaisuuksia loogisen ohjelmoinnin kontekstissa. He osoittivat, että jokaisella määrittelylausekkeiden joukolla D on yksikäsitteinen minimimalli M. Atomikaava A on loogisesti seuraus D:stä jos ja vain jos A on tosi M:ssä. Tämä antaa luonnollisen mallisemantiikan loogisille ohjelmille: ohjelman totuusarvot määräytyvät sen minimimallin mukaan.

Tämä minimimallin semantiikka liittyy myös stabiilien mallien semantiikkaan: Horn-ohjelmilla stabiili malli on yksikäsitteinen ja vastaa minimimallia. Näin Horn-lausekkeet tarjoavat yksinkertaisen ja hyvin ymmärrettävän semanttisen kehikon logiikkaohjelmien käyttäytymiselle.

Käytännön päättelymenetelmät

Käytännössä Horn-lausekkeille on kaksi yleistä päättelystrategiaa:

• taaksepäin suuntautuva päättely (backward chaining) — tavoitteesta aloittava, jota Prolog käyttää (SLD-resoluutio); tehokas, kun vain tiettyihin tavoitteisiin liittyvä tieto on kiinnostavaa;
• eteenpäin suuntautuva päättely (forward chaining) — faktaavaruuden laajentaminen deduktiivisesti (esim. materiaalisaatio), jota käytetään usein tuotussääntijärjestelmissä ja tietyissä tietokantayhteyksissä (Datalog).

Horn-lausekkeiden rajoitukset kannattaa huomioida: ne eivät yksinään ilmaise helposti joissain sovelluksissa tarvittavia epädirektiivisiä relaatioita tai monimutkaista epävarmuutta; laajennukset (kuten negation-as-failure, funktiotermin käyttö tai stabiili malli -laajennukset) lisäävät ilmaisukykyä mutta voivat muuttaa laskennallisia ja semanttisia ominaisuuksia.

Yhteenveto

Horn-lausekkeet ovat kevyt mutta voimakas lausekenttä, jolla on vankka teoreettinen perusta ja monia käytännön sovelluksia erityisesti logiikkaohjelmoinnissa ja automaattisessa päättelyssä. Niiden erikoisrakenne mahdollistaa tehokkaan päättelyn (esimerkiksi HORNSATin lineaarinen ratkaistavuus ja resoluution sulkeutuvuus), minkä vuoksi ne muodostavat käytännöllisen valinnan moniin formaaleihin ja ohjelmallisiin tehtäviin.

Kysymyksiä ja vastauksia

K: Mikä on sarvilauseke?

K: Kuka kuvasi ne ensimmäisenä?

Kysymys: Mikä on definitiivinen lauseke?

K: Mikä on fakta?

K: Mikä on tavoitelause?

K: Miten muuttujat toimivat ei-propositiotapauksissa?

Hae kirjaimella