Computer Aided Design systems provide tools for building and manipulating models of solid objects. Some also provide access to programming languages so that parametrised designs can be expressed. There is a sharp distinction, therefore, between building models, a concrete graphical editing activity, and programming, an abstract, textual, algorithm-construction activity. The recently proposed Language for Structured Design (LSD) was motivated by a desire to combine the design and programming activities in one language. LSD achieves this by extending a visual logic programming language to incorporate the notions of solids and operations on solids. Here we investigate another aspect of the LSD approach, namely, that by using visual logic programming as the engine to drive the parametrised assembly of objects, we also gain the powerful symbolic problem-solving capability that is the forté of logic programming languages. This allows the designer/programmer to work at a higher level, giving declarative specifications of a design in order to obtain the design descriptions. Hence LSD integrates problem solving, design synthesis, and prototype assembly in a single homogeneous programming/design environment. We demonstrate this specification-to-final-assembly capability using the masterkeying problem for designing systems of locks and keys.

Constraint answer set programming is a promising research direction that integrates answer set programming with constraint processing. It is often informally related to the field of satisfiability modulo theories. Yet, the exact formal link is obscured as the terminology and concepts used in these two research areas differ. In this paper, we connect these two research areas by uncovering the precise formal relation between them. We believe that this work will boost the cross-fertilization of the theoretical foundations and the existing solving methods in both areas. As a step in this direction, we provide a translation from constraint answer set programs with integer linear constraints to satisfiability modulo linear integer arithmetic that paves the way to utilizing modern satisfiability modulo theories solvers for computing answer sets of constraint answer set programs.

We propose a timed and soft extension of Concurrent Constraint Programming. The time extension is based on the hypothesis of bounded asynchrony: The computation takes a bounded period of time and is measured by a discrete global clock. Action prefixing is then considered as the syntactic marker that distinguishes a time instant from the next one. Supported by soft constraints instead of crisp ones, tell and ask agents are now equipped with a preference (or consistency) threshold, which is used to determine their success or suspension. In this paper, we provide a language to describe the agents' behavior, together with its operational and denotational semantics, for which we also prove the compositionality and correctness properties. After presenting a semantics using maximal parallelism of actions, we also describe a version for their interleaving on a single processor (with maximal parallelism for time elapsing). Coordinating agents that need to take decisions on both preference values and time events may benefit from this language.

This paper studies the stable model semantics of logic programs with (abstract) constraint atoms and their properties. We introduce a succinct abstract representation of these constraint atoms in which a constraint atom is represented compactly. We show two applications. First, under this representation of constraint atoms, we generalize the Gelfond–Lifschitz transformation and apply it to define stable models (also called answer sets) for logic programs with arbitrary constraint atoms. The resulting semantics turns out to coincide with the one defined by Son et al. (2007), which is based on a fixpoint approach. One advantage of our approach is that it can be applied, in a natural way, to define stable models for disjunctive logic programs with constraint atoms, which may appear in the disjunctive head as well as in the body of a rule. As a result, our approach to the stable model semantics for logic programs with constraint atoms generalizes a number of previous approaches. Second, we show that our abstract representation of constraint atoms provides a means to characterize dependencies of atoms in a program with constraint atoms, so that some standard characterizations and properties relying on these dependencies in the past for logic programs with ordinary atoms can be extended to logic programs with constraint atoms.

We describe an algorithm for proving termination of programs abstracted to systems of monotonicity constraints in the integer domain. Monotonicity constraints are a nontrivial extension of the well-known size-change termination method. While deciding termination for systems of monotonicity constraints is PSPACE complete, we focus on a well-defined and significant subset, which we call MCNP (for “monotonicity constraints in NP”), designed to be amenable to a SAT-based solution. Our technique is based on the search for a special type of ranking function defined in terms of bounded differences between multisets of integer values. We describe the application of our approach as the back end for the termination analysis of Java Bytecode. At the front end, systems of monotonicity constraints are obtained by abstracting information, using two different termination analyzers: AProVE and COSTA. Preliminary results reveal that our approach provides a good trade-off between precision and cost of analysis.

In the context of planning and reasoning about actions and change, we call an action reversible when its effects can be reverted by applying other actions, returning to the original state. Renewed interest in this area has led to several results in the context of the PDDL language, widely used for describing planning tasks. In this paper, we propose several solutions to the computational problem of deciding the reversibility of an action. In particular, we leverage an existing translation from PDDL to Answer Set Programming (ASP), and then use several different encodings to tackle the problem of action reversibility for the STRIPS fragment of PDDL. For these, we use ASP, as well as Epistemic Logic Programming (ELP), an extension of ASP with epistemic operators, and compare and contrast their strengths and weaknesses.

Approximation fixpoint theory (AFT) provides an algebraic framework for the study of fixpoints of operators on bilattices and has found its applications in characterizing semantics for various classes of logic programs and nonmonotonic languages. In this paper, we show one more application of this kind: the alternating fixpoint operator by Knorr et al. for the study of the well-founded semantics for hybrid minimal knowledge and negation as failure (MKNF) knowledge bases is in fact an approximator of AFT in disguise, which, thanks to the abstraction power of AFT, characterizes not only the well-founded semantics but also two-valued as well as three-valued semantics for hybrid MKNF knowledge bases. Furthermore, we show an improved approximator for these knowledge bases, of which the least stable fixpoint is information richer than the one formulated from Knorr et al.’s construction. This leads to an improved computation for the well-founded semantics. This work is built on an extension of AFT that supports consistent as well as inconsistent pairs in the induced product bilattice, to deal with inconsistencies that arise in the context of hybrid MKNF knowledge bases. This part of the work can be considered generalizing the original AFT from symmetric approximators to arbitrary approximators.

Epistemic logic programs (ELPs) are an extension of answer set programming (ASP) with epistemic operators that allow for a form of meta-reasoning, that is, reasoning over multiple possible worlds. Existing ELP solving approaches generally rely on making multiple calls to an ASP solver in order to evaluate the ELP. However, in this paper, we show that there also exists a direct translation from ELPs into non-ground ASP with bounded arity. The resulting ASP program can thus be solved in a single shot. We then implement this encoding method, using recently proposed techniques to handle large, non-ground ASP rules, into the prototype ELP solving system “selp,” which we present in this paper. This solver exhibits competitive performance on a set of ELP benchmark instances.

Answer Set Programming (ASP) solvers are highly-tuned and complex procedures that implicitly solve the consistency problem, i.e., deciding whether a logic program admits an answer set. Verifying whether a claimed answer set is formally a correct answer set of the program can be decided in polynomial time for (normal) programs. However, it is far from immediate to verify whether a program that is claimed to be inconsistent, indeed does not admit any answer sets. In this paper, we address this problem and develop the new proof format ASP-DRUPE for propositional, disjunctive logic programs, including weight and choice rules. ASP-DRUPE is based on the Reverse Unit Propagation (RUP) format designed for Boolean satisfiability. We establish correctness of ASP-DRUPE and discuss how to integrate it into modern ASP solvers. Later, we provide an implementation of ASP-DRUPE into the wasp solver for normal logic programs.

This paper proposes a model, the linear model, for randomly generating logic programs with low density of rules and investigates statistical properties of such random logic programs. It is mathematically shown that the average number of answer sets for a random program converges to a constant when the number of atoms approaches infinity. Several experimental results are also reported, which justify the suitability of the linear model. It is also experimentally shown that, under this model, the size distribution of answer sets for random programs tends to a normal distribution when the number of atoms is sufficiently large.

Assertion checking is an invaluable programmer’s tool for finding many classes of errors or verifying their absence in dynamic languages such as Prolog. For Prolog programmers, this means being able to have relevant properties, such as modes, types, determinacy, nonfailure, sharing, constraints, and cost, checked and errors flagged without having to actually run the program. Such global static analysis tools are arguably most useful the earlier they are used in the software development cycle, and fast response times are essential for interactive use. Triggering a full and precise semantic analysis of a software project every time a change is made can be prohibitively expensive. This is specially the case when complex properties need to be inferred for large, realistic code bases. In our static analysis and verification framework, this challenge is addressed through a combination of modular and incremental (context- and path-sensitive) analysis that is responsive to program edits, at different levels of granularity. In this tool paper, we present how the combination of this framework within an integrated development environment (IDE) takes advantage of such incrementality to achieve a high level of reactivity when reflecting analysis and verification results back as colorings and tooltips directly on the program text – the tool’s VeriFly mode. The concrete implementation that we describe is Emacs-based and reuses in part off-the-shelf “on-the-fly” syntax checking facilities (flycheck). We believe that similar extensions are also reproducible with low effort in other mature development environments. Our initial experience with the tool shows quite promising results, with low latency times that provide early, continuous, and precise assertion checking and other semantic feedback to programmers during the development process. The tool supports Prolog natively, as well as other languages by semantic transformation into Horn clauses.

Head-elementary-set-free (HEF) programs were proposed in (Gebser et al. 2007) and shown to generalize over head-cycle-free programs while retaining their nice properties. It was left as an open problem in (Gebser et al. 2007) to establish the complexity of identifying HEF programs. This note solves the open problem by showing that the problem is complete for coNP.

In the analysis of logic programs, abstract domains for detecting sharing properties are widely used. Recently, the new domain ${\mathtt{ShLin}^{\omega}}$ has been introduced to generalize both sharing and linearity information. This domain is endowed with an optimal abstract operator for single-binding unification. The authors claim that the repeated application of this operator is also optimal for multibinding unification. This is the proof of such a claim.

A core part of the rehabilitation scheduling process consists of planning rehabilitation physiotherapy sessions for patients, by assigning proper operators to them in a certain time slot of a given day, taking into account several legal, medical, and ethical requirements and optimizations, for example, patient’s preferences and operator’s work balancing. Being able to efficiently solve such problem is of upmost importance, in particular after the COVID-19 pandemic that significantly increased rehabilitation’s needs. In this paper, we present a two-phase solution to rehabilitation scheduling based on Answer Set Programming, which proved to be an effective tool for solving practical scheduling problems. We first present a general encoding and then add domain-specific optimizations. Results of experiments performed on both synthetic and real benchmarks, the latter provided by ICS Maugeri, show the effectiveness of our solution as well as the impact of our domain-specific optimizations.

Logic programming provides a high-level view of programming, giving implementers a vast latitude into what techniques to explore to achieve the best performance for logic programs. Towards obtaining maximum performance, one of the holy grails of logic programming has been to design computational models that could be executed efficiently and that would allow both for a reduction of the search space and for exploiting all the available parallelism in the application. These goals have motivated the design of the Extended Andorra Model (EAM), a model where goals that do not constrain nondeterministic goals can execute first. In this work, we present and evaluate the Basic design for EAM, a system that builds upon David H. D. Warren's original EAM with Implicit Control. We provide a complete description and implementation of the Basic design for EAM System as a set of rewrite and control rules. We present the major data structures and execution algorithms that are required for efficient execution, and evaluate system performance. A detailed performance study of our system is included. Our results show that the system achieves acceptable base performance and that a number of applications benefit from the advanced search inherent to the EAM.

In everyday life it happens that a person has to reason out what other peoplethink and how they behave, in order to achieve his goals. In other words, anindividual may be required to adapt his behavior by reasoning about the others'mental state. In this paper we focus on a knowledge-representation languagederived from logic programming which both supports the representation of mentalstates of individual communities and provides each with the capability ofreasoning about others' mental states and acting accordingly. The proposedsemantics is shown to be translatable into stable model semantics of logicprograms with aggregates.

In the theory of answer set programming, two groups of rules are called strongly equivalent if, informally speaking, they have the same meaning in any context. The relationship between strong equivalence and the propositional logic of here-and-there allows us to establish strong equivalence by deriving rules of each group from rules of the other. In the process, rules are rewritten as propositional formulas. We extend this method of proving strong equivalence to an answer set programming language that includes operations on integers. The formula representing a rule in this language is a first-order formula that may contain comparison symbols among its predicate constants, and symbols for arithmetic operations among its function constants. The paper is under consideration for acceptance in TPLP.

A common feature in Answer Set Programming is the use of a second negation, stronger than default negation and sometimes called explicit, strong or classical negation. This explicit negation is normally used in front of atoms, rather than allowing its use as a regular operator. In this paper we consider the arbitrary combination of explicit negation with nested expressions, as those defined by Lifschitz, Tang and Turner. We extend the concept of reduct for this new syntax and then prove that it can be captured by an extension of Equilibrium Logic with this second negation. We study some properties of this variant and compare to the already known combination of Equilibrium Logic with Nelson’s strong negation.

The well-founded semantics is one of the most widely studied and used semantics of logic programs with negation. In the case of finite propositional programs, it can be computed in polynomial time, more specifically, in O([mid ]At(P)[mid ] × size(P)) steps, where size(P) denotes the total number of occurrences of atoms in a logic program P. This bound is achieved by an algorithm introduced by Van Gelder and known as the alternating-fixpoint algorithm. Improving on the alternating-fixpoint algorithm turned out to be difficult. In this paper we study extensions and modifications of the alternating-fixpoint approach. We then restrict our attention to the class of programs whose rules have no more than one positive occurrence of an atom in their bodies. For programs in that class we propose a new implementation of the alternating-fixpoint method in which false atoms are computed in a top-down fashion. We show that our algorithm is faster than other known algorithms and that for a wide class of programs it is linear and so, asymptotically optimal.