Combining Answer Set Programming (ASP) and Constraint Logic Programming (CLP) can create a more powerful language for knowledge representation and reasoning. The language AC(C) is designed to integrate ASP and CLP. Compared with existing integration of ASP and CSP, AC(C) allows representing user-defined constraints. Such integration provides great power for applications requiring logical reasoning involving constraints, e.g., temporal planning. In AC(C), user-defined and primitive constraints can be solved by a CLP inference engine while the logical reasoning over those constraints and regular logic literals is solved by an ASP inference engine (i.e., solver). My PhD work includes improving the language AC(C), implementing its faster inference engine and investigating how effective the new system can be used to solve a challenging application, temporal planning.

Model update is a formal approach to correct a system model M w.r.t some property not satisfied by M. In this work, we show how this formal approach can be used for plan and planning domain verification and update. While a model checking method can directly be used to perform plan verification, model update techniques can be used to either update an incorrect plan and\or update a planning domain specification. Well known model update approaches are based on CTL — a logic which does not take into account the actions. In previous work, we have proposed the alpha-CTL logic, a logic whose semantics is based on actions. Here, we are proposing a model update system based on alpha-CTL which is able to automatically modify a plan M, generating a new plan M' that satisfies phi or, if there is not such a plan, to automatically update the corresponding planning domain.

Cluedo) serves as a fun when it comes to designing an optimal (or even practicable) focus problem for this introduction to propositional knowledge solution. The potential solutions also touch on many representation and reasoning. After covering fundamentals areas of AI, so the students can be creative in applying and of propositional logic, students first solve basic synthesizing what they've learned to a new problem. The logic problems with and without the aid of a satisfiability three challenges give the students the opportunity to choose solver (e.g.

We present a new approach to characterizing the semantics for the integration of rules and first-order logic in general, and description logics in particular, based on a circumscription characterization of answer set programming, introduced earlier by Lin and Zhou. We show that both Rosati's semantics based on NM-models and Lukasiewicz's answer set semantics can be characterized by circumscription, and the difference between the two can be seen as a matter of circumscription policies. This approach leads to a number of new insights. First, we rebut a criticism on Lukasiewicz's semantics for its inability to reason for negative consequences. Second, our approach leads to a spectrum of possible semantics based on different circumscription policies, and shows a clear picture of how they are related. Finally, we show that the idea of this paper can be applied to first-order general stable models.

Recently the general Game Description Language (GDL) has been extended so as to cover arbitrary games with incomplete/imperfect information. Learning — without human intervention — to play such games poses a reasoning challenge for general game-playing systems that is much more intricate than in case of complete information games. Action formalisms like the Situation Calculus have been developed for precisely this purpose. In this paper we present a full embedding of the Game Description Language into the Situation Calculus (with Scherl and Levesque's knowledge fluent ). We formally prove that this provides a sound and complete reasoning method for players' knowledge about game states as well as about the knowledge of the other players.

The result of forgetting some predicates in a first-order sentence may not exist in the sense that it might not be captured by any first-order sentences. This, indeed, severely restricts the usage of forgetting in applications. To address this issue, we propose a notion called $k$-forgetting, also called bounded forgetting in general, for any fixed number $k$. We present several equivalent characterizations of bounded forgetting and show that the result of bounded forgetting, on one hand, can always be captured by a single first-order sentence, and on the other hand, preserves the information that we are concerned with.

A general game player automatically learns to play arbitrary new games solely by being told their rules. For this purpose games are specified in the game description language GDL, a variant of Datalog with function symbols and a few known keywords. In its latest version GDL allows to describe nondeterministic games with any number of players who may have imperfect, asymmetric information. We analyse the epistemic structure and expressiveness of this language in terms of epistemic modal logic and present two main results: The operational semantics of GDL entails that the situation at any stage of a game can be characterised by a multi-agent epistemic (i.e., S5-) model; (2) GDL is sufficiently expressive to model any situation that can be described by a (finite) multi-agent epistemic model.

General Game Players (GGPs) are programs which can play an arbitrary game given only its rules and the Game Description Language (GDL) is a variant of Datalog used in GGP competitions to specify the rules. GDL inherits from Datalog the use of Horn clauses as rules and recursion, but it too requires stratification and does not allow to use quantifiers. We present an alternative formalism for game description which is based on first-order logic (FO). States of the game are represented by relational structures, legal moves by structure rewriting rules guarded by FO formulas, and the goals of the players by formulas which extend FO with counting. The advantage of our formalism comes from more explicit state representationcand from the use of quantifiers in formulas. We show how to exploit existential quantification in players' goals to generate heuristics for evaluating positions in the game. The derived heuristics are good enough for a basic alpha-beta agent to win against state of the art GGP.

The research on low-complexity nonmonotonic description logics recently identified a fragment of EL with bottom, supporting defeasible inheritance with overriding, where reasoning can be carried out in polynomial time. We contribute to that framework by supporting more axiom schemata and all the concept constructors of EL++ without increasing asymptotic complexity. Moreover, we show that all the syntactic restrictions we adopt are necessary by proving several coNP-hardness results.

We present a computational method to generate explanations to answers of complex queries over biomedical ontologies and databases, using the high-level representation and efficient automated reasoners of Answer Set Programming. We show the applicability of our approach with some queries related to drug discovery over PHARMGKB, DRUGBANK, BIOGRID, CTD and SIDER.