Artificial Intelligence (AI) has gradually attracted attention in the field of artistic creation, resulting in a debate on the evaluation of AI artistic outputs. However, there is a lack of common criteria for objective artistic evaluation both of human and AI creations. This is a frequent issue in the field of dance, where different performance metrics focus either on evaluating human or computational skills separately. This work proposes a methodological approach for the artistic evaluation of both AI and human artistic creations in the field of robotic dance. First, we define a series of common initial constraints to create robotic dance choreographies in a balanced initial setting, in collaboration with a group of human dancers and choreographer. Then, we compare both creation processes through a human audience evaluation. Finally, we investigate which choreography aspects (e.g., the music genre) have the largest impact on the evaluation, and we provide useful guidelines and future research directions for the analysis of interconnections between AI and human dance creation.

Despite the indisputable progresses of artificial intelligence, some tasks that are rather easy for a human being are still challenging for a machine. An emblematic example is the resolution of mathematical puzzles with diagrams. Sub-symbolical approaches have proven successful in fields like image recognition and natural language processing, but the combination of these techniques into a multimodal approach towards the identification of the puzzle’s answer appears to be a matter of reasoning, more suitable for the application of a symbolic technique. In this work, we employ logic programming to perform spatial reasoning on the puzzle’s diagram and integrate the deriving knowledge into the solving process. Analysing the resolution strategies required by the puzzles of an international competition for humans, we draw the design principles of a Prolog reasoning library, which interacts with image processing software to formulate the puzzle’s constraints. The library integrates the knowledge from different sources, and relies on the Prolog inference engine to provide the answer. This work can be considered as a first step towards the ambitious goal of a machine autonomously solving a problem in a generic context starting from its textual-graphical presentation. An ability that can help potentially every human–machine interaction.

As the need to understand and formalise business processes into a model has grown over the last years, the process discovery research field has gained more and more importance, developing two different classes of approaches to model representation: procedural and declarative. Orthogonally to this classification, the vast majority of works envisage the discovery task as a one-class supervised learning process guided by the traces that are recorded into an input log. In this work instead, we focus on declarative processes and embrace the less-popular view of process discovery as a binary supervised learning task, where the input log reports both examples of the normal system execution, and traces representing a “stranger” behaviour according to the domain semantics. We therefore deepen how the valuable information brought by both these two sets can be extracted and formalised into a model that is “optimal” according to user-defined goals. Our approach, namelyNegDis, is evaluated w.r.t. other relevant works in this field, and shows promising results regarding both the performance and the quality of the obtained solution.

The compliance verification task amounts to establishing if the execution of a system, given in terms of observed happened events, does respect a given property. In the past both the frameworks of Temporal Logics and Logic Programming have been extensively exploited to assess compliance in differen t domains, such as normative multi-agent systems, business process management and service oriented computing. In this work we review the LTL and SCIFF frameworks in the light of compliance evaluation, and formally investigate the relationship between the two approaches. We define a notion of compliance within each approach, and then we show that an arbitrary LTL formula can be expressed in SCIFF, by providing a translation procedure from LTL to SCIFF which preserves compliance.

The capability to store data about Business Process (BP) executions in so-called Event Logs has brought to the identification of a range of key reasoning services (consistency, compliance, runtime monitoring, prediction) for the analysis of process executions and process models. Tools for the provi sion of these services typically focus on one form of reasoning alone. Moreover, they are often very rigid in dealing with forms of incomplete information about the process execution. While this enables the development of ad hoc solutions, it also poses an obstacle for the adoption of reasoning-based solutions in the BP community. In this paper, we introduce the notion of Structured Processes with Observability and Time (SPOT models), able to support incompleteness (of traces and logs), and temporal constraints on the activity duration and between activities. Then, we exploit the power of abduction to provide a flexible, yet computationally effective framework able to reinterpret key reasoning services in terms of incompleteness and observability in a uniform way.

Deep networks have been successfully applied to a wide range of tasks in artificial intelligence, and game playing is certainly not an exception. In this paper, we present an experimental study to assess whether purely subsymbolic systems, such as deep networks, are capable of learning to play by the rules, without anya prioriknowledge neither of the game, nor of its rules, but only by observing the matches played by another player. Similar problems arise in many other application domains, where the goal is to learn rules, policies, behaviors, or decisions, simply by the observation of the dynamics of a system. We present a case study conducted with residual networks on the popular board game ofNine Men's Morris, showing that this kind of subsymbolic architecture is capable of correctly discriminating legal from illegal decisions, just from the observation of past matches of a single player.

The adoption of mobile devices and sensors, and the Internet of Things trend, are making available a huge quantity of information that needs to be analyzed. Distributed architectures, such as Map Reduce, are indeed providing technical answers to the challenge of processing these big data. Due to the distributed nature of these solutions, it can be difficult to guarantee the Quality of Service: e.g., it might be not possible to ensure that processing tasks are performed within a temporal deadline, due to specificities of the infrastructure or processed data itself. However, relaying on cloud infrastructures, distributed applications for data processing can easily be provided with additional resources, such as the dynamic provisioning of computational nodes. In this paper, we focus on the step of monitoring Map Reduce applications, to detect situations where resources are needed to meet the deadlines. To this end, we exploit some techniques and tools developed in the research field of Business Process Management: in particular, we focus on declarative languages and tools for monitoring the execution of business process. We introduce a distributed architecture where a logic-based monitor is able to detect possible delays, and trigger recovery actions such as the dynamic provisioning of further resources.

The capability to store data about Business Process executions in so-called Event Logs has brought to the identification of a range of key reasoning services (consistency, compliance, runtime monitoring, prediction) for the analysis of process executions and process models. Tools for the provision of these services typically focus on one form of reasoning alone. Moreover, they are often very rigid in dealing with forms of incomplete information about the process execution. While this enables the development of ad hoc solutions, it also poses an obstacle for the adoption of reasoning-based solutions. In this paper we exploit the power of abduction to provide a flexible, and yet computationally effective framework able to reinterpret key reasoning services in terms of incompleteness and observability in a uniform and effective way.

In many countries of the world, the life expectancy increases but the population ages so rapidly that it is expected that soon it will be difficult to ensure a good life quality to the elder people when health issues arise. In this paper, we consider this problem from the point of view of the physiotherapy rehabilitation which nowadays is perceived as costly and inconvenient for the elder patients. In order to lessen these problems, we propose a distributed architecture to allow the physiotherapists to remotely assist their patients while they comfortably do exercises from home. As in other proposals, the Human Pose Recognition is delegated to a computer equipped with MS Kinect and neural networks. Our approach, however, differs from others because it includes a logical framework based on Event Calculus augmented with Expectations which provides a higher-level description of the exercises and a mean to measure how well they were done.

Today, large business processes are composed of smaller, autonomous, interconnected subsystems, achieving modularity and robustness. Quite often, these large processes comprise software components as well as human actors, they face highly dynamic environments and their subsystems are updated and evolve independently of each other. Due to their dynamic nature and complexity, it might be difficult, if not impossible, to ensure at design-time that such systems will always exhibit the desired/expected behaviors. This, in turn, triggers the need for runtime verification and monitoring facilities. These are needed to check whether the actual behavior complies with expected business constraints, internal/external regulations and desired best practices. In this work, we present Mobucon EC, a novel monitoring framework that tracks streams of events and continuously determines the state of business constraints. In Mobucon EC, business constraints are defined using the declarative language Declare. For the purpose of this work, Declare has been suitably extended to support quantitative time constraints and non-atomic, durative activities. The logic-based language Event Calculus (EC) has been adopted to provide a formal specification and semantics to Declare constraints, while a light-weight, logic programming-based EC tool supports dynamically reasoning about partial, evolving execution traces. To demonstrate the applicability of our approach, we describe a case study about maritime safety and security and provide a synthetic benchmark to evaluate its scalability.

We propose $${\mathcal{B}}$$ -Tropos as a modeling framework to support agent-oriented systems engineering, from high-level requirements elicitation down to execution-level tasks. In particular, we show how $${\mathcal{B}}$$ -Tropos extends the Tropos methodology by means of declarative business constraints, inspired by the ConDec graphical language. We demonstrate the functioning of $${\mathcal{B}}$$ -Tropos using a running example inspired by a real-world industrial scenario, and we describe how $${\mathcal{B}}$$ -Tropos models can be automatically formalized in computational logic, discussing formal properties of the resulting framework and its verification capabilities.

Despite their dynamic nature, social commitments have rarely been used for monitoring purposes. Little attention has been paid to the relationship between commitments and the temporal dimension and to the corresponding run-time verification. Building on previous work, we present a declarative axiomatization of time-aware social commitments, extending their basic life cycle with time-related transitions and compensation mechanisms. The formalization is based on a reactive version of the event calculus, able to monitor the commitment's evolution during a system's execution, to check whether the interacting agents are honoring them or not. The resulting monitoring framework can be used in the context of agent-based simulation, either to dynamically evaluate whether a running simulation is compliant with a commitment-based contract or to provide useful information to the interacting agents, helping them to behave in a compliant manner.

Since its introduction, the Event Calculus (ℰ𝒞) 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 formalization inside logic-based frameworks has been

We discuss the static verification of declarative Business Processes. We identify four desiderata about verifiers, and propose a concrete framework which satisfies them. The framework is based on the ConDec graphical notation for modeling Business Processes, and on Abductive Logic Programming technology for verification of properties. Empirical evidence shows that our verification method seems to perform and scale better, in most cases, than other state of the art techniques (model checkers, in particular). A detailed study of our framework’s theoretical properties proves that our approach is sound and complete when applied to ConDec models that do not contain loops, and it is guaranteed to terminate when applied to models that contain loops.

The RETE algorithm is a very efficient option for the development of a rule-based system, but it supports only boolean, first order logic. Many real-world contexts, instead, require some degree of vagueness or uncertainty to be handled in a robust and efficient manner, imposing a trade-off between the number of rules and the cases that can be handled with sufficient accuracy. Thus, in the first part of the paper, an extension of RETE networks is proposed, capable of handling a more general inferential process, which actually includes several types of schemes for reasoning with imperfect information. In particular, the architecture depends on a number of configuration parameters which could be set by the user, individually or as a whole for the entire rule base. The second part, then, shows how an appropriate combination of parameters can be used to emulate some of the most common, specialized engines: 3-valued logic, classical certainty factors, fuzzy, many-valued logic and Bayesian networks.

Service-oriented computing, an emerging paradigm for architecting and implementing business collaborations within and across organizational boundaries, is currently of interest to both software vendors and scientists. While the technologies for implementing and interconnecting basic services are reaching a good level of maturity, modeling service interaction from a global viewpoint, that is, representing service choreographies, is still an open challenge. The main problem is that, although declarativeness has been identified as a key feature, several proposed approaches specify choreographies by focusing on procedural aspects, leading to over-constrained and over-specified models. To overcome these limits, we propose to adopt DecSerFlow, a truly declarative language, to model choreographies. Thanks to its declarative nature, DecSerFlow semantics can be given in terms of logic-based languages. In particular, we present how DecSerFlow can be mapped ontoLinear Temporal Logicand ontoAbductive Logic Programming. We show how the mappings onto both formalisms can be concretely exploited to address the enactment of DecSerFlow models, to enrich its expressiveness and to perform a variety of different verification tasks. We illustrate the advantages of using a declarative language in conjunction with logic-based semantics by applying our approach to a running example.

In semantic Web technologies, searching for a service means to identify components that can potentially satisfy the user needs in terms of outputs and effects (discovery), and that, when invoked by the customer, can fruitfully interact with her (contracting). In this paper, we present an application framework that encompasses both the discovery and the contracting steps, in a unified search process. In particular, we accommodate service discovery by ontology-based reasoning, and contracting by automated reasoning about policies published in a formal language. To this purpose, we consider a formal approach grounded on computational logic, and abductive logic programming in particular. We propose a framework, called SCIFF reasoning engine, able to establish, by ontological and abductive reasoning, if a semantic Web service and a requester can fruitfully inter-operate, taking as input the behavioral interfaces of both the participants, and producing as output a sort of a contract.

SCIFF is a framework thought to specify and verify interaction in open agent societies. The SCIFF language is equipped with a semantics based on abductive logic programming; SCIFF's operational component is a new abductive logic programming proof procedure, also named SCIFF, for reasoning with expectations in dynamic environments. In this article we present the declarative and operational semantics of the SCIFF language, and the termination, soundness, and completeness results of the SCIFF proof procedure, and we demonstrate SCIFF's possible application in the multiagent domain.

Although stemming from very different research areas, Multi-Agent Systems (MAS) and Service Oriented Computing (SOC) share common topics, problems and settings. One of the common problems is the need to formally verify the conformance of individuals (Agents or Web Services) to common rules and specifications (resp. Protocols/Choreographies), in order to provide a coherent behaviour and to reach the goals of the user.In previous publications, we developed a framework, SCIFF, for the automatic verification of compliance of agents to protocols. The framework includes a language based on abductive logic programming and on constraint logic programming for formally defining the social rules; suitable proof-procedures to check on-the-fly and a-priori the compliance of agents to protocols have been defined.Building on our experience in the MAS area, in this paper we make a first step towards the formal verification of web services conformance to choreographies. We adapt the SCIFF\ framework for the new settings, and propose a heir of SCIFF, the framework AlLoWS (Abductive Logic Web-service Specification).. AlLoWS comes with a language for defining formally a choreography and a web service specification. As its ancestor, AlLoWS has a declarative and an operational semantics. We show examples of how AlLoWS deals correctly with interaction patterns previously identified. Moreover, thanks to its constraint-based semantics, AlLoWS deals seamlessly with other cases involving constraints and deadlines

The monitoring and detection of nosocomial infections is a very important problem arising in hospitals. A hospital-acquired or nosocomial infection is a disease that develops after admission into the hospital and it is the consequence of a treatment, not necessarily a surgical one, performed by the medical staff. Nosocomial infections are dangerous because they are caused by bacteria which have dangerous (critical) resistance to antibiotics. This problem is very serious all over the world. In Italy, almost 5-8% of the patients admitted into hospitals develop this kind of infection. In order to reduce this figure, policies for controlling infections should be adopted by medical practitioners. In order to support them in this complex task, we have developed a system, called MERCURIO, capable of managing different aspects of the problem. The objectives of this system are the validation of microbiological data and the creation of a real time epidemiological information system. The system is useful for laboratory physicians, because it supports them in the execution of the microbiological analyses; for clinicians, because it supports them in the definition of the prophylaxis, of the most suitable antibi-otic therapy and in monitoring patients' infections; and for epidemiologists, because it allows them to identify outbreaks and to study infection dynamics. In order to achieve these objectives, we have adopted expert system and data mining techniques. We have also integrated a statistical module that monitors the diffusion of nosocomial infections over time in the hospital, and that strictly interacts with the knowledge based module. Data mining techniques have been used for improving the system knowledge base. The knowledge discovery process is not antithetic, but complementary to the one based on manual knowledge elicitation. In order to verify the reliability of the tasks performed by MERCURIO and the usefulness of the knowledge discovery approach, we performed a test based on a dataset of real infection events. In the validation task MERCURIO achieved an accuracy of 98.5%, a sensitivity of 98.5% and a specificity of 99%. In the therapy suggestion task, MERCURIO achieved very high accuracy and specificity as well. The executed test provided many insights to experts, too (we discovered some of their mistakes). The knowledge discovery approach was very effective in validating part of the MERCURIO knowledge base, and also in extending it with new validation rules, confirmed by interviewed microbiologists and specific to the hospital laboratory under consideration.

We propose to adopt a formalism, based on social integrity constraints (ICs), for specifying social interactions between actors involved in a guideline. ICs allow us to represent interaction protocols using a logic formalism and to perform an on-the-fly verification of the protocol's application compliance, based on an abductive proof procedure which operates on relevant events occurred during its application. The paper presents the results of a first trial performed on a microbiological clinical guideline which exploits the potentialities of the formalism in representing and verifying the compliance to medical guidelines.

Constraint Logic Programming languages on Finite Domains, CLP( FD ), provide a declarative framework for Artificial Intelligence problems. However, in many real life cases, domains are not known and must be acquired or computed. In systems that interact with the outer world, domain elements synthesize information on the environment, they are not all known at the beginning of the computation, and must be retrieved through an expensive acquisition process.In this article, we extend the CLP( FD ) language by combining it with a new sort (called Incrementally specified Sets, I-Set ). In the resulting language, CLP( FD + I-Set ), FD variables can be defined on partially or fully unknown domains ( I-Set ). Domains can be linked each other through relations, and constraints can be imposed on them. We describe a propagation algorithm (called Known Arc Consistency (KAC)) based on known domain elements, and theoretically compare it with arc-consistency.The language can be implemented on top of different CLP systems, thus letting the user exploit different possible semantics for domains (e.g., lists, sets or streams). We state the specifications that the employed system should provide, and we show that two different CLP systems (Conjunto and { log }) can be effectively used.We provide motivating examples and describe promising applications.

In classical CLP(FD) systems, domains of variables are completely known at the beginning of the constraint propagation process. However, in systems interacting with an external environment, acquiring the whole domains of variables before the beginning of constraint propagation may cause waste of computation time, or even obsolescence of the acquired data at the time of use. For such cases, the Interactive Constraint Satisfaction Problem (ICSP) model has been proposed (Cucchiara et al. 1999a) as an extension of the CSP model, to make it possible to start constraint propagation even when domains are not fully known, performing acquisition of domain elements only when necessary, and without the need for restarting the propagation after every acquisition. In this paper, we show how a solver for the two sorted CLP language, defined in previous work (Gavanelli et al. 2005) to express ICSPs, has been implemented in the Constraint Handling Rules (CHR) language, a declarative language particularly suitable for high level implementation of constraint solvers.

We present a tool for measuring the Function Point (FP) software metric from the specification of a software system expressed in the form of an Entity Relationship (ER) diagram plus a Data Flow Diagram (DFD). First, the informal and general FP counting rules are translated into rigorous rules expressing properties of the ER–DFD. Then, the rigorous rules are translated into Prolog. The measures given by the system on a number of case studies are in accordance with those of human experts.

We describe a knowledge based system for microbiological laboratory data validation and \nbacteria infections monitoring. The knowledge base has been obtained from international \nstandard guidelines for microbiological laboratory practice, from experts’ suggestions and \nfrom data mining. In this work, we evaluate the system in terms of accuracy on a test dataset.

The paper presents an approach for detecting vehicles in urban traffic scenes by means of rule-based reasoning on visual data. The strength of the approach is its formal separation between the low-level image processing modules and the high-level module, which provides a general-purpose knowledge-based framework for tracking vehicles in the scene. The image-processing modules extract visual data from the scene by spatio-temporal analysis during daytime, and by morphological analysis of headlights at night. The high-level module is designed as a forward chaining production rule system, working on symbolic data, i.e., vehicles and their attributes (area, pattern, direction, and others) and exploiting a set of heuristic rules tuned to urban traffic conditions. The synergy between the artificial intelligence techniques of the high-level and the low-level image analysis techniques provides the system with flexibility and robustness.

In this paper, we investigate the possibility of integrating Artificial Intelligence (AI) and Operations Research (OR) techniques for solving the Crew Rostering Problem (CRP). CRP calls for the optimal sequencing of a given set of duties into rosters satisfying a set of constraints. The optimality criterion requires the minimization of the number of crews needed to cover the duties. This kind of problem has been traditionally solved by OR techniques. In recent years, a new programming paradigm based on Logic Programming, named Constraint Logic Programming (CLP), has been successfully used for solving hard combinatorial optimization problems. CLP maintains all the advantages of logic programming such as declarativeness, non-determinism and an incremental style of programming, while overcoming its limitations, mainly due to the inefficiency in exploring the search space. CLP achieves good results on hard combinatorial optimization problems which, however, are not comparable with those achieved by OR approaches. Therefore, we integrate both techniques in order to design an effective heuristic algorithm for CRP which fully exploits the advantages of the two methodologies: on the one hand, we maintain the declarativeness of CLP, its ease of representing knowledge and its rapid prototyping; on the other hand, we inherit from OR some efficient procedures based on a mathematical approach to the problem. Finally, we compare the results we achieved by means of the integration with those obtained by a pure OR approach, showing that AI and OR techniques for hard combinatorial optimization problems can be effectively integrated. © 1998 John Wiley & Sons, Ltd.

The assumption-based truth maintenance system (ATMS) is a reasoning maintenance system proved useful in many applications and fields such as diagnosis and abductive reasoning. However, one limitation of the ATMS is that it handles propositional justifications only. There are problems, instead, where one has to move to the first-order predicate calculus, and explicitly consider variables. In this paper, we present an extension of the basic ATMS where justifications are definite Horn clauses possibly containing variables, and non-ground terms can occur in ATMS data structures. To maintain the incrementality feature peculiar to the ATMS, we extend the basic label-updating algorithm from the propositional case to the first-order one. In this way, we obtain a system able to produce, for a given atomic formula, the set of minimal hypotheses (possibly containing variables) we have to add to a given theory to prove this formula. We show how this extension relates to logic programs when they are optimized through partial evaluation.

Structuring logic programs to deal with evolving and incomplete knowledge is one of the main issues in representing knowledge with logic. On the one hand, evolving knowledge in logic programming can be modelled through suitable operators for the dynamic composition of separate programs. On the other hand, when dealing with dynamic compositions of logic programs, the open world assumption adequately models the aspects of incompleteness of knowledge. We analyse the notion of open program along with suitable operators for composing and closing programs. We present the semantics of open programs and of the associated operators in two different, equivalent styles. We define a model-theoretic semantics in terms of Herbrand models, while an operational semantics is given by means of inference rules. In the second part of the paper, we explore some applications of open programs and of their compositions. We show how a number of policies for structuring logic programming can be reconstructed in this setting, including the construction of modules with import declarations. Finally, the relations between open programs and abductive logic programming are discussed.

Abstract By using practical examples, this paper outlines the power of reflection mechanisms for logic programming systems in the domain of knowledge structuring. In particular, it presents an extension of Prolog, where separate databases can be handled as first‐class objects. Different forms of database combination such as inheritance and dynamic context extension/contraction are specified and implemented in a dynamic and flexible way through reflection. The main aim is to broaden the application area of logic programming to encompass most of the paradigms needed by systems that use artificial intelligence techniques. Practical results presented in the paper show that logic programs that use reflection can be shorter, more readable and efficient than those using more conventional full meta‐interpretation techniques. Full meta‐interpretation, however, is more general than reflection.