Uncertain information is being taken into account in an increasing number of application fields. In the meantime, abduction has been proved a powerful tool for handling hypothetical reasoning and incomplete knowledge. Probabilistic logical models are a suitable framework to handle uncertain information, and in the last decade many probabilistic logical languages have been proposed, as well as inference and learning systems for them. In the realm of Abductive Logic Programming (ALP), a variety of proof procedures have been defined as well. In this paper, we consider a richer logic language, coping with probabilistic abduction with variables. In particular, we consider an ALP program enriched with integrity constraints à la IFF, possibly annotated with a probability value. We first present the overall abductive language and its semantics according to the Distribution Semantics. We then introduce a proof procedure, obtained by extending one previously presented, and prove its soundness and completeness.

Graph transformation systems (GTS) and constraint handling rules (CHR) are non-deterministic rule-based state transition systems. CHR is well known for its powerful confluence and program equivalence analyses, for which we provide the basis in this work to apply them to GTS. We give a sound and complete embedding of GTS in CHR, investigate confluence of an embedded GTS and provide a program equivalence analysis for GTS via the embedding. The results confirm the suitability of CHR-based program analyses for other formalisms embedded in CHR.

Answer Set Programming (ASP) is a well-known declarative formalism in logic programming. Efficient implementations made it possible to apply ASP in many scenarios, ranging from deductive databases applications to the solution of hard combinatorial problems. State-of-the-art ASP systems are based on the traditional ground&solve approach and are general-purpose implementations, i.e., they are essentially built once for any kind of input program. In this paper, we propose an extended architecture for ASP systems, in which parts of the input program are compiled into an ad-hoc evaluation algorithm (i.e., we obtain a specific binary for a given program), and might not be subject to the grounding step. To this end, we identify a condition that allows the compilation of a sub-program, and present the related partial compilation technique. Importantly, we have implemented the new approach on top of a well-known ASP solver and conducted an experimental analysis on publicly-available benchmarks. Results show that our compilation-based approach improves on the state of the art in various scenarios, including cases in which the input program is stratified or the grounding blow-up makes the evaluation unpractical with traditional ASP systems.

Traditional approaches to automatic AND-parallelization of logic programs rely on some static analysis to identify independent goals that can be safely and efficiently run in parallel in any possible execution. In this paper, we present a novel technique for generating annotations for independent AND-parallelism that is based on partial evaluation. Basically, we augment a simple partial evaluation procedure with (run-time) groundness and variable sharing information so that parallel conjunctions are added to the residual clauses when the conditions for independence are met. In contrast to previous approaches, our partial evaluator is able to transform the source program in order to expose more opportunities for parallelism. To the best of our knowledge, we present the first approach to a parallelizing partial evaluator.

We address the problem of belief revision of logic programs (LPs), i.e., how to incorporate to a LP P a new LP Q. Based on the structure of SE interpretations, Delgrande et al. (2008. Proc. of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR'08), 411–421; 2013b. Proc. of the 12th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'13), 264–276) adapted the well-known AGM framework (Alchourrón et al. 1985. Journal of Symbolic Logic 50, 2, 510–530) to LP revision. They identified the rational behavior of LP revision and introduced some specific operators. In this paper, a constructive characterization of all rational LP revision operators is given in terms of orderings over propositional interpretations with some further conditions specific to SE interpretations. It provides an intuitive, complete procedure for the construction of all rational LP revision operators and makes easier the comprehension of their semantic and computational properties. We give a particular consideration to LPs of very general form, i.e., the generalized logic programs (GLPs). We show that every rational GLP revision operator is derived from a propositional revision operator satisfying the original AGM postulates. Interestingly, the further conditions specific to GLP revision are independent from the propositional revision operator on which a GLP revision operator is based. Taking advantage of our characterization result, we embed the GLP revision operators into structures of Boolean lattices, that allow us to bring to light some potential weaknesses in the adapted AGM postulates. To illustrate our claim, we introduce and characterize axiomatically two specific classes of (rational) GLP revision operators which arguably have a drastic behavior. We additionally consider two more restricted forms of LPs, i.e., the disjunctive logic programs (DLPs) and the normal logic programs (NLPs) and adapt our characterization result to disjunctive logic program and normal logic program revision operators.

We show that database schema validation and update processing problems such as view updating, materialized view maintenance, integrity constraint checking, integrity constraint maintenance or condition monitoring can be classified as problems of either abductive or deductive nature, according to the reasoning paradigm that inherently suites them. This is done by performing abductive and deductive reasoning on the event rules (Olivé 1991), a set of rules that define the difference between consecutive database states. In this way, we show that it is possible to provide methods able to deal with all these problems as a whole. We also show how some existing general deductive and abductive procedures may be used to reason on the event rules. In this way, we show that these procedures can deal with all database schema validation and update processing problems considered in this paper.

U-Datalog has been developed with the aim of providing a set-oriented logical update language, guaranteeing update parallelism in the context of a Datalog-like language. In U-Datalog, updates are expressed by introducing constraints (+p(X), to denote insertion, and −p(X), to denote deletion) inside Datalog rules. A U-Datalog program can be interpreted as a CLP program. In this framework, a set of updates (constraints) is satisfiable if it does not represent an inconsistent theory, that is, it does not require the insertion and the deletion of the same fact. This approach resembles a very simple form of negation. However, on the other hand, U-Datalog does not provide any mechanism to explicitly deal with negative information, resulting in a language with limited expressive power. In this paper, we provide a semantics, based on stratification, handling the use of negated atoms in U-Datalog programs, and we show which problems arise in defining a compositional semantics.

Programmers currently enjoy access to a very high number of code repositories and libraries of ever increasing size. The ensuing potential for reuse is however hampered by the fact that searching within all this code becomes an increasingly difficult task. Most code search engines are based on syntactic techniques such as signature matching or keyword extraction. However, these techniques are inaccurate (because they basically rely on documentation) and at the same time do not offer very expressive code query languages. We propose a novel approach that focuses on querying for semantic characteristics of code obtained automatically from the code itself. Program units are pre-processed using static analysis techniques, based on abstract interpretation, obtaining safe semantic approximations. A novel, assertion-based code query language is used to express desired semantic characteristics of the code as partial specifications. Relevant code is found by comparing such partial specifications with the inferred semantics for program elements. Our approach is fully automatic and does not rely on user annotations or documentation. It is more powerful and flexible than signature matching because it is parametric on the abstract domain and properties, and does not require type definitions. Also, it reasons with relations between properties, such as implication and abstraction, rather than just equality. It is also more resilient to syntactic code differences. We describe the approach and report on a prototype implementation within the Ciao system.

Coding standards and good practices are fundamental to a disciplined approach to software projects irrespective of programing languages being employed. Prolog programing can benefit from such an approach, perhaps more than programing in other languages. Despite this, no widely accepted standards and practices seem to have emerged till now. The present paper is a first step toward filling this void: It provides immediate guidelines for code layout, naming conventions, documentation, proper use of Prolog features, program development, debugging, and testing. Presented with each guideline is its rationale and, where sensible options exist, illustrations of the relative pros and cons for each alternative. A coding standard should always be selected on a per-project basis, based on a host of issues pertinent to any given programing project; for this reason the paper goes beyond the mere provision of normative guidelines by discussing key factors and important criteria that should be taken into account when deciding on a full-fledged coding standard for the project.

Metabolic networks play a crucial role in biology since they capture all chemical reactions in an organism. While there are networks of high quality for many model organisms, networks for less studied organisms are often of poor quality and suffer from incompleteness. To this end, we introduced in previous work an answer set programming (ASP)-based approach to metabolic network completion. Although this qualitative approach allows for restoring moderately degraded networks, it fails to restore highly degraded ones. This is because it ignores quantitative constraints capturing reaction rates. To address this problem, we propose a hybrid approach to metabolic network completion that integrates our qualitative ASP approach with quantitative means for capturing reaction rates. We begin by formally reconciling existing stoichiometric and topological approaches to network completion in a unified formalism. With it, we develop a hybrid ASP encoding and rely upon the theory reasoning capacities of the ASP system clingo for solving the resulting logic program with linear constraints over reals. We empirically evaluate our approach by means of the metabolic network of Escherichia coli. Our analysis shows that our novel approach yields greatly superior results than obtainable from purely qualitative or quantitative approaches.

The paper provides a framework for the verification of business processes, based on an extension of answer set programming (ASP) with temporal logic and constraints. The framework allows to capture expressive fluent annotations as well as data awareness in a uniform way. It allows for a declarative specification of a business process but also for encoding processes specified in conventional workflow languages. Verification of temporal properties of a business process, including verification of compliance to business rules, is performed by bounded model checking techniques in Answer Set Programming, extended with constraint solving for dealing with conditions on numeric data.

In recent work we defined resource-based answer set semantics, which is an extension to answer set semantics stemming from the study of its relationship with linear logic. In fact, the name of the new semantics comes from the fact that in the linear-logic formulation every literal (including negative ones) were considered as a resource. In this paper, we propose a query-answering procedure reminiscent of Prolog for answer set programs under this extended semantics as an extension of XSB-resolution for logic programs with negation.1 We prove formal properties of the proposed procedure. Under consideration for acceptance in TPLP.

We describe the BinProlog system's compilation technology, runtime system and its extensions supporting first-class Logic Engines while providing a short history of its development, details of some of its newer re-implementations as well as an overview of the most important architectural choices involved in their design. With focus on its differences with conventional Warren Abstract Machine (WAM) implementations, we explain key details of BinProlog's compilation technique, which replaces the WAM with a simplified continuation passing runtime system (the “BinWAM”), based on a mapping of full Prolog to binary logic programs. This is followed by a description of a term compression technique using a “tag-on-data” representation. Later derivatives, the Java-based Jinni Prolog compiler and the recently developed Lean Prolog system refine the BinProlog architecture with first-class Logic Engines, made generic through the use of an Interactor interface. An overview of their applications with focus on the ability to express at source level a wide variety of Prolog built-ins and extensions covers these newer developments.

We consider an extension of logic programs, called ω-programs, that can be used to define predicates over infinite lists. ω-programs allow us to specify properties of the infinite behavior of reactive systems and, in general, properties of infinite sequences of events. The semantics of ω-programs is an extension of the perfect model semantics. We present variants of the familiar unfold/fold rules which can be used for transforming ω-programs. We show that these new rules are correct, that is, their application preserves the perfect model semantics. Then we outline a general methodology based on program transformation for verifying properties of ω-programs. We demonstrate the power of our transformation-based verification methodology by proving some properties of Büchi automata and ω-regular languages.

Answer set programming (ASP) emerged in the late 1990s as a paradigm for knowledge representation and reasoning. The attractiveness of ASP builds on an expressive high-level modeling language along with the availability of powerful off-the-shelf solving systems. While the utility of incorporating aggregate expressions in the modeling language has been realized almost simultaneously with the inception of the first ASP solving systems, a general semantics of aggregates and its efficient implementation have been long-standing challenges. Aggregates have been proposed and widely used in database systems, and also in the deductive database language Datalog, which is one of the main precursors of ASP. The use of aggregates was, however, still restricted in Datalog (by either disallowing recursion or only allowing monotone aggregates), while several ways to integrate unrestricted aggregates evolved in the context of ASP. In this survey, we pick up at this point of development by presenting and comparing the main aggregate semantics that have been proposed for propositional ASP programs. We highlight crucial properties such as computational complexity and expressive power, and outline the capabilities and limitations of different approaches by illustrative examples.

This paper introduces GLINTS, a graphical tool for exploring variant narrowing computations in Maude. The most recent version of Maude, version 2.7.1, provides quite sophisticated unification features, including order-sorted equational unification for convergent theories modulo axioms such as associativity, commutativity, and identity. This novel equational unification relies on built-in generation of the set of variants of a term t, i.e., the canonical form of tσ for a computed substitution σ. Variant generation relies on a novel narrowing strategy called folding variant narrowing that opens up new applications in formal reasoning, theorem proving, testing, protocol analysis, and model checking, especially when the theory satisfies the finite variant property, i.e., there is a finite number of most general variants for every term in the theory. However, variant narrowing computations can be extremely involved and are simply presented in text format by Maude, often being too heavy to be debugged or even understood. The GLINTS system provides support for (i) determining whether a given theory satisfies the finite variant property, (ii) thoroughly exploring variant narrowing computations, (iii) automatic checking of node embedding and closedness modulo axioms, and (iv) querying and inspecting selected parts of the variant trees.

A recent framework of relativized hyperequivalence of programs offers a unifying generalization of strong and uniform equivalence. It seems to be especially well suited for applications in program optimization and modular programming due to its flexibility that allows us to restrict, independently of each other, the head and body alphabets in context programs. We study relativized hyperequivalence for the three semantics of logic programs given by stable, supported, and supported minimal models. For each semantics, we identify four types of contexts, depending on whether the head and body alphabets are given directly or as the complement of a given set. Hyperequivalence relative to contexts where the head and body alphabets are specified directly has been studied before. In this paper, we establish the complexity of deciding relativized hyperequivalence with respect to the three other types of context programs.

In order to automatically infer the resource consumption of programs, analyzers track how data sizes change along program’s execution. Typically, analyzers measure the sizes of data by applying norms which are mappings from data to natural numbers that represent the sizes of the corresponding data. When norms are defined by taking type information into account, they are named typed-norms. This article presents a transformational approach to resource analysis with typed-norms that are inferred by a data-flow analysis. The analysis is based on a transformation of the program into an intermediate abstract program in which each variable is abstracted with respect to all considered norms which are valid for its type. We also present the data-flow analysis to automatically infer the required, useful, typed-norms from programs. Our analysis is formalized on a simple rule-based representation to which programs written in different programming paradigms (e.g., functional, logic, and imperative) can be automatically translated. Experimental results on standard benchmarks used by other type-based analyzers show that our approach is both efficient and accurate in practice.

FO(·)IDP3 extends first-order logic with inductive definitions, partial functions, types and aggregates. Its model generator IDP3 first grounds the theory and then uses search to find the models. The grounder uses Lifted Unit Propagation (LUP) to reduce the size of the groundings of problem specifications in IDP3. LUP is in general very effective, but performs poorly on definitions of predicates whose two-valued interpretation can be computed from data in the input structure. To solve this problem, a preprocessing step is introduced that converts such definitions to Prolog code and uses XSB Prolog to compute their interpretation. The interpretation of these predicates is then added to the input structure, their definitions are removed from the theory and further processing is done by the standard IDP3 system. Experimental results show the effectiveness of our method.

In this paper, we study an extension of the stable model semantics for disjunctive logic programs where each true atom in a model is associated with an algebraic expression (in terms of rule labels) that represents its justifications. As in our previous work for non-disjunctive programs, these justifications are obtained in a purely semantic way, by algebraic operations (product, addition and application) on a lattice of causal values. Our new definition extends the concept of causal stable model to disjunctive logic programs and satisfies that each (standard) stable model corresponds to a disjoint class of causal stable models sharing the same truth assignments, but possibly varying the obtained explanations. We provide a pair of illustrative examples showing the behaviour of the new semantics and discuss the need of introducing a new type of rule, which we call causal-choice. This type of rule intuitively captures the idea of “A may cause B” and, when causal information is disregarded, amounts to a usual choice rule under the standard stable model semantics.