We present Web-STAR, an online platform for story understanding built on top of the STAR reasoning engine for STory comprehension through ARgumentation. The platform includes a web-based integrated development environment, integration with the STAR system, and a web service infrastructure to support integration with other systems that rely on story understanding functionality to complete their tasks. The platform also delivers a number of “social” features, including a community repository for public story sharing with a built-in commenting system, and tools for collaborative story editing that can be used for team development projects and for educational purposes.

Cooperation among constraint solvers is difficult because different solving paradigms have different theoretical foundations. Recent works have shown that abstract interpretation can provide a unifying theory for various constraint solvers. In particular, it relies on abstract domains which capture constraint languages as ordered structures. The key insight of this paper is viewing cooperation schemes as abstract domains combinations. We propose a modular framework in which solvers and cooperation schemes can be seamlessly added and combined. This differs from existing approaches such as SMT where the cooperation scheme is usually fixed (e.g., Nelson-Oppen). We contribute to two new cooperation schemes: (i) interval propagators completion that allows abstract domains to exchange bound constraints, and (ii) delayed product which exchanges over-approximations of constraints between two abstract domains. Moreover, the delayed product is based on delayed goal of logic programming, and it shows that abstract domains can also capture control aspects of constraint solving. Finally, to achieve modularity, we propose the shared product to combine abstract domains and cooperation schemes. Our approach has been fully implemented, and we provide various examples on the flexible job shop scheduling problem.

Control flow compilation is a hybrid between classical WAM compilation and meta-call, limited to the compilation of non-recursive clause bodies. This approach is used successfully for the execution of dynamically generated queries in an inductive logic programming setting (ILP). Control flow compilation reduces compilation times up to an order of magnitude, without slowing down execution. A lazy variant of control flow compilation is also presented. By compiling code by need, it removes the overhead of compiling unreached code (a frequent phenomenon in practical ILP settings), and thus reduces the size of the compiled code. Both dynamic compilation approaches have been implemented and were combined with query packs, an efficient ILP execution mechanism. It turns out that locality of data and code is important for performance. The experiments reported in the paper show that lazy control flow compilation is superior in both artificial and real life settings.

The infinitary propositional logic of here-and-there is important for the theory of answer set programming in view of its relation to strongly equivalent transformations of logic programs. We know a formal system axiomatizing this logic exists, but a proof in that system may include infinitely many formulas. In this note we describe a relationship between the validity of infinitary formulas in the logic of here-and-there and the provability of formulas in some finite deductive systems. This relationship allows us to use finite proofs to justify the validity of infinitary formulas.

The runtime system of dynamic languages such as Prolog or Lisp and their derivatives contain a symbol table, in Prolog often called the atom table. A simple dynamically resizing hash-table used to be an adequate way to implement this table. As Prolog becomes fashionable for 24 × 7 server processes we need to deal with atom garbage collection and concurrent access to the atom table. Classical lock-based implementations to ensure consistency of the atom table scale poorly and a stop-the-world approach to implement atom garbage collection quickly becomes a bottle-neck, making Prolog unsuitable for soft real-time applications. In this article we describe a novel implementation for the atom table using lock-free techniques where the atom-table remains accessible even during atom garbage collection. Relying only on CAS (Compare And Swap) and not on external libraries, the implementation is straightforward and portable.

This paper investigates the relationship between the Logical Algorithms (LA) language of Ganzinger and McAllester and Constraint Handling Rules (CHR). We present a translation schema from LA to CHRrp: CHR with rule priorities, and show that the meta-complexity theorem for LA can be applied to a subset of CHRrp via inverse translation. Inspired by the high-level implementation proposal for Logical Algorithm by Ganzinger and McAllester and based on a new scheduling algorithm, we propose an alternative implementation for CHRrp that gives strong complexity guarantees and results in a new and accurate meta-complexity theorem for CHRrp. It is furthermore shown that the translation from Logical Algorithms to CHRrp combined with the new CHRrp implementation satisfies the required complexity for the Logical Algorithms meta-complexity result to hold.

Answer Set Programming (ASP) is a well-established formalism for logic programming. Problem solving in ASP requires to write an ASP program whose answers sets correspond to solutions. Albeit the non-existence of answer sets for some ASP programs can be considered as a modeling feature, it turns out to be a weakness in many other cases, and especially for query answering. Paracoherent answer set semantics extend the classical semantics of ASP to draw meaningful conclusions also from incoherent programs, with the result of increasing the range of applications of ASP. State of the art implementations of paracoherent ASP adopt the semi-equilibrium semantics, but cannot be lifted straightforwardly to compute efficiently the (better) split semi-equilibrium semantics that discards undesirable semi-equilibrium models. In this paper an efficient evaluation technique for computing a split semi-equilibrium model is presented. An experiment on hard benchmarks shows that better paracoherent answer sets can be computed consuming less computational resources than existing methods.

Approximation fixpoint theory (AFT) is an abstract and general algebraic framework for studying the semantics of non-monotonic logics. In recent work, AFT was generalized to non-deterministic operators, that is, operators whose range are sets of elements rather than single elements. In this paper, we make three further contributions to non-deterministic AFT: (1) we define and study ultimate approximations of non-deterministic operators, (2) we give an algebraic formulation of the semi-equilibrium semantics by Amendola et al., and (3) we generalize the characterizations of disjunctive logic programs to disjunctive logic programs with aggregates.

Declarative languages offer unprecedented opportunities for the use of parallelism to speed up execution. A declarative language, being not procedural, removes the need to perform operations in a strict order and reduces the number of dependencies among operations, thus opening the doors for concurrent execution. The potential for transparent exploitation of parallelism in logic programming emerged almost immediately with the birth of the paradigm (Pollard 1981).

Many practical problems can be understood as the search for a state of affairs that extends a fixed partial state of affairs, the environment, while satisfying certain conditions that are formally specified. Such problems are found in, for example, engineering, law or economics. We study this class of problems in a context where some of the relevant information about the environment is not known by the user at the start of the search. During the search, the user may consider tentative solutions that make implicit hypotheses about these unknowns. To ensure that the solution is appropriate, these hypotheses must be verified by observing the environment. Furthermore, we assume that, in addition to knowledge of what constitutes a solution, knowledge of general laws of the environment is also present. We formally define partial solutions with enough verified facts to guarantee the existence of complete and appropriate solutions. Additionally, we propose an interactive system to assist the user in their search by determining (1) which hypotheses implicit in a tentative solution must be verified in the environment, and (2) which observations can bring useful information for the search. We present an efficient method to over-approximate the set of relevant information, and evaluate our implementation.

Theory of stable models is the mathematical basis of answer set programming. Several results in that theory refer to the concept of the positive dependency graph of a logic program. We describe a modification of that concept and show that the new understanding of positive dependency makes it possible to strengthen some of these results.

Fairness in machine learning is of considerable interest in recent years owing to the propensity of algorithms trained on historical data to amplify and perpetuate historical biases. In this paper, we argue for a formal reconstruction of fairness definitions, not so much to replace existing definitions but to ground their application in an epistemic setting and allow for rich environmental modeling. Consequently we look into three notions: fairness through unawareness, demographic parity and counterfactual fairness, and formalize these in the epistemic situation calculus.

Tau Prolog is a client-side Prolog interpreter fully implemented in JavaScript, which aims at implementing the ISO Prolog Standard. Tau Prolog has been developed to be used with either Node.js or a browser seamlessly, and therefore, it has been developed following a non-blocking, callback-based approach to avoid blocking web browsers. Taking the best from JavaScript and Prolog, Tau Prolog allows the programmer to handle browser events and manipulate the Document Object Model (DOM) of a web using Prolog predicates. In this paper we describe the architecture of Tau Prolog and its main packages for interacting with the Web, and we present its programming environment.

Cloud computing refers to maximizing efficiency by sharing computational and storage resources, while data-parallel systems exploit the resources available in the cloud to perform parallel transformations over large amounts of data. In the same line, considerable emphasis has been recently given to two apparently disjoint research topics: data-parallel, and eventually consistent, distributed systems. Declarative networking has been recently proposed to ease the task of programming in the cloud, by allowing the programmer to express only the desired result and leave the implementation details to the responsibility of the run-time system. In this context, we deem it appropriate to propose a study on a logic-programming-based computational model for eventually consistent, data-parallel systems, the keystone of which is provided by the recent finding that the class of programs that can be computed in an eventually consistent, coordination-free way is that of monotonic programs. This principle is called Consistency and Logical Monotonicity (CALM) and has been proven by Ameloot et al. for distributed, asynchronous settings. We advocate that CALM should be employed as a basic theoretical tool also for data-parallel systems, wherein computation usually proceeds synchronously in rounds and where communication is assumed to be reliable. We deem this problem relevant and interesting, especially for what concerns parallel dataflow optimizations. Nowadays, we are in fact witnessing an increasing concern about understanding which properties distinguish synchronous from asynchronous parallel processing, and when the latter can replace the former. It is general opinion that coordination-freedom can be seen as a major discriminant factor. In this work, we make the case that the current form of CALM does not hold in general for data-parallel systems, and show how, using novel techniques, the satisfiability of the CALM principle can still be obtained although just for the subclass of programs called connected monotonic queries. We complete the study with considerations on the relationships between our model and the one employed by Ameloot et al., showing that our techniques subsume the latter when the synchronization constraints imposed on the system are loosened.

Assurance cases offer a structured way to present arguments and evidence for certification of systems where safety and security are critical. However, creating and evaluating these assurance cases can be complex and challenging, even for systems of moderate complexity. Therefore, there is a growing need to develop new automation methods for these tasks. While most existing assurance case tools focus on automating structural aspects, they lack the ability to fully assess the semantic coherence and correctness of the assurance arguments.

In prior work, we introduced the Assurance 2.0 framework that prioritizes the reasoning process, evidence utilization, and explicit delineation of counter-claims (defeaters) and counter-evidence. In this paper, we present our approach to enhancing Assurance 2.0 with semantic rule-based analysis capabilities using common-sense reasoning and answer set programming solvers, specifically s(CASP). By employing these analysis techniques, we examine the unique semantic aspects of assurance cases, such as logical consistency, adequacy, indefeasibility, etc. The application of these analyses provides both system developers and evaluators with increased confidence about the assurance case.

In this note, we introduce the notion of support graph to define explanations for any model of a logic program. An explanation is an acyclic support graph that, for each true atom in the model, induces a proof in terms of program rules represented by labels. A classical model may have zero, one or several explanations: when it has at least one, it is called a justified model. We prove that all stable models are justified, whereas, for disjunctive programs, some justified models may not be stable. We also provide a meta-programming encoding in Answer Set Programming that generates the explanations for a given stable model of some program. We prove that the encoding is sound and complete, that is, there is a one-to-one correspondence between each answer set of the encoding and each explanation for the original stable model.

Program transformation is an appealing technique which allows to improve run-time efficiency, space-consumption, and more generally to optimize a given program. Essentially, it consists of a sequence of syntactic program manipulations which preserves some kind of semantic equivalence. Unfolding is one of the basic operations used by most program transformation systems and consists of the replacement of a procedure call by its definition. While there is a large body of literature on the transformation and unfolding of sequential programs, very few papers have addressed this issue for concurrent languages. This paper defines an unfolding system for Constraint Handling Rules programs. We define an unfolding rule, show its correctness and discuss some conditions that can be used to delete an unfolded rule while preserving the program meaning. We also prove that, under some suitable conditions, confluence and termination are preserved by the above transformation.

A recent trend in object-oriented programming languages is the use of access permissions (APs) as an abstraction for controlling concurrent executions of programs. The use of AP source code annotations defines a protocol specifying how object references can access the mutable state of objects. Although the use of APs simplifies the task of writing concurrent code, an unsystematic use of them can lead to subtle problems. This paper presents a declarative interpretation of APs as linear concurrent constraint programs (lcc). We represent APs as constraints (i.e., formulas in logic) in an underlying constraint system whose entailment relation models the transformation rules of APs. Moreover, we use processes in lcc to model the dependencies imposed by APs, thus allowing the faithful representation of their flow in the program. We verify relevant properties about AP programs by taking advantage of the interpretation of lcc processes as formulas in Girard's intuitionistic linear logic (ILL). Properties include deadlock detection, program correctness (whether programs adhere to their AP specifications or not), and the ability of methods to run concurrently. By relying on a focusing discipline for ILL, we provide a complexity measure for proofs of the above-mentioned properties. The effectiveness of our verification techniques is demonstrated by implementing the Alcove tool that includes an animator and a verifier. The former executes the lcc model, observing the flow of APs, and quickly finding inconsistencies of the APs vis-à-vis the implementation. The latter is an automatic theorem prover based on ILL.