Πρόταση Horn

Μια πρόταση Horn είναι μια λογική διάζευξη λογικών, όπου το πολύ ένα από τα λογικά είναι θετικό και όλα τα άλλα είναι αρνητικά. Πήρε το όνομά της από τον Alfred Horn, ο οποίος τις περιέγραψε σε ένα άρθρο του το 1951.

Μια πρόταση Horn με ακριβώς ένα θετικό λεκτικό είναι μια οριστική πρόταση- μια οριστική πρόταση χωρίς αρνητικά λεκτικά ονομάζεται μερικές φορές "γεγονός"- και μια πρόταση Horn χωρίς θετικό λεκτικό ονομάζεται μερικές φορές πρόταση στόχου. Αυτά τα τρία είδη ρητρών Horn απεικονίζονται στο ακόλουθο προτασιακό παράδειγμα:

οριστική πρόταση: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t ∨ u {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u} $\neg p\lor \neg q\vee \cdots \vee \neg t\vee u$

fact: u {\displaystyle u} $u$

ρήτρα στόχου: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t} $\neg p\lor \neg q\vee \cdots \vee \neg t$

Στη μη προτασιακή περίπτωση, όλες οι μεταβλητές σε μια πρόταση προσδιορίζονται σιωπηρά καθολικά με πεδίο εφαρμογής ολόκληρη την πρόταση. Έτσι, για παράδειγμα:

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

σημαίνει:

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

το οποίο είναι λογικά ισοδύναμο με:

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

Οι ρήτρες Horn παίζουν βασικό ρόλο στην εποικοδομητική λογική και την υπολογιστική λογική. Είναι σημαντικές στην αυτοματοποιημένη απόδειξη θεωρημάτων με επίλυση πρώτης τάξης, επειδή η επίλυση δύο ρητρών Horn είναι η ίδια μια ρήτρα Horn και η επίλυση μιας ρήτρας στόχου και μιας οριστικής ρήτρας είναι μια ρήτρα στόχου. Αυτές οι ιδιότητες των ρητρών Horn μπορούν να οδηγήσουν σε μεγαλύτερη αποτελεσματικότητα στην απόδειξη ενός θεωρήματος (που αναπαρίσταται ως η άρνηση μιας ρήτρας στόχου).

Οι ρήτρες Horn αποτελούν επίσης τη βάση του λογικού προγραμματισμού, όπου είναι σύνηθες να γράφονται οριστικές ρήτρες με τη μορφή συνεπαγωγής:

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

Στην πραγματικότητα, η επίλυση μιας πρότασης στόχου με μια οριστική πρόταση για την παραγωγή μιας νέας πρότασης στόχου είναι η βάση του κανόνα συμπερασμού επίλυσης SLD, που χρησιμοποιείται για την υλοποίηση του λογικού προγραμματισμού και της γλώσσας προγραμματισμού Prolog.

Στον λογικό προγραμματισμό μια οριστική πρόταση συμπεριφέρεται ως διαδικασία μείωσης στόχων. Για παράδειγμα, η ρήτρα Horn που γράφτηκε παραπάνω συμπεριφέρεται ως διαδικασία:

για να δείξει u {\displaystyle u} $u$ , να δείξει p {\displaystyle p} $p$ και να δείξει q {\displaystyle q} και ⋯ {\displaystyle \cdots } $\cdots$ και show t {\displaystyle t} $t$

Για να τονιστεί αυτή η αντίστροφη χρήση της ρήτρας, συχνά γράφεται με την αντίστροφη μορφή:

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

Στην Prolog αυτό γράφεται ως εξής:

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

Ο συμβολισμός της Prolog είναι στην πραγματικότητα διφορούμενος και ο όρος "goal clause" χρησιμοποιείται μερικές φορές επίσης διφορούμενα. Οι μεταβλητές σε μια ρήτρα στόχου μπορούν να διαβαστούν ως καθολικά ή υπαρξιακά ποσοτικοποιημένες, και η εξαγωγή του "false" μπορεί να ερμηνευτεί είτε ως εξαγωγή μιας αντίφασης είτε ως εξαγωγή μιας επιτυχούς λύσης του προβλήματος που πρέπει να επιλυθεί.

Οι Van Emden και Kowalski (1976) διερεύνησαν τις μοντελοθεωρητικές ιδιότητες των ρητρών Horn στο πλαίσιο του λογικού προγραμματισμού, δείχνοντας ότι κάθε σύνολο οριστικών ρητρών D έχει ένα μοναδικό ελάχιστο μοντέλο M. Ένας ατομικός τύπος A υπονοείται λογικά από το D αν και μόνο αν ο A είναι αληθής στο M. Προκύπτει ότι ένα πρόβλημα P που αναπαρίσταται από μια υπαρξιακά ποσοτικοποιημένη ένωση θετικών γραμματικών υπονοείται λογικά από το D αν και μόνο αν ο P είναι αληθής στο M. Η σημασιολογία του ελάχιστου μοντέλου των ρητρών Horn είναι η βάση για τη σημασιολογία του σταθερού μοντέλου των λογικών προγραμμάτων.

Οι προτασιακές ρήτρες Horn παρουσιάζουν επίσης ενδιαφέρον στην υπολογιστική πολυπλοκότητα, όπου το πρόβλημα της εύρεσης αναθέσεων τιμών αλήθειας για να γίνει αληθής μια ένωση προτασιακών ρητρών Horn είναι ένα P-πλήρες πρόβλημα (στην πραγματικότητα επιλύσιμο σε γραμμικό χρόνο), το οποίο μερικές φορές ονομάζεται HORNSAT. (Ωστόσο, το πρόβλημα ικανοποίησης Boole χωρίς περιορισμούς είναι ένα NP-πλήρες πρόβλημα). Η ικανοποιησιμότητα των ρητρών Horn πρώτης τάξης είναι αναποφάσιστη.

Ερωτήσεις και απαντήσεις

Q: Τι είναι η ρήτρα Horn;

A: Μια πρόταση Horn είναι μια λογική διάζευξη λογικών στοιχείων, όπου το πολύ ένα από τα λογικά στοιχεία είναι θετικό και όλα τα άλλα είναι αρνητικά.

Ερ: Ποιος τα περιέγραψε πρώτος;

A: Ο Alfred Horn τις περιέγραψε για πρώτη φορά σε ένα άρθρο του το 1951.

Ερ: Τι είναι μια οριστική πρόταση;

Α: Μια πρόταση Horn με ακριβώς ένα θετικό λεκτικό ονομάζεται οριστική πρόταση.

Ε: Τι είναι το γεγονός;

Α: Μια οριστική πρόταση χωρίς αρνητικά κυριολεκτικά αναφέρεται μερικές φορές ως "γεγονός".

Ε: Τι είναι η πρόταση στόχου;

Α: Μια πρόταση Horn χωρίς ένα θετικό κυριολεκτικό ονομάζεται μερικές φορές πρόταση στόχου.

Ερ: Πώς λειτουργούν οι μεταβλητές σε μη προτασιακές περιπτώσεις;

Α: Στη μη προτασιακή περίπτωση, όλες οι μεταβλητές σε μια πρόταση είναι σιωπηρά καθολικά ποσοτικοποιημένες με πεδίο εφαρμογής ολόκληρη την πρόταση. Αυτό σημαίνει ότι εφαρμόζονται σε κάθε τμήμα της πρότασης.

Ερ: Τι ρόλο παίζουν οι ρήτρες Horn στην εποικοδομητική λογική και στην υπολογιστική λογική; Α: Οι ρήτρες Horn παίζουν σημαντικό ρόλο στην αυτοματοποιημένη απόδειξη θεωρημάτων με επίλυση πρώτης τάξης, επειδή η επίλυση δύο ρητρών Horn ή μεταξύ μιας ρήτρας στόχου και μιας οριστικής ρήτρας μπορεί να χρησιμοποιηθεί για τη δημιουργία μεγαλύτερης αποτελεσματικότητας κατά την απόδειξη κάποιου πράγματος που αναπαρίσταται ως η άρνηση της ρήτρας στόχου του. Χρησιμοποιούνται επίσης ως βάση για γλώσσες λογικού προγραμματισμού όπως η Prolog, όπου συμπεριφέρονται σαν διαδικασίες αναγωγής στόχων.