MSc thesis of Ιωάννης Κοκκίνης
Συστήματα Ακολουθητών με Υποσημειώσεις για τη Γραμμική Χρονική Λογική
Supervisor: Ευστάθιος Ζάχος
Χρησιμοποιώντας ακολουθητές με υποσημειώσεις, μπορούμε να σχεδιάσουμε κατανοητά και απλά συστήματα απαγωγής για χρονικές λογικές. ́Ομως, οι ακολουθητές με υποσημειώσεις, παρά τη σαφήνεια που προσφέρουν, καθιστούν την απόδειξη συντακτικών ιδιοτήτων πάρα πολύ δύσκολη. Μέχρι πρόσφατα, δεν ήταν καν σαφές πως να αποδείξουμε (με καθαρά συντακτικές μεθόδους) ότι ένα σύστημα ακολουθητών με υποσημειώσεις αποδέχεται την εξασθένηση. Σε αυτή την εργασία παρουσιάζουμε ένα σύστημα ακολουθητών με υποσημειώσεις για τη γραμμική χρονική λογική, το οποίο δεν βασίζεται ούτε σε κάποιον κανόνα με άπειρες υποθέσεις ούτε στον κανόνα της τομής. Παρουσιάζουμε αποδείξεις ορθότητας και πληρότητας, καθώς και μία καθαρά συντακτική απόδειξη για την εξασθένηση στο εν λόγω σύστημα.
Defended: 06 Απριλίου 2015.