ABSTRACT. A warm welcome to everybody interested in reasoning with preferences, uncertainty and vagueness!

ABSTRACT. We present a research program which investigates the intersection of deductive reasoning with explicit quantitative capabilities. These capabilities encompass probabilistic reasoning, counting and counting quantifiers, and similar systems. The need to have a combined reasoning system that enables a unified way of reasoning with quantities has always been recognized in modern logic, as proposals of probabilistic logic reasoning are present since the work of Boole [1854]. Equally ubiquitous is the need to deal with cardinality restrictions on finite sets. More recently, a well-founded probabilistic theory has been developed for non-classical settings as well, such as probabilistic reasoning over Lukasiewicz infinitely-valued logic.

We show that there is a common way to deal with these several deductive quantitative capabilities, involving a framework based on Linear Algebra and Linear Programming. The distinction between classical and non-classical reasoning on the one hand, and probabilistic and cardinality reasoning on the other hand, comes from the different family of algebras employed. The quantitative logic systems also allow for the introduction of inconsistency measurements, which quantify the degree of inconsistency of a given quantitative logic theory, following some basic principles of inconsistency measurements.

On the practical level, we aim at exploring quantitative logic systems in which the complexity of reasoning is "only NP-complete". We provide open-source implementations for solvers operating over those systems and study some notable empirical properties, such as the present of a phase transition.

ABSTRACT. When combining beliefs from different sources, often not only new knowledge but also conflicts arise. In this paper, we investigate how we can measure the disagreement among sources. We start our investigation with disagreement measures that can be induced from inconsistency measures in an automated way. After discussing some problems with this approach, we propose a new measures that is inspired by the eta-inconsistency measure. Roughly speaking, it measures how well we can satisfy all sources simultaneously. We show that the new measure satisfies desirable properties, scales well with respect to the number of sources and illustrate its applicability in inconsistency-tolerant reasoning.

ABSTRACT. In a large number of problems such as product configuration, automated recommendation and combinatorial auctions, decisions stem from agents subjective preferences and requirements in the presence of uncertainty. In this paper, we introduce a framework based on the belief function theory to deal with problems in group decision settings where the preferences of the agents may be uncertain, imprecise, incomplete, conflicting and possibly distorted. A case study is conducted on product recommendation to illustrate the applicability and validity of the proposed framework.

ABSTRACT. Soft constraints play a major rule in AI, since they allow to restrict the set of possible worlds (obtained from hard constraints) to a small fraction of preferred or most plausible states. Only a few formalisms fully integrate soft and hard constraints. A prominent examples is Qual- itative Choice Logic (QCL), where propositional logic is augmented by a dedicated connective and preferred models are discriminated via ac- ceptance degress determined by this connective. In this work, we follow an analogous approach in terms of syntax but propose an alternative semantics. The key idea is to assign to formulas a set of models plus a partial relation on these models. Preferred models are then obtained from this partial relation. We investigate properties of our logic which demon- strate that our semantics shows some favorable behavior compared to QCL. Moreover, we provide a partial complexity analysis of our logic.

ABSTRACT. Abstraction-refinement is widely used in verification but, with some exceptions, is largely overlooked in the state-of-the-art automated theorem proving. One of our main motivations comes from the problem of reasoning with large theories where usually only a small part of the theory is needed for proving the conjecture. Efficient reasoning with large theories is one of the main challenges in automated theorem proving arising in many applications including reasoning with ontologies, large mathematical theories and verification. Current methods for reasoning with large theories are mainly based on axiom selection which we believe is limited in the scope. We propose a general approach to automated reasoning based on abstraction-refinement which aims at over and under approximation of theories in order to speed up reasoning. In particular, in this approach axiom selection can be seen as a special case of under approximation. In this talk we present a general abstraction-refinement framework for automated reasoning, draw connections with current approaches and discuss some practical abstractions.

This is a joint work with Julio Cesar Lopez Hernandez.

ABSTRACT. Reasoning about exceptions in ontologies is nowadays one of the challenges the description logics community is facing. The paper describes a preferential approach for dealing with exceptions in Description Logics, based on the rational closure. The rational closure has the merit of providing a simple and efficient approach for reasoning with exceptions, but it does not allow independent handling of the inheritance of different defeasible properties of concepts. In this work we outline a possible solution to this problem by introducing a variant of the lexicographical closure, that we call {\em skeptical closure}, which requires to construct a single base. This work is based on the extended abstract presented at CILC/ICTCS 2017.

ABSTRACT. Automated decision making often requires solving difficult and primarily NP-hard problems. In many AI applications (e.g., planning, robotics, recommender systems), users can assist decision making by specifying their preferences over some domain of interest. To take preferences into account, we take a model-theoretic approach to both computations and preferences. Computational problems are characterized as model expansion, that is the logical task of expanding an input structure to satisfy a specification. The uniformity of the model-theoretic approach allows us to link preferences and computations by introducing a framework of a prioritized model expansion. The main technical contribution is an analysis of the impact of preferences on the computational complexity of model expansion. We also study an application of our framework for the case where some information about preferences is missing. Finally, we discuss how prioritized model expansion can be related to other preference-based declarative programming paradigms.

ABSTRACT. t. Constrained counting is important in domains ranging from artificial intelligence to software analysis. There are already a few approaches for counting models over various types of constraints. Recently, hashing-based approaches achieve success but still rely on solution enumeration. In the IJCAR version, a probabilistic approximate model counter is proposed, which is also a hashingbased universal framework, but with only satisfiability queries. A dynamic stopping criteria, for the algorithm, is presented, which has not been studied yet in previous works of hashing-based approaches. Although the algorithm lacks theoretical guarantee, it works well in practice. In this paper, we further extend our approach to SMT(LIA) formulas with a new encoding technique.

ABSTRACT. The entity resolution problem in traditional databases, also known as deduplication, seeks to map multiple virtual objects to its corresponding set of real-world entities. Though the problem is challenging, it can be tackled in a variety of ways by means of leveraging several simplifying assumptions, such as the fact that the multiple virtual objects appear as the result of name or attribute ambiguity, clerical errors in data entry or formatting, missing or changing values, or abbreviations. However, in cyber security domains the entity resolution problem takes on a whole different form, since malicious actors that operate in certain environments like hacker forums and markets are highly motivated to remain semi-anonymous---this is because, though they wish to keep their true identities secret from law enforcement, they also have a reputation to keep with their customers. The above simplifying assumptions cannot be made, and we therefore coin the term "adversarial deduplication" to refer to this setting. In this paper, we propose the use of probabilistic existential rules (also known as Datalog+/-) to model knowledge engineering solutions to this problem; we show that tuple-generating dependencies can be used to generate probabilistic deduplication hypotheses, and equality-generating dependencies can later be applied to leverage existing data towards grounding such hypotheses. The main advantage with respect to existing deduplication tools is that our model operates under the open-world assumption, and thus is capable of modeling hypotheses over unknown objects, which can later become known if new data becomes available.

ABSTRACT. We present VolCE, a tool for computing and estimating the size of the solution space of SMT(LA) constraints. VolCE supports the SMT-LIB format. It integrates SMT solving with volume computation/estimation and integer solution counting for convex polytopes. Several effective techniques are adopted, which enable the tool to deal with high-dimensional problem instances efficiently.