CILC09

Many years of teaching demonstrated that one of the hardest concepts for students facing Prolog is the construction of the SLD tree. For this reason one student and the teachers of the Artificial Intelligence Course held at the Computer Science Department, University of Genova, developed PrettyProlog: an interpreter for a subset of Prolog, written in Java, born for didactic use. PrettyProlog features a GUI which allows the user to visualize the inner functioning of the interpreter, namely the construction of stack and SLD tree, and can be used to implement and graphically trace sophisticated programs involving cut, negation as failure, meta-programming.

Providing efficient ontology matching algorithms is one of the means for pursuing semantic interoperability. In this paper we discuss an algorithm that exploits natural language processing techniques for matching ontologies and that post-processes the obtained alignment in order to find semantic inconsistencies. The algorithm has been entirely implemented in Prolog, whose usefulness was mainly evident in the post-processing phase. A careful analysis of the recent state-of-the art witnesses the originality of our matching algorithm which is based on the “Adapted Lesk Algorithm” for word sense disambiguation. The experiments we carried out, although in their early stages, are encouraging.

We present a novel technique to combine satisfiability procedures for theories that model some data-structures and that share the integer offsets. This procedure extends the Nelson-Oppen approach to a family of non-disjoint theories that have practical interest in verification. The result is derived by showing that the considered theories satisfy the hypotheses of a general result on non-disjoint combination. In particular, the capability of computing logical consequences over the shared signature is ensured in a non trivial way by devising a suitable complete superposition calculus.

Since its introduction, the Event Calculus (EC) has been recognized for being an excellent framework to reason about time and events, and it has been applied to a variety of domains. However, its use inside logic-based frameworks has been mainly goal-driven. This has somehow limited its applicability in dynamic environments. We fill this gap by proposing a Reactive and logic-based implementation of the EC, called REC. We give an axiomatization of REC inside the SCIFF Abductive Logic Programming framework, and study its formal properties.

In this paper we propose a nonmonotonic extension ALC + Tmin of the Description Logic ALC for reasoning about prototypical properties and inheritance with exception. The logic ALC + Tmin is built upon a previously introduced (monotonic) logic ALC + T, that is obtained by adding a typicality operator T to ALC. The operator T is intended to select the “most normal” or “most typical” instances of a concept, so that knowledge bases may contain subsumption relations of the form “T(C ) is subsumed by P”, expressing that typical C-members have the property P. In order to perform nonmonotonic inferences, we define a “minimal model” semantics ALC + Tmin for ALC + T. The intuition is that preferred, or minimal models are those that maximise typical instances of concepts. By means of ALC + Tmin we are able to infer defeasible properties of (explicit or implicit) individuals. We also present a tableau calculus for deciding ALC + Tmin entailment. Main contributes of this paper have been also presented at the 11th European Conference on Logics in Artificial Intelligence "JELIA 2008".

We introduce permissive nominal terms. Nominal terms extend first-order terms with binding. They lack properties of first- and higher-order terms: Terms must be reasoned on in a context of `freshness assumptions'; it is not always possible to `choose a fresh variable symbol' for a nominal term; and it is not always possible to `alpha-convert a bound variable symbol'. Permissive nominal terms recover these `always fresh' and `always alpha-rename' properties. Freshness contexts are elided and the notion of unifier is based on substitution alone rather than on nominal terms' notion of substitution plus freshness conditions. Expressivity is not lost moving to the permissive case and the changes have significant effects on the mathematical good behaviour of the syntax.

The current technological trend depicts a scenario in which space, and more generally the environment in which the computation takes place, represents a key aspect that must be considered in order to improve systems context awareness. Reasoning about such context can be therefore interpreted as spatial reasoning, which means not only to be able to carry out inferences about the space itself, but also inferences about spatially related information according a given background knowledge. Past works have shown that hybrid modal logics are a powerful and rich formalism to model qualitative spatial reasoning and reasoning on information spread into graph-like structures. In this paper we present a research project that deals with the design and the implementation of a Model Checker for Hybrid Modal Logic. The functionality of the model checker is based on a backend module that accepts as inputs a list of hybrid modal formulas and the specification of a labeled graph structure representing a Kripke model on which the formulas will be evaluated. The implementation of the backend allows to perform different reasoning tasks with respect to those inputs, i.e. validity and satisfiability of a formula in a model, and satisfiability in all worlds.

We report on the computerized verification of Lagrange's theorem, carried out with the proof assistant ÆtnaNova/Referee. The scenario starts with the basic definitions in group theory, such as the notions of subgroups and right cosets. Then, the proof of Lagrange's theorem is formalized following the approach present in most algebra textbooks. The proof assistant ÆtnaNova/Referee is grounded on a variant of Zermelo-Fraenkel set theory, designed for the automatic verification of proofs. Referee is provided with a powerful inferential and defining mechanism based on set theory, together with a notation very close to that commonly used in mathematics. We also compare our set theoretic approach in the formalization of elementary group theory, and in particular of Lagrange's theorem, with those followed in other, more widespread, proof assistants.

Keywords: automated proof verification, Lagrange's theorem, set theory.

Classical supervised learning techniques are generally based on an inductive mechanism able to generalise a model from a set of positive examples, assuring its consistency with respect to a set of negative examples. In case of learning from positive evidence only, a typical task occurring when an agent would learn by observing and/or by imitating other agents, the inductive learning techniques must take into account the problem of over-generalisation. This paper proposes a general technique for incremental multi-class learning from positive examples only, which has been embedded in the learning system INTHELEX. The idea is to incremental suppose the positive evidence for the class c_i to be a negative evidence for all other classes c_j until the environment does not explicitly declare the contrary. An application of the proposed technique to the agent learning domain has been provided. The proposed framework has been used to simulate an agent learning and revising in an incremental way a logical model of a task by imitating skilled agents. In particular, demonstrations are incrementally received and used as training examples while the agent interacts in a stochastic environment. The experimental results prove the validity of the proposed approach on this application domain.

Keywords: Inductive Logic Programming, Incremental Learning

Planning Domain Definition Language (PDDL) is the most used language to encode and solve planning problems. In this paper we propose two PDDL-like languages that extends PDDL with new constructs such as static causal laws and time fluents with the aim of improving the expressivity of PDDL language. We study the complexity of the main computational problems related to the planning problem in the new languages. Finally we implement a planning solver using constraint programming in GECODE that outperforms the existing solvers for similar languages.

We build upon recent work by Baral, Dzifcal and Son that define the translation into ASP of (some classes of) natural language sentences from the lambda-calculus intermediate format generated by CCG grammars. We propose to use instead SE-DCG grammars, with some advantages: efficient parsing, 'on the flight' semantic analysis of sentences, that performs significant disambiguation in many cases, and automatic generation of lambda-calculus expressions from template ones, thus improving the effectiveness and generality of the translation process. Adopting SE-DCG's results in a fully logical framework, though as future work we envisage an integration of positive aspects of CCG's and SE-DCG's.

By replacement it is meant the substitution of one or more occurences of a formula with an equivalent one. In automated deduction this can be useful to reduce the search space. For tableau and modal calculi, this technique is known as Simplification and consists in replacing a formula with a logical constant (true or false). Recently, this idea has been applied to Intuitionistic Logic. This work in progress investigates further conditions on the applicability of Simplification in Intuitionistic Logic.

Dynamic composition of web services requires an automated step of contracting, i.e., the computation of a possibly fruitful interaction between two (or more) services, based on their policies and goals. In previous work, the SCIFF abductive logic language was used to represent the services' policies, and the associated proof procedure to perform the contracting. In this paper, we build on that work in order to exploit the results of the Description Logics research area to represent domain specific knowledge, either by importing the knowledge encoded in an ontology into a SCIFF knowledge base, or by interfacing the SCIFF proof procedure to an existing ontological reasoner.

This paper explores the use of Constraint Logic Programming (CLP) as a platform for experimenting with planning problems in presence of multiple interacting agents. The paper develops a novel constraint-based action language, BMAP, that enables the declarative description of large classes of multi-agent and multi-valued domains. BMAP supports several complex features, including combined effects, concurrency control, interacting actions, and delayed effects. The paper presents a mapping of BMAP theories to CLP and it demonstrates the effectiveness of an implementation in SICStus Prolog on several benchmark problems.

In previous work an extension of ASP, called RASP (standing for ASP with Resources), has been proposed. RASP supports declarative reasoning on production and consumption of (amounts of) resources. The approach combines stable model semantics with quantitative reasoning and relies on an algebraic structure to support computations and comparisons of amounts. The resulting framework also offered some form of preference reasoning on resources usage. In this paper we go further in this direction by introducing more expressive constructs to support complex preferences specification. The complexity of establishing the existence of an answer set, in such an enriched framework, is then shown to be NP-complete. A prototypical implementation of RASP has been realized. The tool, named raspberry, consists in a compiler that, given a ground RASP program, produces a pure ASP encoding suitable to be processed by commonly available ASP-solvers.

Keywords: Answer set programming, quantitative reasoning, preferences, language extensions

We present a new method for verifying Linear Temporal Logic (LTL) properties of finite state reactive systems based on logic programming and program transformation techniques. We encode a finite state system and the LTL property to be verified as a logic program on infinite lists. Then we apply a verification method consisting of two steps. In the first step we transform the logic program which encodes the system and the property to be verified into a new program belonging to the class of so-called monadic omega-programs (that is, stratified, linear recursive programs defining unary predicates on infinite lists). This transformation is constructed by applying rules that preserve correctness. In the second step we verify the property of interest by using specific proof rules for monadic omega-programs. We show that these proof rules can be encoded in a straightforward way as a logic program which always terminates when evaluated by tabled resolution. The computational complexity of our algorithm is the same as the Lichtenstein-Pnueli algorithm.

Recently, graded modalities have been added to the semantics of two of the logics most commonly used by the computer science community: mu-calculus, in [Kupferman et al.,02], and CTL in [Ferrante et al.,08]. In both these settings, graded modalities enrich the universal and existential quantifiers with the capability to express the concept of "at least k" or "all but k", for a non-negative integer k. Both mu-calculus and CTL naturally apply as specification languages for closed systems: in this paper, we study how graded modalities may affect specification languages for open systems. To this aim, we consider the Alternating-time Temporal Logic (ATL), a derivative of CTL that is interpreted on games, rather than transition systems. We present two different semantics: the first seems suitable to off-line synthesis applications while the second may find application in the verification of fault-tolerant controllers. For both these semantics, we efficiently solve the model checking problem, computing the truth values of graded ATL formulas on the states of a given game.

Product configurators are an emerging software technology, developed for helping companies in deploying mass customization strategies. Among the various approaches, constraint-based techniques look particularly encouraging, both for their modeling capabilities and for their efficiency. In this paper, we present our work on a product configurator based on Constraint Logic Programming. The system we propose integrates an existing configurator module with a reasoning engine written in SICStus Prolog.

The support for function symbols in logic programming under Answer Set Programming semantics (ASP) allows to overcome some modeling limitations of traditional ASP systems, such as the inability of handling infinite domains. On the other hand, admitting function symbols in ASP makes inference undecidable in the general case. Thus, the research is lately focusing on finding proper subclasses of ASP programs with functions for which decidability of inference is guaranteed. The two major proposals so far, finitary programs and finitely-ground programs, are complementary, to some extent; indeed, the former are conceived for allowing decidable querying (using a top-down evaluation strategy), while the latter for allowing finite model computation (using a bottom-up evaluation strategy). One of the main advantages of finitely-ground programs is that they can be directly evaluated by current ASP systems. However, many programs lie outside this class, such as, in general, positive finitary programs. Indeed, ground queries over such programs can be easily answered by means of top-down techniques; bottom-up approaches, instead, are, in general, unsuitable. In this work we present a proper adaptation of the magic-sets technique that aims at making query answering over positive finitary (normal) programs feasible by means of bottom-up techniques, i.e., those all current ASP systems rely on.

We extend arc consistency algorithms proposed in literature in order to deal with not fair valuation structures or not invertible semirings. As a result, consistency algorithms can now be used with partially ordered costs; for instance we can solve multicriteria Soft CSPs, where the Cartesian product of multiple semitings represents the optimization goal. To reach this objective, we first show that each semiring can be transformed into a new one where the + is instantiated with the Least Common Divisor (LCD) between the elements of the semiring set. The LCD value corresponds to the amount we can safely move from the binary constraint to the unary one in the consistency algorithm. At last, we propose an arc consistency algorithm which takes advantage of this operator.

In this paper, we study and compare three techniques based on Concurrent Constraint Programming to model biological systems: stochastic Concurrent Constraint Programming (sCCP), non-deterministic timed Concurrent Constraint (ntcc) and Hybrid Concurrent Constraint (Hcc). We analyses the peculiarities and drawbacks of the three languages considering as case study the biochemical reactions involved in the blood coagulation cascade. We also propose to integrate such languages as an extension of the soft concurrent constraint language. This will permit us to better handle quantitative and qualitative aspects of the biochemical reactions.

Normal Form Nested (NFN ) programs have recently been introduced in order to allow for a richer syntax in heads and bodies of logic programs with variables under the answer sets semantics. In particular, heads of rules can be disjunctions of conjunctions, while bodies can be conjunctions of disjunctions. Different to many other proposals of this kind, these programs may contain variables, and a notion of safety has been defined for guaranteeing domain independence. Moreover, previous results show that there is a polynomial translation from NFN programs to standard disjunctive logic programs (DLP ). In this system description we present the tool nfn2dlp, a compiler for NFN programs, which implements an efficient translation from safe NFN programs to safe DLP programs. The answer sets of the original NFN program can be obtained from the answer sets of the transformed program (which in turn can be obtained by using a DLP system) by a simple transformation. The system has been implemented using the object-oriented programming language Ruby and Treetop, a language for Parsing Expression Grammars (PEGs). It currently produces DLP programs in the format of DLV and can use DLV as a back-end.

Constraint solving problems (CSPs) represent a formalization of an important class of problems in computer science. We propose here a solving methodology based on the naming games. The naming game was introduced to represent N agents that have to bootstrap an agreement on a name to give to an object. The agents do not have a hierarchy and use a minimal protocol. Still they converge to a consistent state by using a distributed strategy. For this reason the naming game can be used to untangle distributed constraint solving problems (DCSPs). Moreover it represents a good starting point for a systematic study of DCSP methods, which can be seen as further improvement of this approach.

In this paper we present a dynamic heuristics that allows for improving the performance of a parallel instantiator algorithm based on the DLV system. In this system, each rule is rewritten in several “splits” of the same size that are assigned to a number of parallel instatiator subprocesses. The new heuristics allows for dynamically determining an optimal amount of work that has to be assigned to each parallel instantiator, and, thus, it improves the overall efficiency of the parallel evaluation. We implemented our heuristics and performed an experimental analysis that confirms the efficacy of the proposed method.

The Magic Sets rewriting technique (MS) consists in rewriting a logic program P with respect to a query Q in such a way that, the bottom-up evaluation of the rewritten program simulates the top-down of Q in the original program. In this way, only a restricted part of P is evaluated, thus obtaining valuable efficiency improvements. Many extensions and modifications of the base technique have been proposed in literature, but most of them are confined to the Datalog realm. In this paper we present an implementation of the Magic Set rewriting technique that is applicable to positive disjunctive logic programs with function symbols under the answer set semantics. We show how the base technique has to be modified when both disjunction in the rule heads and function symbols occur contemporarily in the input program. Finally, we describe our implementation of the technique, which is able to produce magic programs compatible with DLV syntax.

Following the approaches and motivations given in recent works about constructive interpretation of description logics, we introduce the constructive description logic KALC. This logic is based on a Kripke-style semantics inspired by the Kripke semantics for Intuitionistic first order logic. In the paper we present the main features of our semantics and we study its relations with other approaches. Moreover, we present a tableau calculus which turns out to be sound and complete for KALC.

In this paper we present the IDUM system, a successful application of logic programming to e-tourism. IDUM exploits two technologies that are based on the state-of-the-art ASP system DLV:(i) a system for ontology representation and reasoning, called OntoDLV; and, (ii) HiLεX a semantic information extraction tool. The core of IDUM is an ontology which models the domain of the touristic offers. The ontology is automatically populated by extracting the information contained in the touristic leaflets produced by tour operators. A set of specifically devised logic programs is used to reason on the information contained in the ontology for selecting the holiday packages that best fit the customer needs. An intuitive web-based user interface eases the task of interacting with the system for both the customers and the operators of a travel agency.

In this article we present an extension of the Soft Concurrent Constraint Programming language that guarantees a fair execution of the computation and that assure that no (enabled) agents will be never executed. The metric used in the paper to measure the execution of the processes is obtained by extending a carpooling algorithm.