Hornin lause on muotoa:
H <-- B1, B2, ..., Bn
H on kärki (head) ja B1, B2, ..., Bn on
runko (body).
Ilmauksen semantiikka on "Jos jokainen Bi on tosi, kun i=1, ...n, myös H on tosi.
Jos (ja kun!) kärki ja runko sisältävät muuttujia, kärjen muuttujat ajatellaan universaalikvantifioiduiksi, kärjessä esiintymättömät (eli kärjen vapaiksi jättämät) rungon muuttujat eksistentiaalikvantifioiduiksi. Esimerkiksi
X < Y <-- X < Z, Z < Yvoidaan lukea: "Jokaiselle X ja Y pätee, että X on pienempi kuin Y, jos on olemassa sellainen Z, jota pienempi X on ja jota suurempi Y on."
Predikaatteja kirjoitetaan usein tyyliin pienempi(X, Y), jne..., ja siten vaikkapa edellinen voitaisiin kirjoittaa muodossa
pienempi(X,Y) <-- pienempi(X,Z), pienempi(Z,Y)
Jos Hornin lause on pelkkä kärki ilman runkoa, kyseessä on "fakta". Jos Hornin lause on pelkkä runko ilman kärkeä, kyseessä on on kysely tai tavoite, "query", "top-level goal". Kun Hornin lauseessa on molemmat osat, kyseessä on sääntö, "rule".
Esimerkkejä:
tykkää(maija, jäätelö) tykkää(maija, pekka) tykkää(pekka, maija) tykkää(jussi, maija) tykkää(X,Y) <-- tykkää(X,Z), tykkää(Z,Y) // transitiivinen (ohjelmointivirhe?) tykkää(X,Y) <-- tykkää(Y,X) // symmetrinen (ohjelmointivirhe?) <-- tykkää(jussi, X) X=maija X=jäätelö X=pekka
Entä tykkääkö jussi itsestään?
Päättelysääntöjä voidaan Hornin lauseita käyttäen ajatella sovellettavan tyyliin:
C <-- A, B D <-- C ----------- D <-- A, BEsimerkiksi:
kuolevainen(X) <-- ihminen(X) ihminen(sokrates) ----------------------------- kuolevainen(sokrates)