“Εφαρμογές της Λογικής στην Πληροφορική”

Το προτεινόμενο βιβλίο θα περιλαμβάνει μια εισαγωγή στους βασικούς τομείς εφαρμογών της λογικής στην πληροφορική. Η ενδεικτική θεματολογία του βιβλίου περιλαμβάνει μια εισαγωγή στο αντικείμενο της λογικής γενικά (κατηγορηματικός λογισμός), αλλά και στο εύρος των εφαρμογών της στην πληροφορική (σημασιολογία προγραμματισμού, αυτόματη απόδειξη, μοντελοποίηση συστημάτων, επαλήθευση αλγορίθμων). Έμφαση θα δοθεί στις τυπικές μεθόδους λογισμικού (formal methods) που αποτελούν χαρακτηριστικό παράδειγμα εφαρμογής της λογικής στον προγραμματισμό και εν γένει την τεχνολογία λογισμικού.

Ανάμεσα στα θέματα που προτείνεται να παρουσιαστούν περιλαμβάνονται ζητήματα που αφορούν τις κλασσικές και μη κλασσικές λογικές, λ-λογισμός, θεωρία τύπων (type theory), μοντέλα, ορθότητα προγραμμάτων και προδιαγραφών, συναρτησιακός προγραμματισμός, αυτόματη απόδειξη θεωρημάτων (theorem proving), λογικός προγραμματισμός, οι αποδείξεις ως προγράμματα (proofs as programs), σημασιολογία γλωσσών προγραμματισμού και προδιαγραφών συστημάτων, εξισωτική λογική (equational logic), αλγεβρικές προδιαγραφές (algebraic specifications) συστημάτων. Τεχνικές προδιαγραφών και επαλήθευσης ιδιοτήτων προγραμμάτων και συστημάτων.

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

Αξίζει να αναφερθεί ότι το μάθημα αυτό θεωρείται ιδιαίτερα σημαντικό διεθνώς στις σπουδές της πληροφορικής (computer science) και των εφαρμοσμένων μαθηματικών στην πληροφορική.