ΠΑΝΕΠΙΣΤΗΜΙΟ ΚΥΠΡΟΥ ΤΜΗΜΑ ΠΛΗΡΟΦΟΡΙΚΗΣ

 

ΕΠΛ 412: Λογική στην Πληροφορική

 

Χειμερινό Εξάμηνο 2017-2018

 

 

Διδάσκουσα:                                     Άννα Φιλίππου

Γραφείο:                                           FST-01 105

Τηλέφωνο:                                        22-892699

E-mail:                                               annap@cs.ucy.ac.cy

Ιστοσελίδα του μαθήματος:            http://www.cs.ucy.ac.cy/~annap/EPL412/index.html

 

 

ΠΕΡΙΓΡΑΦΗ

Η Μαθηματική Λογική διαδραματίζει αναμφισβήτητα ένα σημαντικό ρόλο στην Πληροφορική αφού στηρίζει και θεμελιώνει πολλαπλές περιοχές της Πληροφορικής όπως την Αρχιτεκτονική (λογικές πύλες), Τεχνολογία Λογισμικού (προδιαγραφή και επαλήθευση), Γλώσσες Προγραμματισμού (σημασιολογία, συστήματα τύπων, λογικός προγραμματισμός), Βάσεις Δεδομένων (relational algebra, SQL), Τεχνητή Νοημοσύνη (theorem proving), Θεωρία Αλγορίθμων (πολυπλοκότητα και εκφραστικότητα) και Θεωρία Υπολογισμού (υπολογισιμότητα).

Τα μάθημα θα παρουσιάσει βασικές έννοιες της Λογικής που βρίσκουν εφαρμογές στην Πληροφορική εστιάζοντας στον Προτασιακό Λογισμό, στον Πρωτοβάθμιο Κατηγορηματικό Λογισμό και σε χρονικούς λογισμούς με έμφαση στην εφαρμογή των σχετικών εννοιών στην Πληροφορική. 

 

ΔΙΑΛΕΞΕΙΣ ΦΡΟΝΤΙΣΤΗΡΙΑ ΚΑΙ ΕΡΓΑΣΤΗΡΙΑ

Διαλέξεις:                   Δευτέρα και Πέμπτη, 10:30 – 12:00

Φροντιστήριο:           Τετάρτη, 12:00 – 13:00

 

Η διδασκαλία του μαθήματος αποτελείται από διαλέξεις και φροντιστήρια. Η παρακολούθηση των διαλέξεων από τους φοιτητές είναι υποχρεωτική. Οι φοιτητές παρακαλούνται όπως προσέρχονται στην αίθουσα των διαλέξεων έγκαιρα. Φροντιστήρια θα γίνονται κάθε βδομάδα εκτός και αν ανακοινωθεί κάτι διαφορετικό από τη διδάσκουσα.

 

ΠΡΟΑΠΑΙΤΟΥΜΕΝΑ

Τo μάθημα ΕΠΛ 111 (Διακριτές Δομές στην Πληροφορική και Υπολογισμό) είναι προαπαιτούμενο για την παρακολούθηση του ΕΠΛ 412.

 

ΠΕΡΙΕΧΟΜΕΝΟ

Προτασιακός Λογισμός: σύνταξη και σημασιολογία, κανονικές μορφές, τυπικά συστήματα και οι έννοιες της ορθότητας, της συνέπειας και της πληρότητας, εφαρμογές. Πρωτοβάθμιος Κατηγορηματικός Λογισμός: σύνταξη και σημασιολογία, κανονικές μορφές, αποδεικτική θεωρία, ορθότητα και πληρότητα, εφαρμογές. Αρχή της Επίλυσης στον Προτασιακό και στον Κατηγορηματικό Λογισμό, Λογικός Προγραμματισμός. Γραμμικός και Διακλαδωμένος Χρονικός Λογισμός (LTL, CTL): σύνταξη και σημασιολογία, αλγόριθμοι μοντελοελέγχου. Τριάδες Hoare και συστήματα απόδειξης προγραμμάτων.

 

ΣΤΟΧΟΙ

Το μάθημα αυτό θα παρουσιάσει μιας εισαγωγή στη  Μαθηματική Λογική η οποία θα καλύψει θέματα όπως τη σύνταξη, τη σημασιολογία και την αποδεικτική θεωρία του Προτασιακού και του Πρωτοβάθμιου Κατηγορηματικού Λογισμού καθώς επίσης και τις εφαρμογές τους στην Πληροφορική. Επίσης, μέσω του μαθήματος, οι φοιτητές θα εξοικειωθούν με έννοιες του γραμμικού και διακλαδωμένου χρονικού λογισμού και σχετικές εφαρμογές στην περιοχή της τυπικής ανάλυσης συστημάτων. Βασικός στόχος του μαθήματος είναι η προετοιμασία των φοιτητών για να χρησιμοποιήσουν τη Μαθηματική Λογική ως εργαλείο στην Πληροφορική. Επιπλέον οι στόχοι του μαθήματος περιλαμβάνουν τους εξής:

-   Ανάπτυξη λογικής και μαθηματικής ωριμότητας

-   Εξοικείωση με τον συμπερασματικό συλλογισμό

-   Αναγνώριση της Λογικής ως έναν από τους θεμέλιους λίθους της Πληροφορικής

-   Εφαρμογές της Λογικής στην ανάλυση της ορθότητας προγραμμάτων και συστημάτων.

 

ΒΙΒΛΙΟΓΡΑΦΙΑ

Εκτός από τις σημειώσεις των διαλέξεων, για επιπλέον πληροφορίες συνιστούνται τα  πιο κάτω βιβλία.

 

1.      M. Huth and A. Ryan. Logic in Computer Science: Modeling and Reasoning about Concurrent Systems. Cambridge University Press, 2000.

2.      M. Ben-Ari. Mathematical Logic for Computer Science. Springer-Verlag, 2nd edition, 2003.

 

ΑΞΙΟΛΟΓΗΣΗ

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

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

Η αναλογία ως προς τον τελικό βαθμό είναι η εξής:

Τελική εξέταση                                               50%

Ενδιάμεση εξέταση                                         30%

Ασκήσεις                                                        20%