mpla.math.uoa.gr
Font size: Αα Αα Αα hide gadgets
You are here: Courses » 2012-2013 » fall semester » Λ15. Proof theory (2012-2013, fall semester) Anonymously browsing from 54.196.127.107 at 11:07:11, 23-11-2017. login

Proof theory: 2012-2013, fall semester

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. Proof theory.

Taught by: Georgios Koletsos & Yiorgos Stavrinos
Start date: Oct. 17, 2012
End date:
Website: http://www.math.ntua.gr/logic/proof-theory/proof-theory.html

Teaching hours

  • every Wednesday, 09:00-11:00, 102, ece, NTUA (new buildings)
    except:
    • Wednesday, 24 Oct 2012
    • Wednesday, 07 Nov 2012
    • Wednesday, 30 Jan 2013
  • every Thursday, 11:45-13:45, 101, ece, NTUA (new buildings)
    except:
    • Thursday, 25 Oct 2012
    • Thursday, 15 Nov 2012
    • Thursday, 06 Dec 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

Wednesday, 17 Oct 2012 Koletsos

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

Wednesday, 31 Oct 2012 Stavrinos

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

Thursday, 01 Nov 2012 Stavrinos

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

Thursday, 08 Nov 2012 Stavrinos

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

Wednesday, 21 Nov 2012 Stavrinos

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

Thursday, 22 Nov 2012 Stavrinos

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

Wednesday, 28 Nov 2012 Stavrinos

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

Thursday, 29 Nov 2012 Stavrinos

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

Wednesday, 05 Dec 2012 Stavrinos

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

Wednesday, 12 Dec 2012 Stavrinos

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

Thursday, 13 Dec 2012 Stavrinos

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

Wednesday, 19 Dec 2012 Stavrinos

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

Thursday, 20 Dec 2012 Stavrinos

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

Wednesday, 09 Jan 2013 Stavrinos

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

Thursday, 10 Jan 2013 Stavrinos

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

Wednesday, 16 Jan 2013 Stavrinos

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

Thursday, 17 Jan 2013 Stavrinos

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

Wednesday, 23 Jan 2013 Stavrinos

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

Thursday, 24 Jan 2013 Stavrinos

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

Thursday, 31 Jan 2013 Stavrinos

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

Wednesday, 06 Feb 2013 Stavrinos

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

Thursday, 07 Feb 2013 Stavrinos

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

Wednesday, 13 Feb 2013 Stavrinos

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

Comments

You must be logged in to comment.

Reporter

Page updates

No recent updates.

Feeds RSS and Atom feeds

posts
all posts RSS
news RSS
announcements RSS
website news RSS
events
all events RSS
defenses RSS
exams RSS
seminars RSS
graduations RSS
Web standards: XHTML1.0, CSS3.
© 1996 – 2017 MPLA: Graduate program in Logic, Algorithms and Computation.
Contact the webmaster.