Η παρούσα εργασία έχει ως θέμα τη μαθηματική απόδειξη και την διαδικασία επίλυσης προβλήματος. Στόχος της είναι αρχικά, να παρουσιάσει το θεωρητικό υπόβαθρο που διέπει αυτά τα δύο θέματα και να κάνει μια σύγκριση ώστε να αναδειχθούν οι διαφορές τους και οι ομοιότητες τους. Στην συνέχεια, γίνεται μια σύντομη παρουσίαση των Αναλυτικών Προγραμμάτων και των διδακτικών εγχειριδίων των Μαθηματικών του Λυκείου για το χρονικό διάστημα από τα τέλη της δεκαετίας του 1980 έως σήμερα έχοντας ως κύριο άξονα, την απόδειξη και την επίλυση προβλήματος. Κατόπιν, με την βοήθεια μιας δραστηριότητας κατάλληλα διαμορφωμένης εξετάζετε ο ρόλος των παραπάνω στους μαθητές και τέλος, γίνετε μια σύντομη ανάλυση της Γραμμικής και Δομικής μορφής της απόδειξης, όπως αυτή είχε προταθεί από τον Uri Leron και μια συγκριτική παρουσίαση των αποδείξεων κάποιων θεωρημάτων του σχολικού βιβλίου της Γεωμετρίας της Α΄ Λυκείου (Αργυρόπουλος Η.) και με τις δύο μορφές. / The objective of this Master Thesis is the presentation of the Mathematical Proof and Problem Solving. Its aim is initially to present the theoretical background behind these two issues and a comparison between the Mathematical Proof and Problem Solving with respect to their similarities and differences takes place. Then a brief presentation of the curriculum programs as well as the school books of mathematics is given. This presentation is about the time period from the late decade of 1980 up to date, mostly concerning the Mathematical Proof and Problem Solving. Moreover, using a suitably formulated activity, the role of the above over the students is studied. Finally, a concise analysis of Linear and Structural style of proof as it suggested by Uri Leron is given. The thesis is completed with the presentation of three theorems along with their proofs (Linear style) as they are stated in the section of "Inequality Relationships" of Geometry school book of A Lyceum class (Αργυρόπουλος Η. 2008), while for each proof its Structural style is also given.

Τα «Συστήματα Αυτόματης Απόδειξης Θεωρημάτων-ΣΑΑΘ» (Automatic Theorem Proving Systems-ATP Systems) είναι συστήματα βασισμένα στη λογική πρώτης τάξεως, τα οποία μπορούν από ένα σύνολο λογικών προτάσεων να συνάγουν την αλήθεια μιας δεδομένης λογικής πρότασης με αυτόματο τρόπο. Η διαδικασία της απόδειξης στα περισσότερα ΣΑΑΘ στηρίζεται στην αρχή της επίλυσης, τον ισχυρότερο κανόνα λογικής εξαγωγής συμπερασμάτων, και την αντίφαση της επίλυσης, μια διαδικασία που εξασφαλίζει την ορθότητα των συμπερασμάτων. Ο ACT-P είναι ένα ΣΑΑΘ που στηρίζεται στην αρχή της επίλυσης και την αντίφαση της επίλυσης, γραμμένο στο εργαλείο GCLISP Developer 5.0 της Gold-Hill, και διαθέτει μια βιβλιοθήκη γνωστών στρατηγικών ελέγχου της διαδικασίας απόδειξης, προσφέροντας τη δυνατότητα στον χρήστη να ορίσει κάθε φορά ένα (κατάλληλο) συνδυασμό στρατηγικών. Στην εργασία αυτή έγινε κατ’ αρχήν μεταφορά του ACT-P σε LispWorks, ένα δυναμικότερο εργαλείο ανάπτυξης εφαρμογών σε Lisp. Επιπλέον, ο χρήστης μέσω του νέου παραθυρικού περιβάλλοντος μπορεί να βλέπει δυο διαφορετικές λύσεις του ίδιου προβλήματος, τη συνοπτική και αναλυτική λύση. Στη συνέχεια, έγινε έλεγχος της καλής λειτουργίας του ACT-P και των στρατηγικών του μέσω δοκιμών με προβλήματα που προέρχονται από την TPTP (Thousands of Problems for Theorem Provers), μια γνωστή βιβλιοθήκη προβλημάτων για ΣΣΑΘ συστήματα στο Διαδίκτυο, και έγιναν οι απαραίτητες διορθώσεις έτσι ώστε να επιλύει προβλήματα από διάφορες κατηγορίες προβλημάτων της βιβλιοθήκης TPTP. Τέλος, έγινε μια μελέτη χρήσης διαφόρων συνδυασμών στρατηγικών ελέγχου για διάφορα προβλήματα της TPTP και εξήχθησαν χρήσιμα συμπεράσματα για την καταλληλότητά τους και την αποδοτικότητά τους σε σχέση με το είδος των προβλημάτων. / Automatic Theorem Proving Systems (ATP Systems) are based on First Order Logic (FOL) and are able to automatically prove the truth of logical sentence. The proof procedure in most ATP Systems uses the resolution principle which is the strongest existing inference rule, and the resolution refutation process which ensure soundeness of the conclusion. The ACT-P is an ATP System which uses the resolution principle and the resolution refutation and it is written in GCLISP Developer 5.0 of Gold-Hill. ACT-P has a library of strategies to control the proof process, and gives users the ability to assign to specify a suitable combination of strategies. In this dissertation a new window based interface is developed for ACTP in Lispworks, which is a powerful tool for developing Lisp applications. The interface gives to the user a more thorough view of the solving process. Moreover, the user can see two different solutions of the problem, the brief and the analytic one. In addition, the functionality and the strategies of ACTP were tested on problems from the TPTP (Thousands of Problems for Theorem Provers) which is a known library of problems for ATP Systems on the web. ACTP has been improved so as to solve problems from various categories of the TPTP library. Finally, different strategy combinations for solving problems from various categories of TPTP library were studied, leading to useful conclusions about the suitability and the performance of the different combinations depending on the problems.

- / -

To αντικείμενο μελέτης της εργασίας αυτής είναι κατά μείζονα λόγο το θεώρημα Tarski-Seidenberg. Στο πρώτο κεφάλαιο μελετάμε το κίνητρο που ώθησε τον Tarski σε αυτή την έρευνα, εξιστορούμε την πορεία της ιδέας του από την ανακάλυψη μέχρι τη δημοσίευση και έπειτα προσπαθούμε να σκιαγραφήσουμε ευκρινώς τη συνολική επίδραση του θεωρήματος στα μαθηματικά και όχι μόνο. Για την ακρίβεια, αναφερόμαστε στην πληρότητα της Ευκλείδειας γεωμετρίας ως συνέπεια του θεωρήματος, στη συμβολή του θεωρήματος στην ανάπτυξη της ημιαλγεβρικής γεωμετρίας. Στο δεύτερο κεφάλαιο αποδικνύεται το εν λόγω θεώρημα, δηλαδή ότι η πρωτοβάθμια θεωρία των πραγματικώς κλειστών σωμάτων είναι πλήρης, με χρήση των θεωρημάτων Sturm και Sylvester. Στο τρίτο κεφάλαιο παρουσιάζεται μία διδακτική έρευνα με φοιτητές του τμήματος με σκοπό τη διάγνωση πιθανών γνωστικών κενών των φοιτητών σε θέματα της θεωρίας πολυωνύμων με πραγματικούς συντελεστές. / To study object of this work is a fortiori the Tarski-Seidenberg theorem. In the first chapter we study Tarski's motivation in this research, we recount the progress of the idea from ​​the discovery until the publication, and then we try to outline clearly the overall effect of the theorem in mathematics and beyond. In fact, we refer to the completeness of Euclidean geometry as a consequence of the theorem, in its contribution to the development of semialgebraic geometry. In the second chapter we prove the Tarski-Seidenberg theorem, namely that the first order theory of real closed fields is actually complete, using the Sturm and Sylvester theorems. In the third chapter we present a teaching research on students of the Department in purpose to diagnose potential knowledge gaps of the students concerning the theory of polynomials with real coefficients.