Prοοf procedure for extensional higher-order logic programming

Abstract

We consider an extensional higher-order logic programming language which possesses the minimum Herbrand model property. We propose an SLD-resolution proof procedure and we demonstrate that it is sound and complete with respect to this semantics. In this way, we extend the familiar proof theory of first-order logic programming to apply to the more general higher-order case. We then enhance our source language with constructive negation and extend the aforementioned proof procedure to support this new feature. We demonstrate the soundness of the resulting proof procedure and describe an actual implementation of a language that embodies the above ideas.

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