Infinite-game semantics for logic programming languages

Abstract

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.

Η διατριβή επικεντρώνεται στη μελέτη της σημασιολογίας λογικών προγραμμάτων και την ανάπτυξη άπειρων παιγνίων πλήρους πληροφόρησης που αποδίδουν αυτή τη σημασιολογία. Αρχικώς, μελετάται ο προτασιακός λογικός προγραμματισμός. Στο άρθρο [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) λογικό προγραμματισμό.