Epistemic logic programs (ELPs) are a popular generalization of standard Answer Set Programming (ASP) providing means for reasoning over answer sets within the language. This richer formalism comes at the price of higher computational complexity reaching up to the fourth level of the polynomial hierarchy. However, in contrast to standard ASP, dedicated investigations towards tractability have not been undertaken yet. In this paper, we give first results in this direction and show that central ELP problems can be solved in linear time for ELPs exhibiting structural properties in terms of bounded treewidth. We also provide a full dynamic programming algorithm that adheres to these bounds. Finally, we show that applying treewidth to a novel dependency structure---given in terms of epistemic literals---allows to bound the number of ASP solver calls in typical ELP solving procedures.

Relation Extraction (RE), the task of detecting and characterizing semantic relations between entities in text, has gained much importance in the last two decades, mainly in the biomedical domain. Many papers have been published on Relation Extraction using supervised machine learning techniques. Most of these techniques rely on statistical methods, such as feature-based and tree-kernels-based methods. Such statistical learning techniques are usually based on a propositional hypothesis space for representing examples, i.e., they employ an attribute-value representation of features. This kind of representation has some drawbacks, particularly in the extraction of complex relations which demand more contextual information about the involving instances, i.e., it is not able to effectively capture structural information from parse trees without loss of information. In this work, we present OntoILPER, a logic-based relational learning approach to Relation Extraction that uses Inductive Logic Programming for generating extraction models in the form of symbolic extraction rules. OntoILPER takes profit of a rich relational representation of examples, which can alleviate the aforementioned drawbacks. The proposed relational approach seems to be more suitable for Relation Extraction than statistical ones for several reasons that we argue. Moreover, OntoILPER uses a domain ontology that guides the background knowledge generation process and is used for storing the extracted relation instances. The induced extraction rules were evaluated on three protein-protein interaction datasets from the biomedical domain. The performance of OntoILPER extraction models was compared with other state-of-the-art RE systems. The encouraging results seem to demonstrate the effectiveness of the proposed solution.

To solve hard problems, AI relies on a variety of disciplines such as logic, probabilistic reasoning, machine learning and mathematical programming. Although it is widely accepted that solving real-world problems requires an integration amongst these, contemporary representation methodologies offer little support for this. In an attempt to alleviate this situation, we introduce a new declarative programming framework that provides abstractions of well-known problems such as SAT, Bayesian inference, generative models, and convex optimization. The semantics of programs is defined in terms of first-order structures with semiring labels, which allows us to freely combine and integrate problems from different AI disciplines.

In this paper, we aim to study how the performance of modern answer set programming (ASP) solvers is influenced by the treewidth of the input program and to investigate the consequences of this relationship. We first perform an experimental evaluation that shows that the solving performance is heavily influenced by treewidth, given ground input programs that are otherwise uniform, both in size and construction. This observation leads to an important question for ASP, namely, how to design encodings such that the treewidth of the resulting ground program remains small. To this end, we study two classes of disjunctive programs, namely guarded and connection-guarded programs. In order to investigate these classes, we formalize the grounding process using MSO transductions. Our main results show that both classes guarantee that the treewidth of the program after grounding only depends on the treewidth (and the maximum degree, in case of connection-guarded programs) of the input instance. In terms of parameterized complexity, our findings yield corresponding FPT results for answer-set existence for bounded treewidth (and also degree, for connection-guarded programs) of the input instance. We further show that bounding treewidth alone leads to NP-hardness in the data complexity for connection-guarded programs, which indicates that the two classes are fundamentally different. Finally, we show that for both classes, the data complexity remains as hard as in the general case of ASP.

By embracing diversity, humanity finds greater strength. Our differences mean we can specialize, using our unique talents to excel in the areas to which we are most suited. This is as true for intelligence as for physical attributes. One person may solve complex algebraic equations for fun but care less about which political party is in power; another may have trouble calculating the tip on a restaurant check but can spend hours discussing the ins and outs of global foreign policy. Both are important skills, but with different applications.

Epistemic Logic Programs (ELPs) are an extension of Answer Set Programming (ASP) with epistemic operators that allow for a form of meta-reasoning, that is, reasoning over multiple possible worlds. Existing ELP solving approaches generally rely on making multiple calls to an ASP solver in order to evaluate the ELP. However, in this paper, we show that there also exists a direct translation from ELPs into non-ground ASP with bounded arity. The resulting ASP program can thus be solved in a single shot. We then implement this encoding method, using recently proposed techniques to handle large, non-ground ASP rules, into the prototype ELP solving system "selp", which we present in this paper. This solver exhibits competitive performance on a set of ELP benchmark instances. Under consideration in Theory and Practice of Logic Programming (TPLP).

Modern applications of artificial intelligence in decision support systems, plan generation systems require reasoning with imprecise a nd uncertain information. Logical frameworks based on bivalent reasoning are not suitable for such applications, because the set {0, 1} cannot capture the vagueness or uncertainty of underlying proposition. Though fuzzy log ic-based systems can represent imprecise linguistic information by ascribi ng membership values to attributes (or truth values to propositions) taken fr om the interval 1 [0,1], but this graded valuation becomes inadequate if the p recise membership can not be determined due to some underlying uncerta inty. This uncertainty may arise from lack of complete information or f rom lack of reliability of source of information or lack of unanimity amon g rational agents in a multi-agent reasoning system or from many other reasons . This uncertainty with respect to the assignment of membership degr ees is captured by assigning a range of possible membership values, i.e. by a ssigning an interval.

In this paper we investigate CNF formulas, for which the unit propagation is strong enough to derive a contradiction if the formula together with a partial assignment of the variables is unsatisfiable (unit refutation complete or URC formulas) or additionally to derive all implied literals if the formula is satisfiable (propagation complete or PC formulas). If a formula represents a function using existentially quantified auxiliary variables, it is called an encoding of the function. We prove several results on the sizes of PC and URC formulas and encodings. One of them are separations between the sizes of formulas of different types. Namely, we prove an exponential separation between the size of URC formulas and PC formulas and between the size of PC encodings using auxiliary variables and URC formulas. Besides of this, we prove that the sizes of any two irredundant PC formulas for the same function differ at most by a polynomial factor in the number of the variables and present an example of a function demonstrating that a similar statement is not true for URC formulas. One of the separations above implies that a q-Horn formula may require an exponential number of additional clauses to become a URC formula. On the other hand, for every q-Horn formula, we present a polynomial size URC encoding of the same function using auxiliary variables. This encoding is not q-Horn in general.

In the 1930s and 40s, around the birth of the "automatic computer", mathematicians wanted to formalise what we mean when we say some result or some function is "effectively computable", whether by machine or human. A "computer", originally, was a person who performed arithmetic calculations. The "effectively" part is included to indicate that we are not concerned with the time any particular computer might take to produce the result, so long as it would get there eventually. They wanted to find the simplest possible system that could be said to compute. Several such systems were invented and for the most part looked entirely unlike each other. Remarkably, they were all eventually shown to be equivalent in the sense that any one could be made to behave like the others.

Synthesizing a program that realizes a logical specification is a classical problem in computer science. We examine a particular type of program synthesis, where the objective is to synthesize a strategy that reacts to a potentially adversarial environment while ensuring that all executions satisfy a Linear Temporal Logic (LTL) specification. Unfortunately, exact methods to solve so-called LTL synthesis via logical inference do not scale. In this work, we cast LTL synthesis as an optimization problem. We employ a neural network to learn a Q-function that is then used to guide search, and to construct programs that are subsequently verified for correctness. Our method is unique in combining search with deep learning to realize LTL synthesis. In our experiments the learned Q-function provides effective guidance for synthesis problems with relatively small specifications.