Search

Symmetry in combinatorial problems is an extensively studied topic. We continue this research in the context of model expansion problems, with the aim of automating the workflow of detecting and breaking symmetry. We focus on local domain symmetry, which is induced by permutations of domain elements, and which can be detected on a first-order level. As such, our work is a continuation of the symmetry exploitation techniques of model generation systems, while it differs from more recent symmetry breaking techniques in answer set programming which detect symmetry on ground programs. Our main contributions are sufficient conditions for symmetry of model expansion problems, the identification of local domain interchangeability, which can often be broken completely, and efficient symmetry detection algorithms for both local domain interchangeability as well as local domain symmetry in general. Our approach is implemented in the model expansion system IDP, and we present experimental results showcasing the strong and weak points of our approach compared to sbass, a symmetry breaking technique for answer set programming. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

Tabling is a powerful resolution mechanism for logic programs that captures their least fixed point semantics more faithfully than plain Prolog. In many tabling applications, we are not interested in the set of all answers to a goal, but only require an aggregation of those answers. Several works have studied efficient techniques, such as lattice-based answer subsumption and mode-directed tabling, to do so for various forms of aggregation.While much attention has been paid to expressivity and efficient implementation of the different approaches, soundness has not been considered. This paper shows that the different implementations indeed fail to produce least fixed points for some programs. As a remedy, we provide a formal framework that generalises the existing approaches and we establish a soundness criterion that explains for which programs the approach is sound. [ABSTRACT FROM AUTHOR]

We present an extension of Logic Programming (under stable models semantics) that, not only allows concluding whether a true atom is a cause of another atom, but also deriving new conclusions from these causal-effect relations. This is expressive enough to capture informal rules like “if some agent's actions have been necessary to cause an event E then conclude atom caused(, E),” something that, to the best of our knowledge, had not been formalised in the literature. To this aim, we start from a first attempt that proposed extending the syntax of logic programs with so-called causal literals. These causal literals are expressions that can be used in rule bodies and allow inspecting the derivation of some atom A in the program with respect to some query function ψ. Depending on how these query functions are defined, we can model different types of causal relations such as sufficient, necessary or contributory causes, for instance. The initial approach was specifically focused on monotonic query functions. This was enough to cover sufficient cause-effect relations but, unfortunately, necessary and contributory are essentially non-monotonic. In this work, we define a semantics for non-monotonic causal literals showing that, not only extends the stable model semantics for normal logic programs, but also preserves many of its usual desirable properties for the extended syntax. Using this new semantics, we provide precise definitions of necessary and contributory causal relations and briefly explain their behaviour on a pair of typical examples from the Knowledge Representation literature. [ABSTRACT FROM AUTHOR]

For some applications, standard resource analyses do not provide the information required. Such analyses estimate the total resource usage of a program (without executing it) as functions on input data sizes. However, some applications require knowing how such total resource usage is distributed over selected parts of a program. We propose a novel, general, and flexible framework for setting up cost equations/relations which can be instantiated for performing a wide range of resource usage analyses, including both static profiling and the inference of the standard notion of cost. We extend and generalize standard resource analysis techniques, so that the relations generated include additional Boolean control variables for switching on or off different terms in the relations, as required by the desired resource usage profile. We also instantiate our framework to perform static profiling of accumulated cost (also parameterized by input data sizes). Such information is much more useful to the software developer than the standard notion of cost: it identifies the parts of the program that have the greatest impact on the total program cost, and which therefore should be optimized first. We also report on an implementation of our framework within the CiaoPP system, and its instantiation for accumulated cost, and provide some experimental results. In addition to generality, our new method brings important advantages over our previous approach based on a program transformation, including support for non-deterministic programs, better and easier integration in the compiler, and higher efficiency. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

Modular logic programs provide a way of viewing logic programs as consisting of many independent, meaningful modules. This paper introduces first-order modular logic programs, which can capture the meaning of many answer set programs. We also introduce conservative extensions of such programs. This concept helps to identify strong relationships between modular programs as well as between traditional programs. We show how the notion of a conservative extension can be used to justify the common projection rewriting. [ABSTRACT FROM AUTHOR]

Management of chronic diseases such as chronic heart failure (CHF) is a major problem in health care. A standard approach followed by the medical community is to have a committee of experts develop guidelines that all physicians should follow. These guidelines typically consist of a series of complex rules that make recommendations based on a patient's information. Due to their complexity, often the guidelines are ignored or not complied with at all. It is not even clear whether it is humanly possible to follow these guidelines due to their length and complexity. For instance, for CHF, the guidelines run nearly eighty pages. In this paper we describe a physician-advisory system for CHF management that codes the entire set of clinical practice guidelines for CHF using answer set programming (ASP). Our approach is based on developing reasoning templates, that we call knowledge patterns, and using them to systemically code the clinical guidelines for CHF as ASP rules. Use of the knowledge patterns greatly facilitates the development of our system. Given a patient's medical information, our system generates a recommendation for treatment just as a human physician would, using the guidelines. Our system works even in the presence of incomplete information. [ABSTRACT FROM AUTHOR]

Answer set programming (ASP) is a well-established logic programming language that offers an intuitive, declarative syntax for problem solving. In its traditional application, a fixed ASP program for a given problem is designed and the actual instance of the problem is fed into the program as a set of facts. This approach typically results in programs with comparably short and simple rules. However, as is known from complexity analysis, such an approach limits the expressive power of ASP; in fact, an entire NP-check can be encoded into a single large rule body of bounded arity that performs both a guess and a check within the same rule. Here, we propose a novel paradigm for encoding hard problems in ASP by making explicit use of large rules which depend on the actual instance of the problem. We illustrate how this new encoding paradigm can be used, providing examples of problems from the first, second, and even third level of the polynomial hierarchy. As state-of-the-art solvers are tuned towards short rules, rule decomposition is a key technique in the practical realization of our approach. We also provide some preliminary benchmarks which indicate that giving up the convenient way of specifying a fixed program can lead to a significant speed-up. [ABSTRACT FROM AUTHOR]

In this paper we exploit Answer Set Programming (ASP) for reasoning in a rational extension SROEL (⊓,×)RT of the low complexity description logic SROEL(⊓, ×), which underlies the OWL EL ontology language. In the extended language, a typicality operator T is allowed to define concepts T(C) (typical C's) under a rational semantics. It has been proven that instance checking under rational entailment has a polynomial complexity. To strengthen rational entailment, in this paper we consider a minimal model semantics. We show that, for arbitrary SROEL(⊓,×)RT knowledge bases, instance checking under minimal entailment is ΠP2-complete. Relying on a Small Model result, where models correspond to answer sets of a suitable ASP encoding, we exploit Answer Set Preferences (and, in particular, the asprin framework) for reasoning under minimal entailment. [ABSTRACT FROM AUTHOR]

Pointer analysis is a fundamental static program analysis for computing the set of objects that an expression can refer to. Decades of research has gone into developing methods of varying precision and efficiency for pointer analysis for programs that use different language features, but determining precisely how efficient a particular method is has been a challenge in itself.For programs that use different language features, we consider methods for pointer analysis using Datalog and extensions to Datalog. When the rules are in Datalog, we present the calculation of precise time complexities from the rules using a new algorithm for decomposing rules for obtaining the best complexities. When extensions such as function symbols and universal quantification are used, we describe algorithms for efficiently implementing the extensions and the complexities of the algorithms. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

We present ABETS, an assertion-based, dynamic analyzer that helps diagnose errors in Maude programs. ABETS uses slicing to automatically create reduced versions of both a run's execution trace and executed program, reduced versions in which any information that is not relevant to the bug currently being diagnosed is removed. In addition, ABETS employs runtime assertion checking to automate the identification of bugs so that whenever an assertion is violated, the system automatically infers accurate slicing criteria from the failure. We summarize the main services provided by ABETS, which also include a novel assertion-based facility for program repair that generates suitable program fixes when a state invariant is violated. Finally, we provide an experimental evaluation that shows the performance and effectiveness of the system. [ABSTRACT FROM AUTHOR]

This paper presents CoreALMlib, an $\mathscr{ALM}$ library of commonsense knowledge about dynamic domains. The library was obtained by translating part of the Component Library (CLib) into the modular action language $\mathscr{ALM}$. CLib consists of general reusable and composable commonsense concepts, selected based on a thorough study of ontological and lexical resources. Our translation targets CLibstates (i.e., fluents) and actions. The resulting $\mathscr{ALM}$ library contains the descriptions of 123 action classes grouped into 43 reusable modules that are organized into a hierarchy. It is made available online and of interest to researchers in the action language, answer-set programming, and natural language understanding communities. We believe that our translation has two main advantages over its CLib counterpart: (i) it specifies axioms about actions in a more elaboration tolerant and readable way, and (ii) it can be seamlessly integrated with ASP reasoning algorithms (e.g., for planning and postdiction). In contrast, axioms are described in CLib using STRIPS-like operators, and CLib's inference engine cannot handle planning nor postdiction. [ABSTRACT FROM AUTHOR]

Standard answer set programming (ASP) targets at solving search problems from the first level of the polynomial time hierarchy (PH). Tackling search problems beyond NP using ASP is less straightforward. The class of disjunctive logic programs offers the most prominent way of reaching the second level of the PH, but encoding respective hard problems as disjunctive programs typically requires sophisticated techniques such as saturation or meta-interpretation. The application of such techniques easily leads to encodings that are inaccessible to non-experts. Furthermore, while disjunctive ASP solvers often rely on calls to a (co-)NP oracle, it may be difficult to detect from the input program where the oracle is being accessed. In other formalisms, such as Quantified Boolean Formulas (QBFs), the interface to the underlying oracle is more transparent as it is explicitly recorded in the quantifier prefix of a formula. On the other hand, ASP has advantages over QBFs from the modeling perspective. The rich high-level languages such as ASP-Core-2 offer a wide variety of primitives that enable concise and natural encodings of search problems. In this paper, we present a novel logic programming–based modeling paradigm that combines the best features of ASP and QBFs. We develop so-called combined logic programs in which oracles are directly cast as (normal) logic programs themselves. Recursive incarnations of this construction enable logic programming on arbitrarily high levels of the PH. We develop a proof-of-concept implementation for our new paradigm. [ABSTRACT FROM AUTHOR]

In recent years, several frameworks and systems have been proposed that extend Inductive Logic Programming (ILP) to the Answer Set Programming (ASP) paradigm. In ILP, examples must all be explained by a hypothesis together with a given background knowledge. In existing systems, the background knowledge is the same for all examples; however, examples may be context-dependent. This means that some examples should be explained in the context of some information, whereas others should be explained in different contexts. In this paper, we capture this notion and present a context-dependent extension of the Learning from Ordered Answer Sets framework. In this extension, contexts can be used to further structure the background knowledge. We then propose a new iterative algorithm, ILASP2i, which exploits this feature to scale up the existing ILASP2 system to learning tasks with large numbers of examples. We demonstrate the gain in scalability by applying both algorithms to various learning tasks. Our results show that, compared to ILASP2, the newly proposed ILASP2i system can be two orders of magnitude faster and use two orders of magnitude less memory, whilst preserving the same average accuracy. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

Word puzzles and the problem of their representations in logic languages have received considerable attention in the last decade (Ponnuru et al. 2004; Shapiro 2011; Baral and Dzifcak 2012; Schwitter 2013). Of special interest is the problem of generating such representations directly from natural language (NL) or controlled natural language (CNL). An interesting variation of this problem, and to the best of our knowledge, scarcely explored variation in this context, is when the input information is inconsistent. In such situations, the existing encodings of word puzzles produce inconsistent representations and break down. In this paper, we bring the well-known type of paraconsistent logics, called Annotated Predicate Calculus (APC) (Kifer and Lozinskii 1992), to bear on the problem. We introduce a new kind of non-monotonic semantics for APC, called consistency preferred stable models and argue that it makes APC into a suitable platform for dealing with inconsistency in word puzzles and, more generally, in NL sentences. We also devise a number of general principles to help the user choose among the different representations of NL sentences, which might seem equivalent but, in fact, behave differently when inconsistent information is taken into account. These principles can be incorporated into existing CNL translators, such as Attempto Controlled English (ACE) (Fuchs et al. 2008) and PENG Light (White and Schwitter 2009). Finally, we show that APC with the consistency preferred stable model semantics can be equivalently embedded in ASP with preferences over stable models, and we use this embedding to implement this version of APC in Clingo (Gebser et al. 2011) and its Asprin add-on (Brewka et al. 2015). [ABSTRACT FROM AUTHOR]

The definition of stable models for propositional formulas with infinite conjunctions and disjunctions can be used to describe the semantics of answer set programming languages. In this note, we enhance that definition by introducing a distinction between intensional and extensional atoms. The symmetric splitting theorem for first-order formulas is then extended to infinitary formulas and used to reason about infinitary definitions. [ABSTRACT FROM AUTHOR]

Recent work has provided delimited control for Prolog to dynamically manipulate the program control-flow, and to implement a wide range of control-flow and dataflow effects on top of. Unfortunately, delimited control is a rather primitive language feature that is not easy to use.As a remedy, this work introduces algebraic effect handlers for Prolog, as a high-level and structured way of defining new side-effects in a modular fashion. We illustrate the expressive power of the feature and provide an implementation by means of elaboration into the delimited control primitives.The latter add a non-negligible performance overhead when used extensively. To address this issue, we present an optimised compilation approach that combines partial evaluation with dedicated rewrite rules. The rewrite rules are driven by a lightweight effect inference that analyses what effect operations may be called by a goal. We illustrate the effectiveness of this approach on a range of benchmarks. [ABSTRACT FROM AUTHOR]

Nowadays, clusters of multicores are becoming the norm and, although, many or-parallel Prolog systems have been developed in the past, to the best of our knowledge, none of them was specially designed to explore the combination of shared and distributed memory architectures. In recent work, we have proposed a novel computational model specially designed for such combination which introduces a layered model with two scheduling levels, one for workers sharing memory resources, which we named a team of workers, and another for teams of workers (not sharing memory resources). In this work, we present a first implementation of such model and for that we revive and extend the YapOr system to exploit or-parallelism between teams of workers. We also propose a new set of built-in predicates that constitute the syntax to interact with an or-parallel engine in our platform. Experimental results show that our implementation is able to increase speedups as we increase the number of workers per team, thus taking advantage of the maximum number of cores in a machine, and to increase speedups as we increase the number of teams, thus taking advantage of adding more computer nodes to a cluster. [ABSTRACT FROM AUTHOR]

This paper presents the pl-nauty library, a Prolog interface to the nauty graph-automorphism tool. Adding the capabilities of nauty to Prolog combines the strength of the “generate and prune” approach that is commonly used in logic programming and constraint solving, with the ability to reduce symmetries while reasoning over graph objects. Moreover, it enables the integration of nauty in existing tool-chains, such as SAT-solvers or finite domain constraints compilers which exist for Prolog. The implementation consists of two components: pl-nauty, an interface connecting nauty's C library with Prolog, and pl-gtools, a Prolog framework integrating the software component of pl-nauty, called gtools, with Prolog. The complete tool is available as a SWI-Prolog module. We provide a series of usage examples including two that apply to generate Ramsey graphs. [ABSTRACT FROM AUTHOR]

Systems for symbolic event recognition infer occurrences of events in time using a set of event definitions in the form of first-order rules. The Event Calculus is a temporal logic that has been used as a basis in event recognition applications, providing among others, direct connections to machine learning, via Inductive Logic Programming (ILP). We present an ILP system for online learning of Event Calculus theories. To allow for a single-pass learning strategy, we use the Hoeffding bound for evaluating clauses on a subset of the input stream. We employ a decoupling scheme of the Event Calculus axioms during the learning process, that allows to learn each clause in isolation. Moreover, we use abductive-inductive logic programming techniques to handle unobserved target predicates. We evaluate our approach on an activity recognition application and compare it to a number of batch learning techniques. We obtain results of comparable predicative accuracy with significant speed-ups in training time. We also outperform hand-crafted rules and match the performance of a sound incremental learner that can only operate on noise-free datasets. [ABSTRACT FROM AUTHOR]

The dlvhex system implements the hex-semantics, which integrates answer set programming (ASP) with arbitrary external sources. Since its first release ten years ago, significant advancements were achieved. Most importantly, the exploitation of properties of external sources led to efficiency improvements and flexibility enhancements of the language, and technical improvements on the system side increased user's convenience. In this paper, we present the current status of the system and point out the most important recent enhancements over early versions. While existing literature focuses on theoretical aspects and specific components, a bird's eye view of the overall system is missing. In order to promote the system for real-world applications, we further present applications which were already successfully realized on top of dlvhex. [ABSTRACT FROM AUTHOR]

Answer Set Programming (ASP) is a popular logic programming paradigm that has been applied for solving a variety of complex problems. Among the most challenging real-world applications of ASP are two industrial problems defined by Siemens: the Partner Units Problem (PUP) and the Combined Configuration Problem (CCP). The hardest instances of PUP and CCP are out of reach for state-of-the-art ASP solvers. Experiments show that the performance of ASP solvers could be significantly improved by embedding domain-specific heuristics, but a proper effective integration of such criteria in off-the-shelf ASP implementations is not obvious. In this paper the combination of ASP and domain-specific heuristics is studied with the goal of effectively solving real-world problem instances of PUP and CCP. As a byproduct of this activity, the ASP solver wasp was extended with an interface that eases embedding new external heuristics in the solver. The evaluation shows that our domain-heuristic-driven ASP solver finds solutions for all the real-world instances of PUP and CCP ever provided by Siemens. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

Unsatisfiable core analysis can boost the computation of optimum stable models for logic programs with weak constraints. However, current solvers employing unsatisfiable core analysis either run to completion, or provide no suboptimal stable models but the one resulting from the preliminary disjoint cores analysis. This drawback is circumvented here by introducing a progression based shrinking of the analyzed unsatisfiable cores. In fact, suboptimal stable models are possibly found while shrinking unsatisfiable cores, hence resulting into an anytime algorithm. Moreover, as confirmed empirically, unsatisfiable core analysis also benefits from the shrinking process in terms of solved instances. [ABSTRACT FROM AUTHOR]

In order to achieve competitive performance, abstract machines for Prolog and related languages end up being large and intricate, and incorporate sophisticated optimizations, both at the design and at the implementation levels. At the same time, efficiency considerations make it necessary to use low-level languages in their implementation. This makes them laborious to code, optimize, and, especially, maintain and extend. Writing the abstract machine (and ancillary code) in a higher-level language can help tame this inherent complexity. We show how the semantics of most basic components of an efficient virtual machine for Prolog can be described using (a variant of) Prolog. These descriptions are then compiled to C and assembled to build a complete bytecode emulator. Thanks to the high-level of the language used and its closeness to Prolog, the abstract machine description can be manipulated using standard Prolog compilation and optimization techniques with relative ease. We also show how, by applying program transformations selectively, we obtain abstract machine implementations whose performance can match and even exceed that of state-of-the-art, highly-tuned, hand-crafted emulators. [ABSTRACT FROM AUTHOR]