In sequent calculi, cut elimination is a property that guarantees that any provable formula can be proven analytically. For example, Gentzen’s classical and intuitionistic calculi LK and LJ enjoy cut elimination. The property is less studied in coinductive extensions of sequent calculi. In this paper, we use coinductive Horn clause theories to show that cut is not eliminable in a coinductive extension of LJ, a system we call CLJ. We derive two further practical results from this study. We show that CoLP by Gupta et al. gives rise to cut-free proofs in CLJ with fixpoint terms, and we formulate and implement a novel method of coinductive theory exploration that provides several heuristics for discovery of cut formulae in CLJ.

Justification theory is a unifying semantic framework. While it has its roots in non-monotonic logics, it can be applied to various areas in computer science, especially in explainable reasoning; its most central concept is a justification: an explanation why a property holds (or does not hold) in a model.

In this paper, we continue the study of justification theory by means of three major contributions. The first is studying the relation between justification theory and game theory. We show that justification frameworks can be seen as a special type of games. The established connection provides the theoretical foundations for our next two contributions. The second contribution is studying under which condition two different dialects of justification theory (graphs as explanations vs trees as explanations) coincide. The third contribution is establishing a precise criterion of when a semantics induced by justification theory yields consistent results. In the past proving that such semantics were consistent took cumbersome and elaborate proofs.

We show that these criteria are indeed satisfied for all common semantics of logic programming.

In this paper, we focus on the problem of existence and computing of small and large stable models. We show that for every fixed integer k, there is a linear-time algorithm to decide the problem LSM (large stable models problem): does a logic program P have a stable model of size at least [mid ]P[mid ]−k? In contrast, we show that the problem SSM (small stable models problem) to decide whether a logic program P has a stable model of size at most k is much harder. We present two algorithms for this problem but their running time is given by polynomials of order depending on k. We show that the problem SSM is fixed-parameter intractable by demonstrating that it is W[2]-hard. This result implies that it is unlikely an algorithm exists to compute stable models of size at most k that would run in time O(mc), where m is the size of the program and c is a constant independent of k. We also provide an upper bound on the fixed-parameter complexity of the problem SSM by showing that it belongs to the class W[3].

In prior work, we showed that logic programming compilation can be given a proof-theoretic justification for generic abstract logic programming languages, and demonstrated this technique in the case of hereditary Harrop formulas and their linear variant. Compiled clauses were themselves logic formulas except for the presence of a second-order abstraction over the atomic goals matching their head. In this paper, we revisit our previous results into a more detailed and fully logical justification that does away with this spurious abstraction. We then refine the resulting technique to support well-moded programs efficiently.

In this paper, we propose an extension of logic programming where each default literal derived from the well-founded model is associated to a justification represented as an algebraic expression. This expression contains both causal explanations (in the form of proof graphs built with rule labels) and terms under the scope of negation that stand for conditions that enable or disable the application of causal rules. Using some examples, we discuss how these new conditions, we respectively call enablers and inhibitors, are intimately related to default negation and have an essentially different nature from regular cause-effect relations. The most important result is a formal comparison to the recent algebraic approaches for justifications in logic programming: Why-not Provenance and Causal Graphs. We show that the current approach extends both Why-not Provenance and Causal Graphs justifications under the well-founded semantics and, as a byproduct, we also establish a formal relation between these two approaches.

Ad hoc teamwork (AHT) refers to the problem of enabling an agent to collaborate with teammates without prior coordination. State of the art methods in AHT are data-driven, using a large labeled dataset of prior observations to model the behavior of other agent types and to determine the ad hoc agent’s behavior. These methods are computationally expensive, lack transparency, and make it difficult to adapt to previously unseen changes. Our recent work introduced an architecture that determined an ad hoc agent’s behavior based on non-monotonic logical reasoning with prior commonsense domain knowledge and models learned from limited examples to predict the behavior of other agents. This paper describes KAT, a knowledge-driven architecture for AHT that substantially expands our prior architecture’s capabilities to support: (a) online selection, adaptation, and learning of the behavior prediction models; and (b) collaboration with teammates in the presence of partial observability and limited communication. We illustrate and experimentally evaluate KAT’s capabilities in two simulated benchmark domains for multiagent collaboration: Fort Attack and Half Field Offense. We show that KAT’s performance is better than a purely knowledge-driven baseline, and comparable with or better than a state of the art data-driven baseline, particularly in the presence of limited training data, partial observability, and changes in team composition.

Conventional processor architectures are restricted in exploiting instruction level parallelism (ILP) due to the relatively low number of programmer-visible registers. Therefore, more recent processor architectures expose their datapaths so that the compiler (1) can schedule parallel instructions to different processing units and (2) can make effective use of local storage of the processing units. Among these architectures, the Synchronous Control Asynchronous Dataflow (SCAD) architecture is a new exposed datapath architecture whose processing units are equipped with first-in first-out (FIFO) buffers at their input and output ports.

In contrast to register-based machines, the optimal code generation for SCAD is still a matter of research. In particular, SAT and SMT solvers were used to generate optimal resource constrained and optimal time constrained schedules for SCAD, respectively. As Answer Set Programming (ASP) offers better flexibility in handling such scheduling problems, we focus in this paper on using an answer set solver for both resource and time constrained optimal SCAD code generation. As a major benefit of using ASP, we are able to generate all optimal schedules for a given program which allows one to study their properties. Furthermore, the experimental results of this paper demonstrate that the answer set solver can compete with SAT solvers and outperforms SMT solvers. This paper is under consideration for acceptance in TPLP.

In the last years, abstract argumentation has met with great success in AI, since it has served to capture several non-monotonic logics for AI. Relations between argumentation framework (AF) semantics and logic programming ones are investigating more and more. In particular, great attention has been given to the well-known stable extensions of an AF, that are closely related to the answer sets of a logic program. However, if a framework admits a small incoherent part, no stable extension can be provided. To overcome this shortcoming, two semantics generalizing stable extensions have been studied, namely semi-stable and stage. In this paper, we show that another perspective is possible on incoherent AFs, called paracoherent extensions, as they have a counterpart in paracoherent answer set semantics. We compare this perspective with semi-stable and stage semantics, by showing that computational costs remain unchanged, and moreover an interesting symmetric behaviour is maintained.

Maher (2012) introduced an approach for relative expressiveness of defeasible logics, and two notions of relative expressiveness were investigated. Using the first of these definitions of relative expressiveness, we show that all the defeasible logics in the DL framework are equally expressive under this formulation of relative expressiveness. The second formulation of relative expressiveness is stronger than the first. However, we show that logics incorporating individual defeat are equally expressive as the corresponding logics with team defeat. Thus the only differences in expressiveness of logics in DL arise from differences in how ambiguity is handled. This completes the study of relative expressiveness in DL begun in Maher (2012).

This paper studies the relation between two recent extensions of propositional Equilibrium Logic, a well-known logical characterisation of Answer Set Programming. In particular, we show how Temporal Equilibrium Logic, which introduces modal operators as those typically handled in Linear-Time Temporal Logic (LTL), can be encoded into Infinitary Equilibrium Logic, a recent formalisation that allows the use of infinite conjunctions and disjunctions. We prove the correctness of this encoding and, as an application, we further use it to show that the semantics of the temporal logic programming formalism called TEMPLOG is subsumed by Temporal Equilibrium Logic.

We study the decidability of termination for two CHR dialects which, similarly to the Datalog like languages, are defined by using a signature which does not allow function symbols (of arity > 0). Both languages allow the use of the = built-in in the body of rules, thus are built on a host language that supports unification. However each imposes one further restriction. The first CHR dialect allows only range-restricted rules, that is, it does not allow the use of variables in the body or in the guard of a rule if they do not appear in the head. We show that the existence of an infinite computation is decidable for this dialect. The second dialect instead limits the number of atoms in the head of rules to one. We prove that in this case, the existence of a terminating computation is decidable. These results show that both dialects are strictly less expressive1 than Turing Machines. It is worth noting that the language (without function symbols) without these restrictions is as expressive as Turing Machines.

$\lambda$Prolog is known to be well-suited for expressing and implementing logics and inference systems. We show that lemmas and definitions in such logics can be implemented with a great economy of expression. We encode a higher-order logic using an encoding that maps both terms and types of the object logic (higher-order logic) to terms of the metalanguage ($\lambda$Prolog). We discuss both the Terzo and Teyjus implementations of $\lambda$Prolog. We also encode the same logic in Twelf and compare the features of these two metalanguages for our purposes.

Modal logic S5 has attracted significant attention and has led to several practical applications, owing to its simplified approach to dealing with nesting modal operators. Efficient implementations for evaluating satisfiability of S5 formulas commonly rely on Skolemisation to convert them into propositional logic formulas, essentially by introducing copies of propositional atoms for each set of interpretations (possible worlds). This approach is simple, but often results into large formulas that are too difficult to process, and therefore more parsimonious constructions are required. In this work, we propose to use Answer Set Programming for implementing such constructions, and in particular for identifying the propositional atoms that are relevant in every world by means of a reachability relation. The proposed encodings are designed to take advantage of other properties such as entailment relations of subformulas rooted by modal operators. An empirical assessment of the proposed encodings shows that the reachability relation is very effective and leads to comparable performance to a state-of-the-art S5 solver based on SAT, while entailment relations are possibly too expensive to reason about and may result in overhead.

This paper develops automated testing and debugging techniques for answer set solver development. We describe a flexible grammar-based black-box ASP fuzz testing tool which is able to reveal various defects such as unsound and incomplete behavior, i.e. invalid answer sets and inability to find existing solutions, in state-of-the-art answer set solver implementations. Moreover, we develop delta debugging techniques for shrinking failure-inducing inputs on which solvers exhibit defective behavior. In particular, we develop a delta debugging algorithm in the context of answer set solving, and evaluate two different elimination strategies for the algorithm.

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).

We investigate the relationship between the generalization of program completion defined in 1984 by Lloyd and Topor and the generalization of the stable model semantics introduced recently by Ferraris et al. The main theorem can be used to characterize, in some cases, the general stable models of a logic program by a first-order formula. The proof uses Truszczynski's stable model semantics of infinitary propositional formulas.

Recent work in Answer Set Programming has integrated ideas from Constraint Programming. This has led to a new field called ASP Modulo CSP (CASP), in which the ASP language is enriched with constraint atoms representing constraint satisfaction problems. These constraints have a more compact grounding and are handled by a new generation of search algorithms. However, the burden is on the modeler to exploit these new constructs in his declarative problem specifications. Here, we explore how to remove this burden by automatically generating constraint atoms. We do so in the context of FO(·)IDP, a knowledge representation language that extends first-order logic with, among others, inductive definitions, arithmetic and aggregates. We uncover functional dependencies in declarative problem specifications with a theorem prover and exploit them with a transformation that introduces functions. Experimental evaluation shows that we obtain more compact groundings and better search performance.

Equational theories that contain axioms expressing associativity and commutativity (AC) of certain operators are ubiquitous. Theorem proving methods in such theories rely on well-founded orders that are compatible with the AC axioms. In this paper, we consider various definitions of AC-compatible Knuth-Bendix orders. The orders of Steinbach and of Korovin and Voronkov are revisited. The former is enhanced to a more powerful version, and we modify the latter to amend its lack of monotonicity on non-ground terms. We further present new complexity results. An extension reflecting the recent proposal of subterm coefficients in standard Knuth-Bendix orders is also given. The various orders are compared on problems in termination and completion.

Precondition inference is a non-trivial problem with important applications in program analysis and verification. We present a novel iterative method for automatically deriving preconditions for the safety and unsafety of programs. Each iteration maintains over-approximations of the set of safe and unsafe initial states, which are used to partition the program’s initial states into those known to be safe, known to be unsafe and unknown. We then construct revised programs with those unknown initial states and iterate the procedure until the approximations are disjoint or some termination criteria are met. An experimental evaluation of the method on a set of software verification benchmarks shows that it can infer precise preconditions (sometimes optimal) that are not possible using previous methods.

This paper presents PFLP, a library for probabilistic programming in the functional logic programming language Curry. It demonstrates how the concepts of a functional logic programming language support the implementation of a library for probabilistic programming. In fact, the paradigms of functional logic and probabilistic programming are closely connected. That is, language characteristics from one area exist in the other and vice versa. For example, the concepts of non-deterministic choice and call-time choice as known from functional logic programming are related to and coincide with stochastic memoization and probabilistic choice in probabilistic programming, respectively. We will further see that an implementation based on the concepts of functional logic programming can have benefits with respect to performance compared to a standard list-based implementation and can even compete with full-blown probabilistic programming languages, which we illustrate by several benchmarks.