1. Home page
  2. Search

Proof Procedures for Extensional Higher-order Logic Programming

This item is provided by the institution :
/aggregator-openarchives/portal/institutions/uoa   

Repository :
Pergamos Digital Library   

see the original item page
in the repository's web site and access all digital files if the item*



Proof Procedures for Extensional Higher-order Logic Programming
Χαραλαμπίδης Άγγελος (EL)
born_digital_thesis
Διδακτορική Διατριβή (EL)
Doctoral Dissertation (EN)
2014
Θεωρούμε μια εκτατική γλώσσα λογικού προγραμματισμού υψηλής τάξης η οποία διαθέτει την ιδιότητα του ελάχιστου μοντέλου 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)
English
Σχολή Θετικών Επιστημών » Τμήμα Πληροφορικής & Τηλεπικοινωνιών » Τομέας Θεωρητικής Πληροφορικής
Βιβλιοθήκη και Κέντρο Πληροφόρησης » Βιβλιοθήκη Σχολής Θετικών Επιστημών
https://creativecommons.org/licenses/by-nc/4.0/
University of Athens
Pergamos Digital Library
Doctoral Dissertation



*Institutions are responsible for keeping their URLs functional (digital file, item page in repository site)