Εφαρμογές της λογικής στην πληροφορική

Abstract

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

The book includes an introduction to the basic areas of application of logic in computer science. The indicative topics covered in the book include an introduction to the subject of logic in general (categorical logic), as well as the range of its applications in computer science (programming semantics, automatic proof, system modeling, algorithm verification). Emphasis is placed on formal methods, which are a typical example of the application of logic in programming and software technology in general. Topics covered include issues related to classical and non-classical logics, lambda calculus, type theory, models, program and specification correctness, functional programming, theorem proving, logical programming, proofs as programs, semantics of programming languages and system specifications, equational logic, algebraic specifications of systems. Also, techniques for specifying and verifying the properties of programs and systems. The algebraic specification language CafeOBJ is used as an example of a logic-based language (combination of equational logic systems) and is used in software modeling applications. Other logic-based languages and their applications are also presented briefly, such as functional programming languages (Lisp). It is worth noting that this course is considered particularly important internationally in the study of computer science and applied mathematics in computer science.