Invited Talks

Title: Quantitative Logic Reasoning – Combining logical reasoning with probabilities and counting

Speaker: Marcelo Finger, University of Sao Paulo, Brazil

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.

Title: An abstraction-refinement framework for automated reasoning – a pragmatic approach

Speaker: Konstantin Korovin, University of Manchester, UK

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.