δείτε την πρωτότυπη σελίδα τεκμηρίου στον ιστότοπο του αποθετηρίου του φορέα για περισσότερες πληροφορίες και για να δείτε όλα τα ψηφιακά αρχεία του τεκμηρίου*
Proof Procedures for Extensional Higher-order Logic Programming
Θεωρούμε μια εκτατική γλώσσα λογικού προγραμματισμού υψηλής τάξης η οποία
διαθέτει την ιδιότητα του ελάχιστου μοντέλου Herbrand. Προτείνουμε μια
αποδεικτική διαδικασία για τη γλώσσα αυτή και αποδεικνύουμε ότι είναι ορθή και
πλήρης σε σχέση με τη σημασιολογία ελάχιστου μοντέλου. Κατά συνέπεια,
επεκτείνουμε την κλασική αποδεικτική διαδικασία του λογικού προγραμματισμού
πρώτης τάξης ώστε να εφαρμόζεται στην πολύ πιο γενική περίπτωση του λογικού
προγραμματισμού υψηλής τάξης. Κατόπιν εμπλουτίζουμε τη γλώσσα υψηλής τάξης ώστε
να υποστηρίζει κατασκευαστική άρνηση και επεκτείνουμε την αποδεικτική
διαδικασία ώστε να χειρίζεται τη νέα αυτή προσθήκη. Αποδεικνύουμε την ορθότητα
της νέας διαδικασίας και περιγράφουμε μια υλοποίηση η οποία ενσωματώνει τις
παραπάνω ιδέες.
(EL)
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.
(EN)
*Η εύρυθμη και αδιάλειπτη λειτουργία των διαδικτυακών διευθύνσεων των συλλογών (ψηφιακό αρχείο, καρτέλα τεκμηρίου στο αποθετήριο) είναι αποκλειστική ευθύνη των αντίστοιχων Φορέων περιεχομένου.
Βοηθείστε μας να κάνουμε καλύτερο το OpenArchives.gr.
Εθνικό και Καποδιστριακό Πανεπιστήμιο Αθηνών
