Προηγούμενη Πάνω Επίπεδο Επόμενη Περιεχόμενα
Επόμενη: Ανάλυση Πάνω Επίπεδο: Λογική Πρώτης Τάξης Προηγούμενη: Κανονικές Μορφές

3.4 Το Θεώρημα του Herbrand

Σύμφωνα με τον ορισμό της ικανοποιησιμότητας (satisfiability), για να ελέγξουμε αν ένας τύπος δεν είναι ικανοποιήσιμος, πρέπει ν' αποδείξουμε το ψεύδος του ως προς όλες τις ερμηνείες και περιοχές (domains). Ωστόσο, μια τέτοια εργασία είναι αρκετά επίπονη και σε πολλές περιπτώσεις ακατόρθωτη. Για καλή μας τύχη, υπάρχει μια περιοχή που είναι τέτοια, ώστε αν κάποιος τύπος είναι ψευδής κάτω από οποιαδήποτε ερμηνεία στη συγκεκριμένη περιοχή, τότε δεν είναι ικανοποιήσιμος. Για ένα συγκεκριμένο τύπο tex2html_wrap_inline660, η περιοχή αυτή ονομάζεται το σύμπαν Herbrand του tex2html_wrap_inline660 (the Herbrand universe of tex2html_wrap_inline660). Η ονομασία οφείλεται στο Γάλλο λογικό Jacques Herbrand.

Περισσότερο συγκεκριμένα, αν L είναι μια γλώσσα πρώτης τάξης, το σύμπαν Herbrand UL για την L, είναι το σύνολο των βασικών όρων οι οποίοι μπορούν να σχηματιστούν από τις σταθερές και τα σύμβολα συναρτήσεων της L. Εάν η L δεν περιέχει σταθερές, της προσθέτουμε μια αυθαίρετη ώστε να μπορούμε να σχηματίζουμε βασικούς όρους. Η βάση Herbrand BL για την L, είναι το σύνολο όλων των βασικών ατόμων που μπορούν να σχηματιστούν από τα σύμβολα κατηγορημάτων της L καθώς και από τους όρους από το σύμπαν Herbrand UL. Θα ονομάζουμε μια ερμηνεία ενός τύπου στο σύμπαν Herbrand, ερμηνεία Herbrand (Herbrand interpretation).

Οι ερμηνείες Herbrand είναι ιδιαίτερα χρήσιμες στις περιπτώσεις των προτάσεων. Αποδεικνύεται ότι ένα σύνολο προτάσεων έχει ένα μοντέλο, αν και μόνον αν έχει ένα μοντέλο Herbrand. Τούτο σημαίνει ότι όταν ελέγχουμε το μη-ικανοποιήσιμο ενός συνόλου προτάσεων, μπορούμε να περιορίσουμε την εργασία μας σε μοντέλα Herbrand.



Εργαστήριο Γλωσσών Προγραμματισμού και Τεχνολογίας Λογισμικού
Mon Apr 5 16:25:43 EEST 1999