Μονάδα:
Διαπανεπιστημιακό ΠΜΣ Λογική και Θεωρία Αλγορίθμων και ΥπολογισμούΒιβλιοθήκη Σχολής Θετικών Επιστημών
Ημερομηνία κατάθεσης:
2015-04-06
Συγγραφέας:
Κοκκίνης Ιωάννης
Στοιχεία επιβλεπόντων καθηγητών:
Ευστάθιος Ζάχος Ομότ. Καθηγητής
Πρωτότυπος Τίτλος:
Annotated sequent systems for linear temporal logic
Γλώσσες εργασίας:
Αγγλικά
Μεταφρασμένος τίτλος:
Συστήματα ακολουθητών με υποσημειώσεις για τη γραμμική χρονική λογική
Περίληψη:
Χρησιμοποιώντας ακολουθητές με υποσημειώσεις, μπορούμε να
σχεδιάσουμε κατανοητά και απλά συστήματα απαγωγής για
χρονικές λογικές. Όμως, οι ακολουθητές με υποσημειώσεις,
παρά τη σαφήνεια που προσφέρουν, καθιστούν την απόδειξη
συντακτικών ιδιοτήτων πάρα πολύ δύσκολη.
Μέχρι πρόσφατα, δεν ήταν καν σαφές πως να αποδείξουμε (με
καθαρά συντακτικές μεθόδους) ότι
ένα σύστημα ακολουθητών με υποσημειώσεις
αποδέχεται την εξασθένηση. Σε αυτή
την εργασία παρουσιάζουμε ένα σύστημα ακολουθητών με υποσημειώσεις
για τη γραμμική χρονική λογική, το οποίο δε βασίζεται ούτε σε
κάποιον κανόνα με άπειρες υποθέσεις ούτε στον κανόνα της τομής.
Παρουσιάζουμε αποδείξεις ορθότητας και
πληρότητας, καθώς και μία καθαρά
συντακτική απόδειξη για την αποδοχή της εξασθένησης
στο εν λόγω σύστημα.
Λέξεις-κλειδιά:
Ακολουθητές με υποσημειώσεις, Γραμμική χρονική λογική, Εξασθένηση, Θεωρία αποδείξεων, Λογισμός ακολουθητών
Αρ. σελίδων ευρετηρίου:
0
Αρ. βιβλιογραφικών αναφορών:
9
