In this work we introduce a defeasible logic programming recommender server that accepts different types of queries from client agents that can be distributed in remote hosts. We formalize new ways of querying recommender servers containing specific information or preferences, and creating a particular context for the queries. This special type of queries (called contextual queries) allows recommender servers to compute recommendations for any client using its preferences, and will be answered using an argumentative inference mechanism. We focus on a particular implementation of recommended systems that extends the integration of argumentation and recommender systems to a multi-agent setting. Our approach is based on a DeLP-server that can answer queries from agents in remote hosts. Since client agents can consult different domain specific recommender servers, then, multiple configurations of clients and servers can be defined.

Inconsistency management policies allow a relational database user to express customized ways for managing inconsistency according to his need. For each functional dependency, a user has a library of applicable policies, each of them with constraints, requirements, and preferences for their application, that can contradict each other. The problem that we address in this work is that of determining a subset of these policies that are suitable for application w.r.t. the set of constraints and user preferences. We propose a classical logic argumentation-based solution, which is a natural approach given that integrity constraints in databases and data instances are, in general, expressed in first order logic (FOL). An automatic argumentation-based selection process allows to retain some of the characteristics of the kind of reasoning that a human would perform in this situation.

Insufficient knowledge and resources is not only a biological constraint on human and animal intelligence, but also has important functional implications for artificial intelligence (AI) systems. Traditional theories dominating AI research typically assume some kind of sufficiency of knowledge and resources, so cannot solve many problems in the field. AI needs new theories obeying this constraint, which cannot be obtained by minor revisions or extensions of the traditional theories. The practice of NARS, an AI project, shows that such new theories are feasible and promising in providing a new theoretical foundation for AI.

We describe some experiments which simulate a grounded approach to the acquisition of the cognitive and linguistic competence required to communicate propositional logic sentences. This encompasses both the construction of a conceptualisation of its environment by each individual agent and of a shared language by the population. The processes of conceptualisation and language acquisition in each individual agent are based on general purpose cognitive capacities, such as categorisation, discrimination, invention, adoption and induction. The construction of a shared language by the population is achieved using a particular type of linguistic interaction, known as the evaluation game, which gives rise to a common set of linguistic conventions through a process of self-organisation. This work addresses the problem of the acquisition of both the semantics and the syntax of propositional logic. Trying to learn these two aspects at the same time is more difficult than learning the semantics or the syntax of propositional logic separately. Because the agents must coordinate their linguistic behaviour taking into account only the subset of objects which constitutes the topic of a particular linguistic interaction. This means that a pair of agents can communicate successfully about a particular subset of objects (a topic) even if they use different conceptualisations (formulas) in order to identify the same topic. And this introduces a high degree of ambiguity in the interpretation process the agents have to deal with when they try to construct a shared communication language. In spite of this, the results of the experiments show that at the end of the simulation runs the individual agents build different conceptualisations and grammars, but that the conceptualisations and grammars of the agents in the population are compatible in the sense that they guarantee the unambiguous communication of propositional logic sentences.

The survey propagation (SP) algorithm has been shown to work well on large instances of the random 3-SAT problem near its phase transition. It was shown that SP estimates marginals over covers that represent clusters of solutions. The SP-y algorithm generalizes SP to work on the maximum satisfiability (Max-SAT) problem, but the cover interpretation of SP does not generalize to SP-y. In this paper, we formulate the relaxed survey propagation (RSP) algorithm, which extends the SP algorithm to apply to the weighted Max-SAT problem. We show that RSP has an interpretation of estimating marginals over covers violating a set of clauses with minimal weight. This naturally generalizes the cover interpretation of SP. Empirically, we show that RSP outperforms SP-y and other state-of-the-art Max-SAT solvers on random Max-SAT instances. RSP also outperforms state-of-the-art weighted Max-SAT solvers on random weighted Max-SAT instances.

We present a novel reasoning calculus for the description logic SHOIQ^+---a knowledge representation formalism with applications in areas such as the Semantic Web. Unnecessary nondeterminism and the construction of large models are two primary sources of inefficiency in the tableau-based reasoning calculi used in state-of-the-art reasoners. In order to reduce nondeterminism, we base our calculus on hypertableau and hyperresolution calculi, which we extend with a blocking condition to ensure termination. In order to reduce the size of the constructed models, we introduce anywhere pairwise blocking. We also present an improved nominal introduction rule that ensures termination in the presence of nominals, inverse roles, and number restrictions---a combination of DL constructs that has proven notoriously difficult to handle. Our implementation shows significant performance improvements over state-of-the-art reasoners on several well-known ontologies.

Prime implicates and prime implicants have proven relevant to a number of areas of artificial intelligence, most notably abductive reasoning and knowledge compilation. The purpose of this paper is to examine how these notions might be appropriately extended from propositional logic to the modal logic K. We begin the paper by considering a number of potential definitions of clauses and terms for K. The different definitions are evaluated with respect to a set of syntactic, semantic, and complexity-theoretic properties characteristic of the propositional definition. We then compare the definitions with respect to the properties of the notions of prime implicates and prime implicants that they induce. While there is no definition that perfectly generalizes the propositional notions, we show that there does exist one definition which satisfies many of the desirable properties of the propositional case. In the second half of the paper, we consider the computational properties of the selected definition. To this end, we provide sound and complete algorithms for generating and recognizing prime implicates, and we show the prime implicate recognition task to be PSPACE-complete. We also prove upper and lower bounds on the size and number of prime implicates. While the paper focuses on the logic K, all of our results hold equally well for multi-modal K and for concept expressions in the description logic ALC.

The recently introduced series of description logics under the common moniker `DL-Lite' has attracted attention of the description logic and semantic web communities due to the low computational complexity of inference, on the one hand, and the ability to represent conceptual modeling formalisms, on the other. The main aim of this article is to carry out a thorough and systematic investigation of inference in extensions of the original DL-Lite logics along five axes: by (i) adding the Boolean connectives and (ii) number restrictions to concept constructs, (iii) allowing role hierarchies, (iv) allowing role disjointness, symmetry, asymmetry, reflexivity, irreflexivity and transitivity constraints, and (v) adopting or dropping the unique same assumption. We analyze the combined complexity of satisfiability for the resulting logics, as well as the data complexity of instance checking and answering positive existential queries. Our approach is based on embedding DL-Lite logics in suitable fragments of the one-variable first-order logic, which provides useful insights into their properties and, in particular, computational behavior.

Despite the extensive development of first-principles planning in recent years, planning applications are still primarily developed using knowledge-based planners which can exploit domain-specific heuristics and weaker domain models.  Hierarchical Task Network (HTN) planners capture domain-specific heuristics for more efficient search, accommodate incomplete causal models, and can be used to enforce standard operating procedures.  Unfortunately, we do not have semantics for the methods or tasks that make up HTN models, that help evaluate the correctness of methods, or to build a reliable executive for HTN plans.  This paper fills the gap by providing a well-defined semantics for the methods and plans of SHOP2, a state-of-the-art HTN planner.  The semantics are defined in terms of concurrent golog (ConGolog) and the situation calculus.  We provide a proof of equivalence between the plans generated by SHOP2 and the action sequences of the ConGolog semantics.  We show how the semantics reflects the distinction between plan-time and execution-time, and provide some simple examples showing how the semantics can support method verification.  The semantics provide an implementation-neutral specification for an executive, showing how an executive must treat the plans SHOP2 generates in order to enforce the expected behaviors.  Future directions include automated verification of method specifications, automatically generating plan monitors, and plan revision and repair.

Planning based on propositional SAT(isfiability) is a powerful approach to computing step-optimal plans given a parallel execution semantics. In this setting: (i) a solution plan must be minimal in the number of plan steps required, and (ii) non-conflicting actions can be executed instantaneously in parallel at a plan step. Underlying SAT-based approaches is the invocation of a decision procedure on a SAT encoding of a bounded version of the problem. A fundamental limitation of existing approaches is the size of these encodings. This problem stems from the use of a direct representation of actions — i.e. each action has a corresponding variable in the encoding. A longtime goal in planning has been to mitigate this limitation by developing a more compact split — also termed lifted — representation of actions in SAT encodings of parallel step-optimal problems. This paper describes such a representation. In particular, each action and each parallel execution of actions is represented uniquely as a conjunct of variables. Here, each variable is derived from action pre and post- conditions . Because multiple actions share conditions , our encoding of the planning constraints is factored and relatively compact. We find experimentally that our encoding yields a much more efficient and scalable planning procedure over the state-of-the-art in a large set of planning benchmarks.