ABSTRACT. This work deals with the problem of combining reactive features, such as the ability to respond to events and define complex events, with the execution of ACID transactions over general Knowledge Bases (KBs).

With this as goal, we build on Transaction Logic (TR), a logic precisely designed to model and execute (ACID) transactions in KBs defined in arbitrary logic theories. In it, transactions are written in a logic-programming style, by combining primitive update operations over a general KB, with the usual logic programming connectives and some additional connectives e.g. to express sequence of actions.

While TR is a natural choice to deal with transactions, it remains the question whether if TR can be used to express complex events, but also to deal simultaneously with the detection of complex events and the execution of transactions. In this paper we show that the former is possible while the latter is not. For that, we start by illustrating how TR can express and detect complex events, and in particular, how SNOOP event expressions can be translated in the logic. Afterwards, we show why TR fails to deal with the two issues together, and propose Transaction Logic with Events to solve the intended problem.

The achieved solution is a non-monotonic conservative extension of TR, which guarantees that every complex event detected in a transaction is necessarily responded. Along with its syntax, model theory and executional semantics, in this paper we prove the correspondence of Transaction Logic with Events with TR, and that it enjoys from important properties of non-monotonic logics, like support.

ABSTRACT. The stable model (SM) semantics lacks the properties of existence, relevance and cumulativity. This is due to the set of SM models being generally smaller than the set of all minimum models of a normal logic program (the semantics that consists in all the minimal models of a normal logic program, let it be SEMmin, trivially verifies these three properties). If we prospectively consider the class of conservative extensions of SM semantics (i.e., semantics that for each normal logic program P retrieve a superset of the set of stable models of P), other than the trivial SEMmin, one may wander how do the semantics of this class behave in what concerns the aforementioned properties. That is the type of issue we deal with in this paper. We define a large class of conservative extensions of the SM semantics, dubbed affix stable model semantics, ASM, and study the above referred properties into two non-disjoint subfamilies of the class ASM, here dubbed ASMh and ASMm. From this study a number of results stem which facilitate the assessment of semantics in the class ASMh ∪ASMm with respect to the properties of existence, relevance and cumulativity, whilst unveiling relations among these properties. The following results should be emphasized: (1) We present a refined definition of cumulativity for semantics of in the class ASMh ∪ ASMm, which turns into an easier job the dismissal of this property by resorting to counter-examples; (2) We divide the sets of rules of normal logic programs into layers, and use the decomposition of models into that layered structure to define three new (structural) properties, defectivity, excessiveness and irregularity, which allow to state a number of relations between the properties of existence, relevance and cumulativity for semantics of the ASMh ∪ ASMm class, and at the same time facilitate the assessment of semantics in this class with respect to those properties; (3) As a result of the approach in our work light is shed on the characterization of the SM semantics, as we show that the properties of (lack of) existence and (lack of) cautious monotony are equivalent, which opposes statements on this issue that may be found in the literature; we also characterize the relevance failure of SM semantics in a more clear way than usually stated in the literature.

ABSTRACT. An FOL-program consists of a background theory in a decidable fragment of first-order logic and a collection of rules possibly containing first-order formulas. The formalism stems from recent approaches to tight integrations of ASP with description logics. In this paper, we define a well-founded semantics for FOL-programs based on a new notion of unfounded sets on consistent as well as inconsistent sets of literals, and study some of its properties. The semantics is defined for all FOL-programs, including those where it is necessary to represent inconsistencies explicitly. The semantics supports a form of combined reasoning by rules under closed world as well as open world assumptions, and it is a generalization of the standard well-founded semantics for normal logic programs. We also show that the well-founded semantics defined here approximates the well-supported answer set semantics for normal DL programs.

ABSTRACT. Existing semantics for answer-set program updates fall into two categories: either they consider only strong negation in heads of rules, or they primarily rely on default negation in heads of rules and optionally provide support for strong negation by means of a syntactic transformation. In this paper we pinpoint the limitations of both these approaches and argue that both types of negation should be first-class citizens in the context of updates. We identify principles that plausibly constrain their interaction but are not simultaneously satisfied by any existing rule update semantics. Then we extend one of the most advanced semantics with direct support for strong negation and show that it satisfies the outlined principles as well as a variety of other desirable properties.

ABSTRACT. Cause-effect relations are an important part of human knowledge. In real life, humans often reason about complex causes linked to complex effects. By comparison, existing formalisms for representing knowledge about causal relations are quite limited in the kind of specifications of causes and effects they allow. In this paper, we present the new language C-Log, which offers a significantly more expressive representation of effects. We show how Approximation Fixpoint Theory can be used to define a formal semantics that captures the intuitions underlying this language. We also compare C-Log with several related languages and paradigms, including inductive definitions, disjunctive logic programming, and extensions of Datalog and we show that we provided a new semantics for (a generalisation of) disjunctive logic programming with existential quantifications in rule heads.

ABSTRACT. This paper introduces an epistemic specification solver ESmodels, which is designed and implemented as an experiment platform to investigate the semantics, language, related reasoning algorithms, and possible applications of epistemic specifications.We first give the epistemic specification language of ESmodels and its semantics. The language only employs one modal operator K but we prove that it is able to represent luxuriant modal operators by presenting transformation rules. Then, we describe basic algorithms and optimization approaches used in ESmodels. After that, we discuss several applications of ESmodels in commonsense reasoning, conformant planning, constraint satisfaction. Finally, we conclude with perspectives.

ABSTRACT. Bound Founded Answer Set Programming (BFASP) is an extension of Answer Set Programming (ASP) that extends stable model semantics to numeric variables. While the theory of BFASP is defined on ground rules, in practice BFASP programs are written as complex non-ground expressions. Flattening of BFASP is a technique used to simplify arbitrary expressions of the language to a small and well defined set of primitive expressions. In this paper, we first show how we can flatten arbitrary BFASP rule expressions, to give equivalent BFASP programs. Next, we extend the bottom-up grounding technique and magic set transformation used by ASP to BFASP programs. Our implementation shows that for BFASP problems, these techniques can significantly reduce the ground program size, and improve subsequent solving.

ABSTRACT. Traditional AI reasoning techniques have been used successfully in many domains, including logistics, scheduling and game playing. This paper is part of a project aimed at investigating how such techniques can be extended to coordinate teams of unmanned aerial vehicles (UAVs) in dynamic environments. Specifically challenging are real-world environments where UAVs and other network-enabled devices must communicate to coordinate---and communication actions are neither reliable nor free. Such network-centric environments are common in military, public safety and commercial applications, yet most research (even multi-agent planning) usually takes communications among distributed agents as a given. We address this challenge by developing an agent architecture and reasoning algorithms based on Answer Set Programming (ASP). ASP has been chosen for this task because it enables high flexibility of representation, both of knowledge and of reasoning tasks. Although ASP\ has been used successfully in a number of applications, and ASP-based architectures have been studied for about a decade, to the best of our knowledge this is the first practical application of an ASP based agent architecture. It is also the first practical application of ASP\ involving a combination of centralized reasoning, decentralized reasoning, execution monitoring, and reasoning about network communications. This work has been empirically validated using a distributed network-centric software evaluation testbed and the results provide guidance to designers in how to understand and control intelligent systems that operate in these environments.

ABSTRACT. The number of issues, stakeholders and regulations that a policy must consider in the current world is so high that trying to address them only with good-will and common-sense is unthinkable. Policy makers have to consider disparate issues, as diverse as economic development, pollution, traffic, as well as the acceptance of the policy from the population, just to name a few. This holds also for relatively low-scale levels, such as the Regional scope, not to mention National or European levels. A single person cannot be expert in all these subjects, and to obtain a suitable policy in the current complex world one can adopt decision support systems featuring optimization components.

Leveraging on previous work on Strategic Environmental Assessment, we developed a fully-fledged system that is able to provide optimal plans with respect to a given objective, to perform multi-objective optimization and provide sets of Pareto optimal plans, and to visually compare plans. While the previous version only considered qualitative information, the new version provides also the environmental footprint of the plan in a quantitative information, considering emissions, global warming effect, human toxicity, and acidification. The heart of the system is an application developed in a popular Constraint Logic Programming system on the Reals sort. It has been equipped with a web service module that can be queried through standard interfaces. An intuitive graphic user interface has been added to provide easy access to the web service and the CLP application.

ABSTRACT. Min-closed constraints are numerical relationships characterised by a simple algebraic property. Yet, with finite domain variables, min-closed systems give rise to a polynomial class of Constraint Satisfaction Problems. Propagation alone checks them for satisfiability. Solving is therefore search-free. Can this noteworthy result be generalized from a discrete to a continuous (or mixed) setting, with constraints involving real variables, using interval solvers? In this paper, we show that the completeness property observed in the discrete case gracefully degrades into a 'close approximation' property in the continuous case, which is also more general. When switching from finite to infinite domains, we show that the pruning power of propagation remains intact in the sense that it provides a box enclosure whose lower bound cannot be further updated (even by domain splitting). In the corresponding integer case, this box, when not empty, has a least element. This witness point thus ensures satisfiability and restores decidability. Applications of this analysis to scheduling, rule-based reasoning and scientific simulation are finally briefly mentioned.

ABSTRACT. We present the new ASP system clingo 4. Unlike its predecessors, being mere monolithic combinations of the grounder gringo with the solver clasp, the new clingo 4 series offers high-level constructs for realizing complex reasoning processes. Among others, such processes feature advanced forms of search, as in optimization or theory solving, or even interact with an environment, as in robotics or query-answering. Common to them is that the problem specification evolves during the reasoning process, either because data or constraints are added, deleted, or replaced. In fact, clingo 4 carries out such complex reasoning within a single integrated ASP grounding and solving process. This avoids redundancies in relaunching grounder and solver programs and benefits from the solver's learning capacities. clingo 4 accomplishes this by complementing ASP's declarative input language by control capacities expressed via the embedded scripting languages lua and python. On the declarative side, clingo 4 offers a new directive that allows for structuring logic programs into named and parameterizable subprograms. The grounding and integration of these subprograms into the solving process is completely modular and fully controllable from the procedural side, viz. the scripting languages. By strictly separating logic and control programs, clingo 4 also abolishes the need for dedicated systems for incremental and reactive reasoning, like iclingo and oclingo, respectively, and its flexibility goes well beyond the advanced yet still rigid solving processes of the latter.

ABSTRACT. The field of Distributed Constraint Optimization Problems (DCOPs) has gained momentum, thanks to its suitability to capture complex problems (e.g., resource allocation and management, multi-agent coordination) that are naturally distributed and cannot be realistically addressed in a centralized manner. The state-of-the-art in solving DCOPs relies on the use of ad-hoc infrastructures and ad-hoc constraint solving procedures. This paper investigates an infrastructure for solving DCOPs that is completely built on logic programming technologies. In particular, the paper explores the use of a general constraint solver (CLP in this context) to handle the agent-level constraint solving. The preliminary experiments shows that logic programming provides benefits over a state-of-the-art DCOP system in terms of performance and scalability, opening the doors to the use more advanced technology (e.g., search strategies, complex constraints) for solving DCOPs.

ABSTRACT. Coalgebraic Logic Programming (CoALP) is a dialect of Logic programming designed to work with coinductive definitions of infinite objects. Its main goal is to introduce guarded lazy corecursion akin functional theorem provers into logic programming. In this paper, we give the first full formal account of guarded corecursion in CoALP, and present its implementation.

ABSTRACT. Probabilistic Logic Programming (PLP) languages enable programmers to specify systems that combine logical models with statistical knowledge. The inference problem, to determine the probability of query answers in PLP, is intractable in general, thereby motivating the need for approximate techniques. In this paper, we present a technique for approximate inference of conditional probabilities for PLP queries. It is an Adaptive Markov Chain Monte Carlo (MCMC) technique, where the distribution from which samples are drawn is modified as the Markov Chain is explored. In particular, the distribution is progressively modified to increase the likelihood that a generated sample is consistent with evidence. In our context, each sample is uniquely characterized by the outcomes of a set of random variables. Inspired by reinforcement learning, our technique propagates rewards to random variable/outcome pairs used in a sample based on whether the sample was consistent or not. The cumulative rewards of each outcome is used to derive a new ``adapted distribution'' for each random variable. For a sequence of samples, the distributions are progressively adapted after each sample. For a query with ``Markovian evaluation structure'', we show that the adapted distribution of samples converges to the query's conditional probability distribution. For Markovian queries, we present a modified adaptation process that can be used in adaptive MCMC as well as adaptive independent sampling. We empirically evaluate the effectiveness of the adaptive sampling methods for queries with and without Markovian evaluation structure.

ABSTRACT. This paper introduces a framework for the bottom-up simulation of SLD-resolution based on partial evaluation. The main idea is to use database facts to represent a set of SLD goals. For deductive databases it is natural to assume that the rules defining derived predicates are known at "compile time", whereas the database predicates are known only later at runtime. The framework is inspired by the author's own SLDMagic method, and a variant of Earley deduction recently introduced by Heike Stephan and the author. However, it opens a much broader perspective.

ABSTRACT. Abductive logic programs offer a formalism to declaratively represent and reason about problems  in a variety of areas: diagnosis, decision making, hypothetical reasoning, etc. On the other hand, logic program updates allow us to express knowledge changes, be they internal (or self) and external (or world) changes. Abductive logic programs and logic program updates thus naturally coexist in problems that are susceptible to hypothetical reasoning about change. Taking this as a motivation, in this paper we integrate abductive logic programs and logic program updates by jointly exploiting tabling features of logic programming. The integration is based on and benefits from the two implementation techniques we separately devised previously, viz., tabled abduction and incremental tabling for query-driven propagation of logic program updates. A prototype of the integrated system is implemented in XSB Prolog.

ABSTRACT. A critical component in the design of a concurrent tabling system is the implementation of the table space. One of the most successful data structure for representing tables is based on a two-level trie data structure, where one trie level stores the tabled subgoal calls and the other stores the computed answers. In the previous work, we have presented a sophisticated lock-free design where both levels of the tries where shared among threads in a concurrent environment. To implement lock-freedom we used the CAS atomic instruction that nowadays can be widely found on many common architectures. The CAS reduces the granularity of the synchronization when threads access concurrent areas. However, different concurrent areas can interfere with each other on strong memory hardware architectures, creating problems such as false sharing or cache memory ping pong effects. In this work, we present a simpler and efficient lock-design design based on hash tries that minimizes these problems by dispersing as much as possible the concurrent areas. Experimental results show that our new lock-free design can effectively reduce the execution time and scale better, when increasing the number of threads, than the previous designs.

ABSTRACT. Higher-order constructs extend the expressiveness of first-order (Constraint) Logic Programming ((C)LP). At the same time assertions have been in use for some time in (C)LP systems helping programmers detect errors and validate programs. We report on our work towards filling this gap by extending the assertion-based approach to error detection and program validation to the higher-order context. We propose an extension of properties and assertions as used in (C)LP in order to be able to fully describe arguments that are predicates. We have developed syntax and semantics for (higher-order) properties and assertions, as well as for programs which contain such assertions, as well as several alternatives for performing run-time checking of such programs.

ABSTRACT. Several techniques and tools have been developed for verification in Horn clauses with constraints over some background theory (CHC). Current CHC verification tools implement intricate algorithms and are limited to certain subclasses of CHC problems. Our aim in this work is to investigate the use of a combination of off-the-shelf techniques from the literature in analysis and transformation of Constraint Logic Programs (CLP) to solve challenging CHC verification problems. We find that many problems can be solved using a combination of tools based on well-known techniques from abstract interpretation, semantics-preserving transformations, program specialisation and query-answer transformations. This gives insights into the design of automatic, more general CHC verification tools based on a library of components.

ABSTRACT. Several Prolog interpreters are based on the Warren Abstract Machine (WAM), an elegant model to compile Prolog programs. In order to improve the performance several strategies have been proposed, such as: optimize the selection of clauses, specialize the unification, global analysis, native code generation and tabling. This paper proposes a different strategy to implement an efficient Prolog System, the creation of specialized emulators on the fly. The proposed strategy was implemented and evaluated at YAP Prolog System, and the experimental evaluation showed interesting results.

ABSTRACT. Integration techniques for combining programs written in distinct language paradigms facilitate the implementation of specialised modules in the best language for their task. In the case of Java-Prolog integration, a known problem is the proper representation of references to Java objects on the Prolog side. To solve it adequately, multiple dimensions should be considered, including reference representation, opacity of the representation, identity preservation, reference life span, and scope of the inter-language conversion policies. This paper presents an approach that addresses all these dimensions, generalising and building on existing representation patterns of foreign references in Prolog, and taking inspiration from similar inter-language representation techniques found in other domains. Our approach maximises portability by making few assumptions about the Prolog engine interacting with Java (e.g., embedded or executed as an external process). We validate our work by extending JPC, an open-source integration library, with features supporting our approach.

ABSTRACT. Unification of logic variables instantly connects present and future observations of their value,independently of their location in the data areas of the runtime system. 

The paper extends this property to "interclausal logic variables'', an easy to implement Prolog extension  that supports instant globa information exchanges  without dynamic database updates.

We illustrate their usefulness with two of algorithms, graph coloring and minimum spanning tree. 

Implementations of interclausal variables  as source-level transformations and as abstract machine adaptations are given.

To address the need for globally visible chained transitions of logic variables we describe a DCG-based program transformation that extends the functionality of interclausal variables. 

ABSTRACT. In this paper, we study the framework of abductive logic programming extended with integrity constraints. For this framework, we introduce a new measure of the simplicity of an explanation in terms of its degree of arbitrariness. The more arbitrary the explanation the less appealing it is, with constrained explanations having no arbitrariness and so, being the preferred ones. In the paper, we study basic properties of constrained explanations. For the case when programs in abductive theories are stratified we establish results providing a detailed picture of the complexity of the problem to decide whether constrained explanations exist.

ABSTRACT. The belief bias effect is a phenomenon which occurs when we think that we judge an argument based on our reasoning, but are actually influenced by our beliefs and prior knowledge. Evans, Barston and Pollard carried out a psychological syllogistic reasoning task to prove this effect. Participants were asked whether they would accept or reject a given syllogism. We discuss one specific case which is commonly assumed to be
believable but which is actually not logically valid. By introducing abnormalities, abduction and background knowledge, we adequately model this case under the weak completion semantics. Our formalization reveals new questions about possible extensions in abductive reasoning. For instance, observations and their explanations might include some relevant prior abductive contextual information concerning some side-effect or leading to a contestable or refutable side-effect. A weaker notion indicates the support of some relevant consequences by a prior abductive context. Yet another definition describes jointly supported relevant consequences, which captures the idea of two observations containing mutually supportive side-effects. Though motivated with and exemplified by the running psychology application, the various new general abductive context definitions are introduced here and given a declarative semantics for the first time, and have a much wider scope of application. Inspection points, a concept introduced by Pereira and Pinto, allows us to express these definitions syntactically and intertwine them into an operational semantics.

ABSTRACT. Our understanding of the notion "dynamic system" is a rather broad one: such a system has states, which can change over time. Ontologies are used to describe the states of the system, possibly in an incomplete way. Monitoring is then concerned with deciding whether some run of the system or all of its runs satisfy a certain property, which can be expressed by a formula of an appropriate temporal logic. We consider different instances of this broad framework, which can roughly be classified into two cases. In one instance, the system is assumed to be a black box, whose inner working is not known, but whose states can be (partially) observed during a run of the system. In the second instance, one has (partial) knowledge about the inner working of the system, which provides information on which runs of the system are possible.

In this talk, we will review some of our recent research that investigates different instances of this general framework of ontology-based monitoring of dynamic systems. We will also sketch possible extensions towards probabilistic reasoning and the integration of mathematical modelling of dynamical systems.

ABSTRACT. The Vienna Circle of Logical Empiricism, which was part of the intellectual movement of Central European philosophy of science, is certainly one of the most important currents in the emergence of modern philosophy of science. Apart from this uncontested historical fact there remains the question of the direct and indirect influence, reception and topicality of this scientific community in contemporary philosophy of science in general as well as in the philosophy of the individual sciences, including the formal and social sciences. 

First, I will characterize the road from the Schlick-Circle to contemporary philosophy of science. Second, I will refer to "the present situation in the philosophy of science" by identifying relevant impacts, findings, and unfinished projects since the classical Vienna Circle. Third, I will address some specific European features of this globalized philosophical tradition up to the present, and outline future perspectives after the linguistic, historical and pragmatic turns – looking back to the "received view", or standard view of the Vienna Circle.

ABSTRACT. The aim of the FLoC Olympic Games is to start a tradition in the spirit of the ancient Olympic Games, a Panhellenic sport festival held every four years in the sanctuary of Olympia in Greece, this time in the scientific community of computational logic. Every four years, as part of the Federated Logic Conference, the Games will gather together all the challenging disciplines from a variety of computational logic in the form of the solver competitions.

At the Award Ceremonies, the competition organizers will have the opportunity to present their competitions to the public and give away special prizes, the prestigious Kurt Gödel medals, to their successful competitors. This reinforces the main goal of the FLoC Olympic Games, that is, to facilitate the visibility of the competitions associated with the conferences and workshops of the Federated Logic Conference during the Vienna Summer of Logic.

This award ceremony will host the

• Fifth Answer Set Programming Competition (ASPCOMP 2014);
• The 7th IJCAR ATP System Competition (CASC-J7);
• Hardware Model Checking Competition (HWMCC 2014);
• OWL Reasoner Evaluation (ORE 2014);
• Satisfiability Modulo Theories solver competition (SMT-COMP 2014);
• Competition on Software Verification (SV-COMP 2014);
• Syntax-Guided Synthesis Competition (SyGuS-COMP 2014);
• Synthesis Competition (SYNTCOMP 2014); and
• Termination Competition (termCOMP 2014).

ABSTRACT. Werner "Jimmy" DePauli-Schimanovich is being honored for his contributions to Gödel research, for his efforts towards re-establishing Vienna as a center of logic in the second half of the past century, and for extending the outreach of formal logic and logical thinking to other disciplines. The books about Gödel he authored, co-authored, or edited contain precious contributions of historical, philosophical, and mathematical value. His film on Gödel, and related articles and TV testimonials, attracted the general public to Gödel and his work. Moreover, DePauli-Schimanovich has unceasingly and successfully fought to re-establish logic in Vienna. He has inspired and encouraged a large number of students and young researchers, has organised meetings and social gatherings, and has created an intellectual home for scholars of logic. His activities significantly contributed to filling the intellectual vacuum in logic research that had developed in Austria in the years 1938–1945 and well into the post-war period. He was a main initiator and co-founder of the International Kurt Gödel Society. Jimmy’s research in logic involved criticism of current axiomatisations of set theory and development of new systems of naïve set theory. In informatics, DePauli-Schimanovich was co-founder and co-organiser of EuroCAST, a conference series on computer-assisted systems theory meeting alternatively in Vienna and Las Palmas, Gran Canaria. Finally, Jimmy has furthered implementation of logical ideas in disparate fields such as mechanical engineering, automated game playing, urban planning, and by inventing a number of logical games.

ABSTRACT. Zhang Mingyi is a pioneer in Artificial Intelligence and Knowledge Representation in China. He has built up a school of non-monotonic logic in Guiyang and has fostered the exchange between Chinese and Western scientists. He has contributed a large number of results on various forms of non-monotonic reasoning, including default logic, answer set programming, and belief revision. In particular, as early as 1992, he has provided important characterizations of various forms of default logic that paved the way for clarifying their computational properties and for developing algorithms for default reasoning.  Jointly with collaborators, he proposed a characterization of answer sets based on sets of generating rules, and introduced the concept of first-order loop formulas to relate answer set programming to classical logic. Other important results relate to theory revision (for example, the proof of the existence and uniqueness of finest splitting of Horn formulae) and to normal forms for Gödel logics. Many of Zhang Mingyi's former students have become internationally respected researchers.

ABSTRACT. The Free University of Bozen-Bolzano, the Technische Universität Dresden, the Universidade Nova de Lisboa, the Universidad Politécnica de Madrid (until 2010), the Technische Universität Wien, and Australia's Information Communications Technology Research Centre of Excellence (since 2007) are jointly running the European Master's Program in Computational Logic (EMCL) since 2004. The program is supported by the European Union within Erasmus Mundus and Eramsus+. So far, more than 100 students from 39 different countries have successfully completed the distributed master's program with a double or joint degree.

For the first time, the partner institutions are announcing the EMCL Distinguished Alumni Award for outstanding contributions of EMCL graduates to the field of Computational Logic.

http://www.emcl-study.eu/