This special issue of TPLP commemorates the 25th edition of the annual conference organized by GULP (Gruppo Ricercatori e Utenti Logic Programming), the Italian group of researchers and users of logic programming. The first event in this series was held at Genoa in 1986, one year after the foundation of the user group, continuing annually ever since. In 1994, the conference joined forces with the Spanish conference PRODE (on Declarative Programming), and in 1996 with the Portuguese APPIA (on Artificial Intelligence). This collaboration continued until 2003. Starting from 2004, the event became known as CILC (Convegno Italiano di Logica Computazionale, Italian Conference on Computational Logic), thereby broadening its topics to general computational logic, while becoming a national Italian event again. Being one of the oldest and largest national events of its kind, over the years the conference has been an important networking opportunity and catalyst for persons with different backgrounds, coming from theory and practice, and from research and industry, for exchanging their visions, achievements, and challenges in logic programming. For a more detailed historical account on GULP and its annual conferences, we refer to Rossi (2010).

The paper presents a knowledge representation formalism, in the form of a high-level Action Description Language (ADL) for multi-agent systems, where autonomous agents reason and act in a shared environment. Agents are autonomously pursuing individual goals, but are capable of interacting through a shared knowledge repository. In their interactions through shared portions of the world, the agents deal with problems of synchronization and concurrency; the action language allows the description of strategies to ensure a consistent global execution of the agents’ autonomously derived plans. A distributed planning problem is formalized by providing the declarative specifications of the portion of the problem pertaining to a single agent. Each of these specifications is executable by a stand-alone CLP-based planner. The coordination among agents exploits a Linda infrastructure. The proposal is validated in a prototype implementation developed in SICStus Prolog.

We present a method for the automated verification of temporal properties of infinite state systems. Our verification method is based on the specialization of constraint logic programs (CLP) and works in two phases: (1) in the first phase, a CLP specification of an infinite state system is specialized with respect to the initial state of the system and the temporal property to be verified, and (2) in the second phase, the specialized program is evaluated by using a bottom-up strategy. The effectiveness of the method strongly depends on the generalization strategy which is applied during the program specialization phase. We consider several generalization strategies obtained by combining techniques already known in the field of program analysis and program transformation, and we also introduce some new strategies. Then, through many verification experiments, we evaluate the effectiveness of the generalization strategies we have considered. Finally, we compare the implementation of our specialization-based verification method to other constraint-based model checking tools. The experimental results show that our method is competitive with the methods used by those other tools.

In this paper, we combine Answer Set Programming (ASP) with Dynamic Linear Time Temporal Logic (DLTL) to define a temporal logic programming language for reasoning about complex actions and infinite computations. DLTL extends propositional temporal logic of linear time with regular programs of propositional dynamic logic, which are used for indexing temporal modalities. The action language allows general DLTL formulas to be included in domain descriptions to constrain the space of possible extensions. We introduce a notion of Temporal Answer Set for domain descriptions, based on the usual notion of Answer Set. Also, we provide a translation of domain descriptions into standard ASP and use Bounded Model Checking (BMC) techniques for the verification of DLTL constraints.

A data integration system provides transparent access to different data sources by suitably combining their data, and providing the user with a unified view of them, called global schema. However, source data are generally not under the control of the data integration process; thus, integrated data may violate global integrity constraints even in the presence of locally consistent data sources. In this scenario, it may be anyway interesting to retrieve as much consistent information as possible. The process of answering user queries under global constraint violations is called consistent query answering (CQA). Several notions of CQA have been proposed, e.g., depending on whether integrated information is assumed to be sound, complete, exact, or a variant of them. This paper provides a contribution in this setting: it uniforms solutions coming from different perspectives under a common Answer-Set Programming (ASP)-based core, and provides query-driven optimizations designed for isolating and eliminating inefficiencies of the general approach for computing consistent answers. Moreover, the paper introduces some new theoretical results enriching existing knowledge on the decidability and complexity of the considered problems. The effectiveness of the approach is evidenced by experimental results.

Answer-Set Programming (ASP) is a powerful logic-based programming language, which is enjoying increasing interest within the scientific community and (very recently) in industry. The evaluation of Answer-Set Programs is traditionally carried out in two steps. At the first step, an input program undergoes the so-called instantiation (or grounding) process, which produces a program ′ semantically equivalent to , but not containing any variable; in turn, ′ is evaluated by using a backtracking search algorithm in the second step. It is well-known that instantiation is important for the efficiency of the whole evaluation, might become a bottleneck in common situations, is crucial in several real-world applications, and is particularly relevant when huge input data have to be dealt with. At the time of this writing, the available instantiator modules are not able to exploit satisfactorily the latest hardware, featuring multi-core/multi-processor Symmetric MultiProcessing technologies. This paper presents some parallel instantiation techniques, including load-balancing and granularity control heuristics, which allow for the effective exploitation of the processing power offered by modern Symmetric MultiProcessing machines. This is confirmed by an extensive experimental analysis reported herein.

Distribution semantics is one of the most prominent approaches for the combination of logic programming and probability theory. Many languages follow this semantics, such as Independent Choice Logic, PRISM, pD, Logic Programs with Annotated Disjunctions (LPADs), and ProbLog. When a program contains functions symbols, the distribution semantics is well–defined only if the set of explanations for a query is finite and so is each explanation. Well–definedness is usually either explicitly imposed or is achieved by severely limiting the class of allowed programs. In this paper, we identify a larger class of programs for which the semantics is well–defined together with an efficient procedure for computing the probability of queries. Since Logic Programs with Annotated Disjunctions offer the most general syntax, we present our results for them, but our results are applicable to all languages under the distribution semantics. We present the algorithm “Probabilistic Inference with Tabling and Answer subsumption” (PITA) that computes the probability of queries by transforming a probabilistic program into a normal program and then applying SLG resolution with answer subsumption. PITA has been implemented in XSB and tested on six domains: two with function symbols and four without. The execution times are compared with those of ProbLog, cplint, and CVE. PITA was almost always able to solve larger problems in a shorter time, on domains with and without function symbols.