The expressive power of second-order datalog under the well-founded semantics of negation

Πτυχιακή Εργασία uoadl:3243392 56 Αναγνώσεις

Μονάδα:
Τμήμα Πληροφορικής & Τηλεπικοινωνιών
Πληροφορική
Ημερομηνία κατάθεσης:
2022-11-04
Έτος εκπόνησης:
2022
Συγγραφέας:
ΑΣΛΑΝΗΣ-ΠΕΤΡΟΥ ΡΩΜΑΝΟΣ
Στοιχεία επιβλεπόντων καθηγητών:
Ροντογιάννης Παναγιώτης, Καθηγητής, Τμήμα Πληροφορικής και Τηλεπικοινωνιών, Εθνικό και Καποδιστριακό Πανεπιστήμιο Αθηνών.
Άγγελος Χαραλαμπίδης, Επίκουρος Καθηγητής, Τμήμα Πληροφορικής και Τηλεματικής, Χαροκόπειο Πανεπιστήμιο
Πρωτότυπος Τίτλος:
The expressive power of second-order datalog under the well-founded semantics of negation
Γλώσσες εργασίας:
Αγγλικά
Ελληνικά
Μεταφρασμένος τίτλος:
Η εκφραστική ισχύς της Datalog δεύτερης τάξης υπό την well-founded σημασιολογία της άρνησης
Περίληψη:
Πρόσφατα δείχτηκε ότι η datalog k-τάξης χωρίς άρνηση εκφράζει την κλάση πολυπλοκότη-
τας (k − 1)-EXPTIME σε διατεταγμένες βάσεις δεδομένων και ειδικότερα η datalog δεύτερης τάξης εκφράζει την κλάση EXPTIME. Σε αυτή την πτυχιακή ερευνούμε την εκφραστική ισχύ της datalog 2ης-τάξης κάτω απο την well-founded σημασιολογία της άρνησης. Πιο συγκεκριμένα, παρουσιάζουμε έναν αναδρομικό αλγόριθμο που δέχεται ως είσοδο έναν λογικό τύπο φ της υπαρξιακής λογικής δεύτερης τάξης SO(∃) και κατασκευάζει ένα πρόγραμμα datalog 2ης-τάξης Pφ . Επιπλέον υπάρχει μια ισοδυναμία, όσον αφορά την ικανοποιησιμότητα, μεταξύ των πεπερασμένων μοντέλων του φ και του well-founded μοντέλου του Pφ , που υπονοεί μια σωστή συμπεριφορά του προγράμματος Pφ. Με άλλα λόγια η ικανοποιησιμότητα ενός δοσμένου λογικού τύπου της SO(∃) από μια συγκεκριμένη δομή (ερμηνεία), μεταφέρεται στην ικανοποιησιμότητα ενός "τελικού" κανόνα του προγράμματος Pφ απο το well-founded μοντέλο. Ως αποτέλεσμα, με βάση το γνωστό
θεώρημα του Fagin και τον παραπάνω μετασχηματισμό συμπαιρένουμε ότι η datalog
2ης-τάξης με well-founded σημασιολογία εκφράζει την κλάση NP. Τέλος το αποτέλεσμα
αυτό δεν είναι αυστηρό, δηλαδή η datalog 2ης-τάξης μπορεί να είναι ακόμα πιο δυνατή,
και δεν βασίζεται σε κάποια υπόθεση διάταξης της εισόδου, δεδομένου ότι η SO(∃) είναι
αρκετά δυνατή για να επιλέξει μη ντετερμινιστικά μια τέτοια διάταξη.
Κύρια θεματική κατηγορία:
Τεχνολογία – Πληροφορική
Λέξεις-κλειδιά:
Λογικός προγραμματισμός υψηλής τάξης, datalog δεύτερης τάξης, περιγραφική θεωρία πολυπλοκότητας
Ευρετήριο:
Ναι
Αρ. σελίδων ευρετηρίου:
1
Εικονογραφημένη:
Όχι
Αρ. βιβλιογραφικών αναφορών:
19
Αριθμός σελίδων:
22