mpla.math.uoa.gr
Font size: Αα Αα Αα hide gadgets
You are here: Courses » 2012-2013 » χειμερινό εξάμηνο » Λ15. Θεωρία αποδείξεων (2012-2013, χειμερινό εξάμηνο)

Θεωρία αποδείξεων: 2012-2013, χειμερινό εξάμηνο

This is a course that has been given 7 times. For information about this course in general (not just for this specific semester), visit its page: Λ15. Θεωρία αποδείξεων.

Taught by: Γεώργιος Κολέτσος & Γιώργος Σταυρινός
Start date: 17 Οκτωβρίου 2012
End date:
Website: http://www.math.ntua.gr/logic/proof-theory/proof-theory.html

Teaching hours

  • every Τετάρτη, 09:00-11:00, 102, ΣΗΜΜΥ, ΕΜΠ (νέα κτ.)
    except:
    • Τετάρτη, 24 Οκτ 2012
    • Τετάρτη, 07 Νοέ 2012
    • Τετάρτη, 30 Ιαν 2013
  • every Πέμπτη, 11:45-13:45, 101, ΣΗΜΜΥ, ΕΜΠ (νέα κτ.)
    except:
    • Πέμπτη, 25 Οκτ 2012
    • Πέμπτη, 15 Νοέ 2012
    • Πέμπτη, 06 Δεκ 2012

Course information

Το μάθημα δίνεται στα πλαίσια του Διαπανεπιστημιακού Μεταπτυχιακού Προγράμματος στη Λογική και Θεωρία Αλγορίθμων και Υπολογισμού (ΜΠΛΑ) στο οποίο συμμετέχει η Σχολή Hλεκτρολόγων Mηχανικών και Mηχανικών Yπολογιστών (ΣHMMY) και ο Tομέας Mαθηματικών της Σχολής Eφαρμοσμένων Mαθηματικών και Φυσικών Eπιστημών (ΣEMΦE) του EMΠ. Επίσης προσφέρεται ως μεταπτυχιακό μάθημα στα πλαίσια του μεταπτυχιακού προγράμματος της ΣΗΜΜΥ (Λογική και Πληροφορική Ι) καθώς και του αντίστοιχου προγράμματος της ΣΕΜΦΕ.
Πρόκειται για εισαγωγικό μάθημα στη Θεωρία Αποδείξεων με έμφαση στη Δομική Θεωρία Aποδείξεων (δομή των μαθηματικών αποδείξεων, απαλοιφή των τομών και κανονικοποίηση) καθώς και τη σύνδεση που έχει με την πληροφορική (λ-λογισμός με τύπους) μέσω της ισοδυναμίας Curry-Howard. Παρουσιάζει μεγάλο ενδιαφέρον για τους Μαθηματικούς και τους θεωρητικούς Πληροφορικούς καθώς η μελέτη της απόδειξης ενός μαθηματικού τύπου μπορεί να θεωρηθεί ως μελέτη του προγράμματος υπολογισμού ενός τύπου δεδομένων. Ενδιαφέρει όμως και τους ασχολούμενους με τα θεμέλια των μαθηματικών και την Επιστημολογία αφού το αρχικό έναυσμα της δημιουργίας της θεωρίας αποδείξεων ήταν η προσπάθεια του Hilbert να θεμελιώσει αυστηρά τα Μαθηματικά προσπαθώντας με περατοκρατικές μεθόδους να αποδείξει τη συνέπειά τους. Θα επιδιωχθεί, με εμβόλιμες σεμιναριακές ώρες, η ανάπτυξη και άλλων ζητημάτων σχετιζομένων με τη Θεωρία Αποδείξεων.

Μικρό ιστορικό: Η ανακάλυψη, πριν από έναν αιώνα, των αντινομιών στη θεωρία συνόλων και η συνακόλουθη αμφιβολία και αβεβαιότητα σε σχέση με τη χρήση αφαιρετικών μεθόδων στα Μαθηματικά οδήγησε τον D. Hilbert στη διατύπωση του περίφημου προγράμματός του: να περισώσει τις μεθόδους που χρησιμοποιούνται στα κλασικά μαθηματικά αποδεικνύοντας τη συνέπεια των μαθηματικών θεωριών με μεθόδους που έχουν στοιχειώδη συνδυαστικό (περατοκρατικό) χαρακτήρα και ως εκ τούτου διαφανείς και ασφαλείς. Παρ' όλο που ο K. Goedel απέδειξε με το θεώρημα της μη πληρότητας ότι το πρόγραμμα του Hilbert δεν μπορεί να πραγματοποιηθεί σύμφωνα με τον αρχικό του σχεδιασμό η ιδέα του Hilbert παρέμεινε η κινούσα δύναμη για την ανάπτυξη της θεωρίας αποδείξεων για πολλά χρόνια. Και επειδή αυτό το πρόγραμμα απαιτούσε την αξιωματικοποίηση-τυποποίηση των διαφόρων μαθηματικών θεωριών αυτό οδήγησε στη μελέτη per se των τυποποιημένων μαθηματικών αποδείξεων. Σήμερα υπάρχουν πολύ περισσότεροι λόγοι για τη μελέτη των αποδείξεων από αυτούς που επιβάλλει το πρόγραμμα Hilbert. Για παράδειγμα, η Aυτόματη Aπόδειξη Θεωρημάτων, μέρος της μελέτης στην Τεχνητή Νοημοσύνη, οδηγεί στη μελέτη των αποδείξεων ως συνδυαστικές δομές. Στο Λογικό Προγραμματισμό οι τυπικές απαγωγές χρησιμοποιούνται στους υπολογισμούς κλπ.

Περιεχόμενα

Αποδεικτικά συστήματα: φυσική απαγωγή, συστήματα Hilbert, συστήματα ακολουθητών του Gentzen.
Η έννοια της τομής, θεωρήματα απαλοιφής των τομών και εφαρμογές.
Κανονικοποίηση και αριθμητικά φράγματα στην απαλοιφή των τομών, δομή των αποδείξεων χωρίς τομές.
Ισοδυναμία Curry-Howard-de Bruijn.
Kανονικοποίηση στη φυσική απαγωγή.
Εισαγωγή στη Γραμμική Λογική.
Αριθμητική του Peano και ανάλυση των αποδείξεων με διατακτικούς αριθμούς.

Βιβλιογραφία, Αναφορές

Basic Proof theory, A.S. Troelstra & H. Schwichtenberg, 2nd ed., Cambridge Univ. Press, 2000.
Structural Proof Theory, Sara Negri & Jan von Plato, Cambridge Univ. Press, 2001.
Proofs and Types, J.-Y. Girard, Cambridge Univ. Press, 1989.
An Introduction to Proof Theory, Samuel R. Buss., in Handbook of Proof Theory, Elsevier, 1998.
Proof Theory and Logical Complexity, J.-Y. Girard, Bibliopolis, 1987.
Λογική και Απόδειξη, Branislav Boricic, Εκδ. Ζήτη, 1995.
The collected papers of G. Gentzen, M.E. Szabo, North Holland, 1969.
Proof Theory and Automated Deduction, Jean Goubault-Larrecq & Ian Mackie, Kluwer Ac. Publ., 1997.

Enrolled students

Exams

Diary

Τετάρτη, 17 Οκτ 2012 Κολέτσος

Εισαγωγη, Το προγραμμα του Hilbert

Τετάρτη, 31 Οκτ 2012 Σταυρινός

Συντομη εισαγωγη στο λ-λογισμο, β-αναγωγη

Πέμπτη, 01 Νοέ 2012 Σταυρινός

Θεωρημα Church-Rosser, Θεωρηματα κανονικοποιησης
Γλωσσα πρωτοβαθμιου κατηγορηματικου λογισμου

Πέμπτη, 08 Νοέ 2012 Σταυρινός

Η ιντουισιονιστικη ερμηνεια Brouwer-Heyting-Kolmogorov

Τετάρτη, 21 Νοέ 2012 Σταυρινός

Εισαγωγή στη Φυσική Απαγωγή (σύστημα ->Nm)
Ισοδυναμία Curry-Howard-de Bruijn

Πέμπτη, 22 Νοέ 2012 Σταυρινός

Εισαγωγή στα συστήματα ακολουθητών (->G1), κανόνας τομής

Τετάρτη, 28 Νοέ 2012 Σταυρινός

Κλασική εγκυρότητα ακολουθητών
Αξιωματικό σύστημα Hilbert (σύστημα ->Hm)
Κανόνες φυσικής απαγωγής (συστήματα Nm, Ni, Nc)

Πέμπτη, 29 Νοέ 2012 Σταυρινός

Η αρνηση στην minimal, ιντουισιονιστικη και κλασικη λογικη
Αρνητικοι τυποι, Αρνητικη μεταφραση Gödel-Gentzen

Τετάρτη, 05 Δεκ 2012 Σταυρινός

Εμφυτευση της κλασικης στην ιντουισιονιστικη λογικη
(μεταφρασεις Gödel-Gentzen/Kolmogorov/Kuroda, υποθεσεις ευσταθειας)

Τετάρτη, 12 Δεκ 2012 Σταυρινός

Αξιωματικο συστημα Hilbert H[mic]
Ισοδυναμια φυσικης απαγωγης και αξιωματικου συστηματος (Θεωρημα απαγωγης)
Λογισμος ακολουθητων G1[mic]

Πέμπτη, 13 Δεκ 2012 Σταυρινός

Προσθετικοι/πολλαπλασιαστικοι κανονες
Λογισμος ακολουθητων G2
Ιδιοτητα υποτυπου

Τετάρτη, 19 Δεκ 2012 Σταυρινός

Θεωρημα απαλοιφης της τομης
Ισοδυναμια λογισμου ακολουθητων G[12][mi] και φυσ. απαγωγης N[mi]
Ισοδυναμια λογισμου ακολουθητων G[12]c και φυσ. απαγωγης Nc

Πέμπτη, 20 Δεκ 2012 Σταυρινός

Λογισμος ακολουθητων G3
Λημμα αντιστρεψιμοτητας των κανονων
Κλασικος λογισμος ακολουθητων Gentzen-Schütte GS

Τετάρτη, 09 Ιαν 2013 Σταυρινός

Αποδειξη του Θεωρηματος απαλοιφης της τομης (1ο μερος)

Πέμπτη, 10 Ιαν 2013 Σταυρινός

Αποδειξη του Θεωρηματος απαλοιφης της τομης (2ο μερος)
Πολυτομη & απαλοιφη της τομης κατα Gentzen

Τετάρτη, 16 Ιαν 2013 Σταυρινός

Εφαρμογες Θεωρηματος απαλοιφης της τομης: ιδιοτητα υποτυπου, συνεπεια, τυποι Harrop, (γενικευμενη) ιδιοτητα διαζευξης και υπαρξης, Θεωρημα Herbrand

Πέμπτη, 17 Ιαν 2013 Σταυρινός

Αποκρισιμοτητα προτασιακης ιντουισιονιστικης λογικης (G3ip)
Αποδειξεις μη-αποδειξιμοτητας

Τετάρτη, 23 Ιαν 2013 Σταυρινός

Θεωρημα παρεμβολης [Craig], Θεωρημα ορισιμοτητας [Beth], Θεωρημα κοινης συνεπειας [Robinson]
Κανονικοποιηση στην ιντουϊσιονιστικη φυσικη απαγωγη Ni

Πέμπτη, 24 Ιαν 2013 Σταυρινός

Μετατροπες συστολης (τομες μηκους 1), μεταθεσης (τομες μηκους > 1), απλοποιησης
Θεωρημα ασθενους κανονικοποιησης

Πέμπτη, 31 Ιαν 2013 Σταυρινός

Δομη κανονικων απαγωγων, μονοπατια (tracks), Θεωρημα υποτυπου

Τετάρτη, 06 Φεβ 2013 Σταυρινός

Εισαγωγη στη Γραμμικη Λογικη

Πέμπτη, 07 Φεβ 2013 Σταυρινός

Διαισθητικη ερμηνεια της Γραμμικης Λογικης

Τετάρτη, 13 Φεβ 2013 Σταυρινός

Εμφυτευση της ιντουϊσιονιστικης λογικης (G1i) στην Γραμμικη λογικη (ILL και CLL)

Comments

You must be logged in to comment.

Reporter

Web standards: XHTML1.0, CSS3.
© 1996 – 2018 MPLA: Graduate program in Logic, Algorithms and Computation.
Contact the webmaster.