Τμήμα Πληροφορικής & Τηλεπικοινωνιών
Πληροφορική

2017-06-29

2017

Dona Ergys

Πάνος Ροντογιάννης, Καθηγητής, Πληροφορικής και Τηλεπικοινωνιών, ΕΚΠΑ
Άγγελος Χαραλαμπίδης, Ερευνητής, ΕΚΕΦΕ «Δημόκριτος»

Implementation of Constructive Negation in Extensional Higher-Order Logic Programming

Αγγλικά

Υλοποίηση Κατασκευαστικής Άρνησης σε Εκτατικό Λογικό Προγραμματισμό Υψηλής Τάξης

Η κατασκευαστική άρνηση είναι μια μέθοδος άρνησης στον λογικό προγραμματισμό, η οποία επιτρέπει το χειρισμό μη-συγκεκριμενοποιημένων αρνητικών προτάσεων. Τα συστήματα λογικού προγραμματισμού τα οποία είναι επαυξημένα με κατασκευαστική άρνηση μπορούν δυνητικά να παράγουν όχι μόνο ισότητες (αναθέσεις ή ενοποιήσεις μεταβλητών), αλλά και ανισότητες, οι οποίες, γενικά μιλώντας, περιορίζουν τις μεταβλητές έτσι ώστε να είναι διαφορετικές από κάποια τιμή.

Ο εκτατικός λογικός προγραμματισμός υψηλής τάξης είναι ένα παράδειγμα λογικού προγραμματισμού που επεκτείνει τον κλασικό (πρώτης τάξης) λογικό προγραμματισμό εισάγοντας όρους υψηλής τάξης, ενώ παράλληλα διατηρεί τις καλά ορισμένες ιδιότητες του προηγούμενου. Αυτοί οι υψηλής τάξης όροι αναπαριστούν σύνολα, τα οποία περιλαμβάνουν στοιχεία για τα οποία οι προηγούμενοι είναι αληθείς.

Μια γλώσσα λογικού προγραμματισμού υψηλής τάξης με όνομα HOPES έχει προταθεί πρόσφατα. Η γλώσσα αυτή έχει επαυξηθεί με κατασκευαστική άρνηση για να διαμορφωθεί η γλώσσα "HOPES with constructive negation".

Ενώ η σημασιολογία της HOPES είναι καλά ορισμένη, η υλοποίηση ενός συστήματος λογικού προγραμματισμού (διερμηνευτή) για την τελευταία αποδείχθηκε δυσκολότερη υπόθεση απ'ότι αναμενόταν. Ο λόγος είναι πως η διαδικασία απόδειξης της HOPES δεν υποδεικνύει κανέναν συγκεκριμένο τρόπο επιλογής του επόμενου στόχου για ικανοποίηση. Δείχνουμε πως, ενώ ορισμός της γλώσσας εγγυάται την ύπαρξη μονοπατιών στο δέντρο απόδειξης, τα οποία οδηγούν σε σωστές λύσεις, εάν μια απλοϊκή πολιτική επιλογής (π.χ. η επιλογή πάντα του αριστερότερου υποστόχου, όπως κάνει η PROLOG) έχει υιοθετηθεί, τότε πρέπει να παρθούν επιπλέον μέτρα έτσι ώστε η υλοποίηση να αποφύγει μονοπάτια τα οποία δεν θα οδηγήσουν ποτέ σε σωστές λύσεις.

Η συνεισφορά αυτής της πτυχιακής έγκειται στον επαναορισμό κάποιων εκ των κανόνων της διαδικασίας απόδειξης της HOPES. Δείχνουμε ότι η νέα διαδικασία απόδειξης επιτρέπει την υλοποίηση ενός διερμηνευτή για την HOPES, o οποίος ακολουθεί τον κανόνα της PROLOG για επιλογή του πάντα αριστερότερου υποστόχου και παράλληλα συμπεριφέρεται σωστά (δίνει σωστές λύσεις μόνο) για κάθε επερώτηση.

Πληροφορική

λογική, προγραμματισμός, άρνηση, υψηλή τάξη, εκτατικός

Ναι

2

Ναι

8

48

https://pergamos.lib.uoa.gr/uoa/dl/object/1692144/file.pdf

https://pergamos.lib.uoa.gr/uoa/dl/object/1692144