Σημασιολογία στην Επιστήμη των Υπολογιστών¶
Επίσημο περίγραμμα μαθήματος του ΤΜΗΥΠ (Πανεπιστήμιο Πατρών), όπως δημοσιεύεται στη σελίδα του μαθήματος και στο συνημμένο αρχείο «Περίγραμμα Μαθήματος». Το κείμενο παρατίθεται αυτούσιο, χωρίς τα πρότυπα οδηγιών του εντύπου.
Στόχοι¶
- Γνώση και εφαρμογή του συντακτικού των τύπων Α’ τάξης, και των θεμελιωδών ιδιοτήτων των τιμών αλήθειας τους. Κατανόηση εξειδικευμένων ερωτημάτων και προβλημάτων, σχετικά με τις τυπικές αποδείξεις στη Λογική Α’ τάξης. Γνώση των κυριώτερων αποδεικτικών συστημάτων Α’ τάξης, και των εξειδικευμένων τεχνικών για την ανάλυσή τους. Γνώση εξειδικευμένων υπολογιστικών μεθόδων για εύρεση τυπικών αποδείξεων. Δεξιότητα στην απάντηση σύνθετων ερωτημάτων σχετικά με τη λογική ισοδυναμία Α’ τάξης, καθώς και στον σχεδιασμό και την ανάλυση εξειδικευμένων υπολογιστικών μεθόδων.
Περιεχόμενο (ύλη)¶
Εξειδικευμένες έννοιες και τεχνικές της Λογικής Α’ τάξης, με έμφαση στην μαθηματικά ακριβή περιγραφή των εννοιών και των εφαρμογών τους. Εξετάζεται ο ρόλος της θεωρίας στον σχεδιασμό αλγορίθμων για προβλήματα λογικής ισοδυναμίας, και στην επαλήθευση της ορθότητάς τους. Καλύπτονται: Συντακτικό και σημασιολογία τύπων Α’ τάξης. Έννοιες συνεπαγωγής και λογικής ισοδύναμίας, αντίστοιχες έννοιες τυπικής απόδειξης. Βασικά καθώς και εξειδικευμένα αποδεικτικά συστήματα. Ιδιότητες ορθότητας και πληρότητας αποδεικτικών συστημάτων, εξοικείωση με τις κυριώτερες τεχνικές για τη μελέτη τους. Βασικές καθώς και εξειδικευμένες μέθοδοι αναζήτησης τυπικών αποδείξεων, εφαρμογές τους σε προβλήματα σχετικά με συνεπαγωγή και λογική ισοδυναμία τύπων Α’ τάξης.
Αξιολόγηση¶
Γραπτές εργασίες (Ελληνική γλώσσα). Περιλαμβάνουν Ερωτήσεις Σύντομης Απάντησης και Επίλυση Προβλημάτων. Αξιολογούνται: η πληρότητα της γνώσης της θεωρίας, η ακρίβεια και ορθότητα των λύσεων. Οι απαντήσεις των θεμάτων παρουσιάζονται αναλυτικά στο φροντιστήριο του μαθήματος.
Βιβλιογραφία¶
M. Fitting, “First-Order Logic and Automated Theorem Proving M. Huth, M.Ryan, “Logic in Computer Science”
-Συναφή επιστημονικά περιοδικά: