Η διατριβή επικεντρώνεται στη μελέτη της σημασιολογίας λογικών προγραμμάτων και
την ανάπτυξη άπειρων παιγνίων πλήρους πληροφόρησης που αποδίδουν αυτή τη
σημασιολογία. Αρχικώς, μελετάται ο προτασιακός λογικός προγραμματισμός. Στο
άρθρο [M.H. van Emden, Quantitative deduction and its fixpoint theory, Journal
of Logic Programming 3(1)(1986) 37-53] περιγράφεται ένα παίγνιο μεταξύ δύο
παικτών. Σε αυτό, δεδομένου ενός προτασιακού λογικού προγράμματος χωρίς άρνηση
και ενός ατόμου (ground atom) που ανήκει σε αυτό, ο Παίκτης Ι, προσπαθεί να
αποδείξει ότι ο ατομικός τύπος είναι αληθής (έχει δηλαδή το ρόλο του
Believer), ενώ ο Παίκτης ΙΙ ότι δεν είναι (έχει δηλαδή το ρόλο του Doubter).
Έτσι ο στόχος (goal), επιτυγχάνει ως αποτέλεσμα μιας ερώτησης (query) στο
πρόγραμμα, αν ο Παίκτης Ι έχει νικηφόρα στρατηγική. Στα πλαίσια της
διατριβής, το παίγνιο επεκτείνεται έτσι ώστε να αποδίδει τη σημασιολογία και
των προγραμμάτων με άρνηση. Όταν κατά τη διάρκεια του παιχνιδιού εμφανίζεται
αρνητικά προσημασμένο άτομο, τότε οι δύο παίκτες αλλάζουν τους μεταξύ τους
ρόλους. Ο Believer γίνεται Doubter και το αντίστροφο. Στην περίπτωση άπειρων
εναλλαγών ρόλων το παιχνίδι θεωρείται ισόπαλο. Αποδεικνύεται ότι το παίγνιο
είναι αποφασισμένο (determined). Στην περίπτωση του παιχνιδιού με τρία δυνατά
αποτελέσματα, η ερμηνεία του προγράμματος, η οποία λαμβάνεται χρησιμοποιώντας
το παιχνίδι, αποτελεί μοντέλο του και αποδεικνύεται ισοδύναμη με την καλώς
θεμελιωμένη σημασιολογία (well-founded semantics) του λογικού προγράμματος. Για
την απόδειξη αυτή ορίζεται και χρησιμοποιείται ένα νέο παίγνιο με άπειρα δυνατά
αποτελέσματα. Η τιμή του παιχνιδιού εξαρτάται από το πλήθος των εναλλαγών ρόλων
(role switches) που λαμβάνουν χώρα κατά τη διάρκειά του. Η ερμηνεία που
παίρνουμε χρησιμοποιώντας το παίγνιο αυτό, αποτελεί μοντέλο του λογικού
προγράμματος και αποδεικνύεται ισοδύναμη με την απειρότιμη σημασιολογία
ελαχίστου μοντέλου, όπως αυτή ορίζεται στο [P. Rondogiannis, W.W.Wadge, Minimum
model semantics for logic programs with negation-as-failure, ACM Transactions
on Computational Logic 6(2)(2005) 441-467]. Η μελέτη επεκτείνεται στον
νοηματικό (intensional) λογικό προγραμματισμό όπως παρουσιαζεται στο [M.A.
Orgun, W.W.Wadge, Towards a unified theory of intensional logic programming,
13(4):413-440, 1992] και αποτελεί γενίκευση, μεταξύ άλλων, του χρονικού
(temporal) και τροπικού (modal) λογικού προγραμματισμού. Στα πλαίσια της
διατριβής αναπτύσσεται ένα νέο παίγνιο π
λήρους πληροφόρησης. Και για αυτό, αποδεικνύεται ότι είναι αποφασισμένο
(determined) και ότι το αποτέλεσμά του συμπίπτει με τη σημασιολογία ελαχίστου
μοντέλου του άρθρου των M.A. Orgun, W.W. Wadge. Στη συνέχεια το παίγνιο
επεκτείνεται έτσι ώστε να υποστηρίζει εναλλαγή ρόλων μεταξύ των παικτών και να
έχει τρία δυνατά αποτελέσματα (νίκη για τον Παίκτη Ι ή τον Παίκτη ΙΙ ή
ισοπαλία). Η ερμηνεία την οποία παίρνουμε χρησιμοποιώντας το παιχνίδι,
αποτελεί ελαχιστικό μοντέλο του προγράμματος και αποδίδει τη σημασιολογία
νοηματικών λογικών προγραμμάτων με άρνηση και γενικότερα των νοηματικών
λογικών προγραμμάτων με οποιoδήποτε μη μονοτονικό τελεστή στο σώμα των
κανόνων. Η παιγνιοθεωρητική αυτή προσέγγιση αποτελεί και το πρώτο σημασιολογικό
πλαίσιο για τον μη μονοτονικό νοηματικό (intensional) λογικό προγραμματισμό.
(EL)
This thesis focuses on the study of the semantics of logic programs and the
development of infinite games of perfect information between two players that
capture this semantics. Initially, we study propositional logic programming. In
[M.H. van Emden, Quantitative deduction and its fixpoint theory, Journal of
Logic Programming 3 (1) (1986) 37-53] a game between two players is described.
In this, given a propositional logic program without negation and a ground
atom that belongs to the program, Player I, tries to prove that the atomic
formula is true (he therefore has the role of the Believer), and the other
that it is not (he therefore has the role of the Doubter). So the goal,
succeeds as a result of a query to the program, if Player I has a winning
strategy. In this thesis, the game is extended to capture the semantics of
programs with negation. When during the game a negated atom appears, the two
players switch roles. The Believer becomes Doubter and vice versa. In case of
infinite role-switches we have a tie. It is proved that the game is
determined. In the case of the game with three possible results, the
game-theoretic semantics is equivalent to the well-founded semantics of the
logic program. In order to prove that, we use a new refined game that has
infinite possible outcomes. The value of that game depends on the number of
role switches that take place during it. The refined game is also proved to be
determined and its interpretation is a model of the program and equivalent to
the infinite valued minimum model semantics as defined in
[P.Rondogiannis,W.W.Wadge, Minimum model semantics for logic programs with
negation-as-failure, ACM Transactions on Computational Logic 6(2)(2005)
441-467]. Our study then extends to the Intensional logic programming as
presented in [M.A.Orgun, W.W.Wadge, Towards a unified theory of intensional
logic programming, 13(4):413-440,1992] and is a generalization of temporal and
modal logic programming. In order to capture the semantics of such languages
we develop a new two-valued game of perfect information. This is also proved to
be determined. The game interpretation is a model of the program and
equivalent to the minimum model semantics defined by Orgun and Wadge.
Subsequently, the game is extended so that it can allow role-switches between
the two players, and that it has three possible outcomes (win for either Player
I or Player II, or the two players tie). In that way, the game interpretation
is proved to also capture the semantics of logic programs with negation or
more generally any non-monotonic operator. This game semantics is the first
semantic framework for non-monotonic intensional logic programming.
(EN)
/aggregator-openarchives/portal/institutions/uoa
