February 13, 2014
Τα δύο δημοφιλή παραδείγματα δηλωτικού προγραμματισμού, δηλαδή ο λογικός και ο συναρτησιακός προγραμματισμός διαφέρουν σημαντικά: ο λογικός προγραμματισμός είναι παραδοσιακά πρώτης τάξης ενώ ο συναρτησιακός προγραμματισμός προωθεί την χρήση συναρτήσεων υψηλής τάξης.
Θεωρούμε μια εκτατική γλώσσα λογικού προγραμματισμού υψηλής τάξης όπου κατηγορήματα μπορούν να περαστούν σαν παράμετροι. Κάθε λογικό πρόγραμμα υψηλής τάξης έχει ένα ελάχιστο μοντέλου Herbrand. Σε αυτή την σημασιολογία τα κατηγορήματα αναπαριστούνται από σύνολα και δύο κατηγορήματα είναι ίσα αν και μόνο αν είναι ίσα ως σύνολα.
Προτείνουμε μια αποδεικτική διαδικασία για τη γλώσσα αυτή και αποδεικνύουμε ότι είναι ορθή και πλήρης σε σχέση με τη σημασιολογία ελάχιστου μοντέλου. Κατά συνέπεια, επεκτείνουμε την κλασική αποδεικτική διαδικασία του λογικού προγραμματισμού πρώτης τάξης ώστε να εφαρμόζεται στην πολύ πιο γενική περίπτωση του λογικού προγραμματισμού υψηλής τάξης. Κατόπιν εμπλουτίζουμε τη γλώσσα υψηλής τάξης ώστε να υποστηρίζει κατασκευαστική άρνηση και επεκτείνουμε την αποδεικτική διαδικασία ώστε να χειρίζεται τη νέα αυτή προσθήκη.