ABSTRACT.  Datalog+/?  is a family of languages for knowledge representation and reasoning. These languages extend Datalog with features such as existential quantifiers, equalities, and the falsum in rule heads, and, at the same time, applies restrictions to achieve decidability and tractability. After a general overview of the Datalog+/?  family, this talk will focus on more recent issues. Among other things, I will report on the combination of the two main decidability paradigms guardedness and stickiness, yielding the Tame Fragment, and on incorporating non-monotonic negation and disjunction into Datalog+/–: . I will also report about a special version of Datalog+/?  suitable for reasoning with reverse-engineered UML class diagrams, and about the TriQ language that expresses SPARQL with entailment regimes.

ABSTRACT. Logic programs with ordered disjunction (LPODs) \cite{Brewka02} generalize normal logic programs by combining alternative and ranked options in the heads of rules. It has been showed that LPODs are useful in a number of areas including Game Theory, policy languages, planning and argumentations. In this paper, we extend propositional LPODs to the first-order case, where a classical second-order formula is defined to represent the stable model semantics of the underlying first-order LPODs. We then develop a progression semantics that is equivalent to the stable model semantics but naturally reflects the reasoning procedure of LPODs. We show that under finite structures, every LPOD can be translated into a first-order sentence, which provides a basis for computing stable models of LPODs. We further study the complexity and expressiveness of LPODs and prove that almost positive LPODs precisely capture normal logic programs, which indicates that ordered disjunction itself and constraints are sufficient to represent negation as failure.

ABSTRACT. Extensional higher-order logic programming has been recently proposed as an interesting extension of classical logic programming. An important characteristic of the new paradigm is that it preserves all the well-known properties of traditional logic programming. In this paper we enhance extensional higher-order logic programming with constructive negation. We argue that the main ideas underlying constructive negation are quite close to the existing proof procedure for extensional higher-order logic programming and for this reason the two notions amalgamate quite conveniently. We demonstrate the soundness of the resulting proof procedure and describe an actual implementation of a language that embodies the above ideas. In this way we obtain the first (to our knowledge) higher-order logic programming language supporting constructive negation and offering a new style of programming that genuinely extends that of traditional logic programming.

ABSTRACT. In the past, there have several attempts to explain logic programming under the well-founded semantics as a logic of inductive definitions. A weakness in all is the absence of an obvious connection between how we understand various types of informal inductive definitions in mathematical texts and the complex mathematics of the well-founded semantics. In this paper, we close this gap and show in a more definitive way that indeed, the well-founded semantics is a formalization of the principle of inductive definition.

ABSTRACT. Input languages of answer set solvers are based on the mathematically simple concept of a stable model. But many useful constructs available in these languages, including local variables, conditional literals, and aggregates, cannot be easily explained in terms of stable models in the sense of the original definition of this concept and its straightforward generalizations. Manuals written by designers of answer set solvers usually explain such constructs using examples and informal comments that appeal to the user's intuition, without references to any precise semantics. We propose to approach the problem of defining the semantics of gringo programs by translating them into the language of infinitary propositional formulas. This semantics allows us to study equivalent transformations of gringo programs using natural deduction in infinitary propositional logic, so that the properties of these programs can be more precisely characterized. In this way, we aim to create a foundation on which important issues such as the correctness of gringo programs and optimization methods may be more formally studied.

ABSTRACT. We introduce dynamic causal calculus, a nonmonotonic formalism that can be viewed as a direct logical counterpart of the action description language C+ from \cite{GLMT01}. We formulate a nonmonotonic semantics of the associated causal language, and compare this semantics with the indirect, two-stage semantics for C+, given in \cite{GLMT01}. It will be shown, in particular, that the suggested semantics allows us to alleviate syntactic distinctions between propositional atoms, maintained by C+, as well as type restrictions imposed on its causal laws. We will describe also a logical formalism of dynamic causal inference that constitutes a complete description of the logic that is adequate for this dynamic calculus.

ABSTRACT. Causal models defined in terms structural equations have proved to be quite a powerful way of representing knowledge regarding causality. However, a number of authors have designed examples where it seems that the Halpern-Pearl (HP) definition of causality gives intuitively unreasonable answers. As has been pointed out by many authors, what gets counted as a cause is quite dependent on the choice of variables in the model. Here it is shown that in all the counterexamples suggested, there are two possible stories consistent with the counterexample, where intuitions regarding causality are quite different. By adding additional variables, we can disambiguate the stories; moreover, in the resulting causal models, the HP definition of causality gives the intuitively correct answer. The examples not only give insight into the modeling process, they also highlight some aspects of the definition of causality itself. Specifically, by extending one of the examples, it can be shown that a modification to the original HP definition made to deal with an example by Hopkins and Pearl may not be necessary. By extending another definition, a sequence of models can be constructed, each one a conservative extension of the one before, where the question of whether X=x is cause of Y=y alternates between being true and false.

ABSTRACT. We provide a sound and complete axiomatization for a class of logics appropriate for reasoning about the rationality of players in games. Essentially the same axiomatization applies to a wide class of decision rules.

ABSTRACT. We show that determining whether a Boolean game has an equilibrium that guarantees every player a given payoff is NEXP-hard. In the proof we encode a non-deterministic, exponential time Turing machine by having one player play a mixed strategy from which we can infer a computation history of the machine, and the other players verify that this history does in fact represent a valid, accepting run.