Αποδεικτικές διαδικασίες για τον εκτατικό λογικό προγραμματισμό υψηλής τάξης
Περίληψη
Θεωρούμε μια εκτατική γλώσσα λογικού προγραμματισμού υψηλής τάξης η οποία διαθέτει την ιδιότητα του ελάχιστου μοντέλου Herbrand. Προτείνουμε μια αποδεικτική διαδικασία για τη γλώσσα αυτή και αποδεικνύουμε ότι είναι ορθή και πλήρης σε σχέση με τη σημασιολογία ελάχιστου μοντέλου. Κατά συνέπεια, επεκτείνουμε την κλασική αποδεικτική διαδικασία του λογικού προγραμματισμού πρώτης τάξης ώστε να εφαρμόζεται στην πολύ πιο γενική περίπτωση του λογικού προγραμματισμού υψηλής τάξης. Κατόπιν εμπλουτίζουμε τη γλώσσα υψηλής τάξης ώστε να υποστηρίζει κατασκευαστική άρνηση και επεκτείνουμε την αποδεικτική διαδικασία ώστε να χειρίζεται τη νέα αυτή προσθήκη. Αποδεικνύουμε την ορθότητα της νέας διαδικασίας και περιγράφουμε μια υλοποίηση η οποία ενσωματώνει τις παραπάνω ιδέες.
Περίληψη σε άλλη γλώσσα
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.
![]() | |
![]() | Κατεβάστε τη διατριβή σε μορφή PDF (1.06 MB)
(Η υπηρεσία είναι διαθέσιμη μετά από δωρεάν εγγραφή)
|
Όλα τα τεκμήρια στο ΕΑΔΔ προστατεύονται από πνευματικά δικαιώματα.
|
Στατιστικά χρήσης
![](/eadd/image/spinner.gif)
ΠΡΟΒΟΛΕΣ
Αφορά στις μοναδικές επισκέψεις της διδακτορικής διατριβής για την χρονική περίοδο 07/2018 - 07/2023.
Πηγή: Google Analytics.
Πηγή: Google Analytics.
![](/eadd/image/spinner.gif)
ΞΕΦΥΛΛΙΣΜΑΤΑ
Αφορά στο άνοιγμα του online αναγνώστη για την χρονική περίοδο 07/2018 - 07/2023.
Πηγή: Google Analytics.
Πηγή: Google Analytics.
![](/eadd/image/spinner.gif)
ΜΕΤΑΦΟΡΤΩΣΕΙΣ
Αφορά στο σύνολο των μεταφορτώσων του αρχείου της διδακτορικής διατριβής.
Πηγή: Εθνικό Αρχείο Διδακτορικών Διατριβών.
Πηγή: Εθνικό Αρχείο Διδακτορικών Διατριβών.
![](/eadd/image/spinner.gif)
ΧΡΗΣΤΕΣ
Αφορά στους συνδεδεμένους στο σύστημα χρήστες οι οποίοι έχουν αλληλεπιδράσει με τη διδακτορική διατριβή. Ως επί το πλείστον, αφορά τις μεταφορτώσεις.
Πηγή: Εθνικό Αρχείο Διδακτορικών Διατριβών.
Πηγή: Εθνικό Αρχείο Διδακτορικών Διατριβών.