Τα «Συστήματα Αυτόματης Απόδειξης Θεωρημάτων-ΣΑΑΘ» (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.

Η παρούσα διπλωματική εργασία έχει ως σκοπό την παράθεση και ανάλυση των μεθόδων που έχουν παρουσιαστεί αυτή τη στιγμή στη διεθνή βιβλιογραφία και αφορούν τον έλεγχο και συγχρονισμό σε δίκτυο των Διασπαρμένων Συστημάτων Παραγωγής Ισχύος (Δ.Σ.Π.Ι.). Στο πρώτο κεφάλαιο γίνεται μια εισαγωγή στη Διασπαρμένη Παραγωγή (Δ.Π.) και στα Δ.Σ.Π.Ι. Στο δεύτερο κεφάλαιο παρουσιάζονται και αναλύονται τα κύρια χαρακτηριστικά των στρατηγικών ελέγχου που σχετίζονται με τον έλεγχο των Δ.Σ.Π.Ι. Στο τρίτο κεφάλαιο γίνεται παρουσίαση και ανάλυση των μεθόδων που χρησιμοποιούνται για το συγχρονισμό των Δ.Σ.Π.Ι. με το δίκτυο. Στο τέταρτο κεφάλαιο, όμοια με προηγούμενα, έγινε προσπάθεια για παρουσίαση των στρατηγικών ελέγχου των Δ.Σ.Π.Ι. σε περίπτωση που έχουμε εσφαλμένο δίκτυο. / The aim of this master thesis , is the presentation and analysis of the control strategies which are implemented on the distributed power generation systems(grid connection. Moreover, grid synchronization methods of DPGS are presented and evaluated. Control strategies when running on grid faults are also presented.

Until recently, organic particulate material was simply classified as either primary or secondary with the primary component being treated in models as nonvolatile and inert. This framework is used to simulate the organic aerosol formation, growth and composition in the eastern United States during the four seasons of the year. The model predictions are evaluated against daily average PM2.5 (particulate matter smaller than 2.5 μm) measurements taken throughout the eastern United States by the Interagency Monitoring of Protected Visual Environments (IMPROVE) and the Speciation Trends Network (STN) monitoring networks. The performance of the model in reproducing organic mass concentrations is average during all four seasons of the year. The agreement between the predicted and observed temporal profiles suggests a reasonable understanding and depiction in the model of the corresponding processes. However, this oversimplified view fails to explain the observed highly oxygenated nature of ambient organic aerosols (OA), the relatively small OA concentration gradients between large urban areas and their surroundings, and the concentrations of OA during periods of high photochemical activity. To address the above issues new primary and secondary organic aerosol modules have been added to a three dimensional chemical transport model (PMCAMx) based on recent smog chamber studies. The new modeling framework is based on the volatility basis-set approach: both primary and secondary organic components are assumed to be semivolatile and photochemically reactive and are distributed in logarithmically spaced volatility bins. The resulting PMCAMx-2008 was applied in Mexico City Metropolitan Area (MCMA) for approximately a week during April of 2003. The model predictions are compared with Aerosol Mass Spectrometry (AMS) observations and their Positive Matrix Factorization (PMF) analysis. The final goal of this work is to provide information to the policy makers regarding the response of fine PM to emission controls. PMCAMx is used to investigate changes in PM2.5 concentrations in response to 50% emissions changes of oxides of nitrogen and anthropogenic volatile organic compounds during July 2001 and January 2002 in the Eastern United States. / Τα ατμοσφαιρικά οργανικά σωματίδια συνηθίζεται να χωρίζονται σε δυο κατηγορίες: πρωτογενή και δευτερογενή. Τα πρώτα εκπέμπονται κατευθείαν στην ατμόσφαιρα ενώ τα δευτερογενή δημιουργούνται με την μεταφορά μάζας αερίων χαμηλής πτητικότητας, που προκύπτουν από την οξείδωση πρωτογενών οργανικών αερίων, στα ατμοσφαιρικά σωματίδια. Ένα τρισδιάστατο χημικό μοντέλο (PMCAMx), βασιζόμενο σε αυτό το διαχωρισμό, χρησιμοποιήθηκε για την προσομοίωση της σύνθεσης και της μάζας των οργανικών σωματιδίων της ατμόσφαιρας, στις ανατολικές Ηνωμένες Πολιτείες της Αμερικής κατά τη διάρκεια των τεσσάρων εποχών του χρόνου. Οι προβλέψεις του μοντέλου αξιολογήθηκαν έναντι μετρήσεων που πραγματοποιήθηκαν από τα δίκτυα παρακολούθησης IMPROVE και STN στις ανατολικές ΗΠΑ. Η απόδοση του μοντέλου, όσον αφορά τον προσδιορισμό της συγκέντρωσης των οργανικών ενώσεων κατά τη διάρκεια όλων των εποχών είναι ιδιαίτερα ικανοποιητική. Ωστόσο, αν και οι προβλέψεις του μοντέλου για τη συγκέντρωση της οργανικής μάζας είναι ενθαρρυντικές, δεν είναι ξεκάθαρο εάν το μοντέλο προβλέπει τις σωστές τιμές για τους σωστούς λόγους. Συγκεκριμένα το μοντέλο δεν μπορεί να εξηγήσει την πολύ οξυγονωμένη χημική μορφή των ατμοσφαιρικών οργανικών σωματιδίων όπως αυτή αποτυπώθηκε σε μετρήσεις πεδίου. Για να αντιμετωπιστούν τα ανωτέρω ζητήματα αναπτύσσουμε μια νέα μέθοδο προσομοίωσης των διεργασιών σχηματισμού και χημικής γήρανσης των πρωτογενών και δευτερογενών οργανικών σωματιδίων της ατμόσφαιρας, στο τρισδιάστατο χημικό μοντέλο PMCAMx βασιζόμενοι σε πρόσφατα πειραματικά δεδομένα. Στο νέο αυτό πλαίσιο μοντελοποίησης τόσο τα πρωτογενή, όσο και τα δευτερογενή οργανικά συστατικά θεωρούνται ότι είναι ημιπτητικά και φωτοχημικά ενεργά και κατανέμονται λογαριθμικά σε ομάδες ενώσεων διαφορετικής πτητικότητας. Το βελτιωμένο PMCAMx (PMCAMx-2008) έχει εφαρμοστεί στην ευρύτερη περιοχή της πόλης του Μεξικού για περίπου μια βδομάδα τον Απρίλιο του 2003. Οι προβλέψεις του μοντέλου συγκρίνονται με μετρήσεις φασματογράφου μάζας αεροζόλ και άλλες μετρήσεις που πραγματοποιήθηκαν κατά τη διάρκεια της καμπάνιας MCMA-2003. Τέλος το PMCAMx έχει χρησιμοποιηθεί για να μελετηθούν διεξοδικά οι αλλαγές στη συγκέντρωση των οργανικών σωματιδίων διαμέτρου έως 2.5 μm που προκύπτουν από αλλαγές των εκπομπών NOx και VOCs κατά τη διάρκεια των μηνών του Ιουλίου 2001 και του Ιανουαρίου 2002 στις ανατολικές Ηνωμένες Πολιτείες της Αμερικής.