Logic & Formal Reasoning


Combining Axiom Injection and Knowledge Base Completion for Efficient Natural Language Inference

arXiv.org Artificial Intelligence

In logic-based approaches to reasoning tasks such as Recognizing Textual Entailment (RTE), it is important for a system to have a large amount of knowledge data. However, there is a tradeoff between adding more knowledge data for improved RTE performance and maintaining an efficient RTE system, as such a big database is problematic in terms of the memory usage and computational complexity. In this work, we show the processing time of a state-of-the-art logic-based RTE system can be significantly reduced by replacing its search-based axiom injection (abduction) mechanism by that based on Knowledge Base Completion (KBC). We integrate this mechanism in a Coq plugin that provides a proof automation tactic for natural language inference. Additionally, we show empirically that adding new knowledge data contributes to better RTE performance while not harming the processing speed in this framework.


An Introduction to Fuzzy & Annotated Semantic Web Languages

arXiv.org Artificial Intelligence

We present the state of the art in representing and reasoning with fuzzy knowledge in Semantic Web Languages such as triple languages RDF/RDFS, conceptual languages of the OWL 2 family and rule languages. We further show how one may generalise them to so-called annotation domains, that cover also e.g.


Constructive Logic Covers Argumentation and Logic Programming

AAAI Conferences

In this work, we show that both logic programming and abstract argumentation frameworks can be interpreted in terms of Nelson's constructive logic N4. We do so by formalising, in this logic, two principles that we call non-contradictory inference and strengthened closed world assumption: the first states that no belief can be held based on contradictory evidence while the later forces both unknown and contradictory evidence to be regarded as false. Using these principles, both logic programming and abstract argumentation frameworks are translated into constructive logic in a modular way and using the object language. Logic programming implication and abstract argumentation supports become, in the translation, a new implication connective following the non-contradictory inference principle. Attacks are then represented by combining this new implication with strong negation.


Preference Relations by Approximation

AAAI Conferences

Declarative languages for knowledge representation and reasoning provide constructs to define preference relations over the set of possible interpretations, so that preferred models represent optimal solutions of the encoded problem. We introduce the notion of approximation for replacing preference relations with stronger preference relations, that is, relations comparing more pairs of interpretations. Our aim is to accelerate the computation of a non-empty subset of the optimal solutions by means of highly specialized algorithms. We implement our approach in Answer Set Programming (ASP), where problems involving quantitative and qualitative preference relations can be addressed by ASPRIN, implementing a generic optimization algorithm. Unlike this, chains of approximations allow us to reduce several preference relations to the preference relations associated with ASP's native weak constraints and heuristic directives. In this way, ASPRIN can now take advantage of several highly optimized algorithms implemented by ASP solvers for computing optimal solutions.


Introducing Temporal Stable Models for Linear Dynamic Logic

AAAI Conferences

We propose a new temporal extension of the logic of Here-and-There (HT) and its equilibriaobtained by combining it with dynamic logic over (linear) traces. Unlike previous temporal extensions of HT based on linear temporal logic, the dynamic logic features allow us to reason about the composition of actions. For instance, this can be used to exercise fine grained control when planning in robotics, as exemplified by GOLOG. In this paper,we lay the foundations of our approach, and refer to it as "Linear Dynamic Equilibrium Logic", or simply DEL. We start by developing the formal framework of DEL and provide relevant characteristic results. Among them, we elaborate upon the relationships to traditional linear dynamic logic and previous temporal extensions of HT.


Weight Learning in a Probabilistic Extension of Answer Set Programs

AAAI Conferences

LPMLN is a probabilistic extension of answer set programs with the weight scheme derived from that of Markov Logic. Previous work has shown how inference in LPMLN can be achieved. In this paper, we present the concept of weight learning in LPMLN and learning algorithms for LPMLN derived from those for Markov Logic. We also present a prototype implementation that uses answer set solvers for learning as well as some example domains that illustrate distinct features of LPMLN learning. Learning in LPMLN is in accordance with the stable model semantics, thereby it learns parameters for probabilistic extensions of knowledge-rich domains where answer set programming has shown to be useful but limited to the deterministic case, such as reachability analysis and reasoning about actions in dynamic domains. We also apply the method to learn the parameters for probabilistic abductive reasoning about actions.


A Hybrid Approach to Optimization in Answer Set Programming

AAAI Conferences

Answer set programming (ASP) is today a successful approach to knowledge representation and reasoning in various real-world problem domains. ASP offers an expressive rule-based constraint modelling language, supporting concise declarative modelling of both decision and optimization problems within the first or the second level of the polynomial hierarchy. In this paper, we propose a new approach to solving optimization problems via ASP, i.e., to the problem of finding optimal solutions (in terms of optimal answer sets or stable models) under a given weight function over soft atoms (weak constraints). Our approach constitutes the first adaptation of the so-called implicit hitting set approach in the context of ASP. In particular, in contrast to the earlier proposed family of core-guided algorithms for optimization in answer set programming, we present a hybrid approach which makes use of interactions between an ASP decision solver (as an unsatisfiable core extractor) and an integer programming solver (as a minimum-cost hitting set algorithm). We explain how various concepts and features specific to ASP and IP can be harnessed within the approach, including several ways for obtaining better upper and lower bounds during search, with the aim of speeding up the computation of an optimal answer set. By a careful integration of the interactions between state-of-the-art ASP and IP solvers, we show that already our first implementation provides a complementary approach when empirically compared to the currently available solvers supporting optimization in answer set programming.


An Incremental Approach to Structured Argumentation over Dynamic Knowledge Bases

AAAI Conferences

Considering the structure of arguments allows users to analyze reasons for and against a conclusion; the warrant status of such a conclusion in the context of a knowledge base represents the main output of a dialectical process. A naive approach to computing such statuses is costly, and any update to the knowledge base potentially has a huge impact if done in this manner. We study the case of updates consisting of both additions and removals of pieces of knowledge in the Defeasible Logic Programming (DeLP) framework, first analyzing the complexity of the problem and then identifying conditions under which we can avoid unnecessary computations-- central to this is the development of data structures to keep track of which results can potentially be affected by a given update.


Omission-Based Abstraction for Answer Set Programs

AAAI Conferences

Abstraction is a well-known approach to reduce program complexity by over-approximating the problem with a deliberate loss of information. It has not been considered so far in the context of Answer Set Programming, a convenient tool for problem solving. In this paper, we introduce a method to automatically abstract ground ASP programs that preserves their structure by reducing the vocabulary. Such an abstraction makes it possible to generate partial answer set candidates, which can help with the approximation of reasoning. Faithful (non-spurious) abstractions may be used to represent the projection of answer sets and to guide solvers in answer set construction. In order to deal with the unavoidably introduced spurious answer sets, we employ an ASP debugging approach to help with the refinement of the abstraction. We investigate the usage of such an abstraction to obtain explanations of unsatisfiable programs as a show case.


A Generator of Hard 2QBF Formulas and ASP Programs

AAAI Conferences

The availability of generators of random instances of boolean formulas has had a major impact on solver technology for KR formalisms such as SAT, QBF and ASP. Recently, we proposed new models of random QSAT formulas in non-clausal form, as well as the first model of random disjunctive logic programs. Our models support generating instances of substantial hardness. Here, we present a tool that generates formulas/programs from the new models in a variety of output formats including (Q)DIMACS, QCIR, and ASPCore 2.0.