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 switch from a Model-Centric to a Data-Centric mindset is putting emphasis on data and its quality rather than algorithms, bringing forward new challenges. In particular, the sensitive nature of the information in highly regulated scenarios needs to be accounted for. Specific approaches to address the privacy issue have been developed, as Privacy Enhancing Technologies. However, they frequently cause loss of information, putting forward a crucial trade-off among data quality and privacy. A clever way to bypass such a conundrum relies on Synthetic Data: data obtained from a generative process, learning the real data properties. Both Academia and Industry realized the importance of evaluating synthetic data quality: without all-round reliable metrics, the innovative data generation task has no proper objective function to maximize. Despite that, the topic remains under-explored. For this reason, we systematically catalog the important traits of synthetic data quality and privacy, and devise a specific methodology to test them. The result is DAISYnt (aDoption of Artificial Intelligence SYnthesis): a comprehensive suite of advanced tests, which sets a de facto standard for synthetic data evaluation. As a practical use-case, a variety of generative algorithms have been trained on real-world Credit Bureau Data. The best model has been assessed, using DAISYnt on the different synthetic replicas. Further potential uses, among others, entail auditing and fine-tuning of generative models or ensuring high quality of a given synthetic dataset. From a prescriptive viewpoint, eventually, DAISYnt may pave the way to synthetic data adoption in highly regulated domains, ranging from Finance to Healthcare, through Insurance and Education.

Risk assessment is an important decision support task in many domains, including health, engineering, process management, and economy. There is a growing interest in automated methods for risk assessment. These methods should be able to process information efficiently and with little user involvement. Currently, from the scientific literature in the health domain, there is availability of evidence-based knowledge about specific risk factors. On the other hand, there is no automatic procedure to exploit this available knowledge in order to create a general risk assessment tool which can combine the available quantitative data about risk factors and their impact on the corresponding risk. We present a Framework for the Assessment of Risk of adverse Events (FARE) and its first concrete applications FRAT-up and DRAT-up, which were used for fall and depression risk assessment in older persons and validated on four and three European epidemiological datasets, respectively. FARE consists of i) a novel formal ontology called On2Risk; and ii) a logical and probabilistic rule-based model. The ontology was designed to represent qualitative and quantitative data about risks in a general, structured and machine-readable manner so that this data may be concretely exploited by risk assessment algorithms. We describe the structure of the FARE model in the form of logic and probabilistic rules. We show how when starting from machine-readable data about risk factors, like the data contained in On2Risk, an instance of the algorithm can be automatically constructed and used to estimate the risk of an adverse event.

Assessing the risk to develop a specific disease is the first step towards prevention, both at individual and population levels. The development and validation of risk prediction models (RPMs) is the norm within different fields of medicine but still underused in psychiatry, despite the global impact of mental disorders. In particular, there is a lack of RPMs to assess the risk of developing depression, the first worldwide cause of disability and harbinger of functional decline in old age. We present the depression risk assessment tool DRAT-up, the first prospective RPM to identify late-life depression among community-dwelling subjects aged 60-75. The development of DRAT-up was based on appraisal of relevant literature, extraction of robust risk estimates, and integration into model parameters. A unique feature is the ability to estimate risk even in the presence of missing values. To assess the properties of DRAT-up, a validation study was conducted on three European cohorts, namely, the English Longitudinal Study of Ageing, the Invecchiare nel Chianti, and the Irish Longitudinal Study on Ageing, with 20 206, 1359, and 3124 eligible samples, respectively. The model yielded accurate risk estimation in the three datasets from a small number of predictors. The Brier scores were 0.054, 0.133, and 0.041, respectively, while the values of area under the curve (AUC) were 0.761, 0.736, and 0.768, respectively. Sensitivity analyses suggest robustness to missing values: setting any individual feature to unknown caused the Brier scores to increase by 0.004 and the AUCs to decrease by 0.045 in the worst cases. DRAT-up can be readily used for clinical purposes and to aid policy-making in the field of mental health.

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.

BACKGROUND: Recent Cochrane reviews on falls and fall prevention have shown that it is possible to prevent falls in older adults living in the community and in care facilities. Technologies aimed at fall detection, assessment, prediction and prevention are emerging, yet there has been no consistency in describing or reporting on interventions using technologies. With the growth of eHealth and data driven interventions, a common language and classification is required. OBJECTIVE: The FARSEEING Taxonomy of Technologies was developed as a tool for those in the field of biomedical informatics to classify and characterise components of studies and interventions. METHODS: The Taxonomy Development Group (TDG) comprised experts from across Europe. Through face-to-face meetings and contributions via email, five domains were developed, modified and agreed: Approach; Base; Components of outcome measures; Descriptors of technologies; and Evaluation. Each domain included sub-domains and categories with accompanying definitions. The classification system was tested against published papers and further amendments undertaken, including development of an online tool. Six papers were classified by the TDG with levels of consensus recorded. RESULTS: Testing the taxonomy with papers highlighted difficulties in definitions across international healthcare systems, together with differences of TDG members' backgrounds. Definitions were clarified and amended accordingly, but some difficulties remained. The taxonomy and manual were large documents leading to a lengthy classification process. The development of the online application enabled a much simpler classification process, as categories and definitions appeared only when relevant. Overall consensus for the classified papers was 70.66%. Consensus scores increased as modifications were made to the taxonomy. CONCLUSION: The FARSEEING Taxonomy of Technologies presents a common language, which should now be adopted in the field of biomedical informatics. In developing the taxonomy as an online tool, it has become possible to continue to develop and modify the classification system to incorporate new technologies and interventions.

Fall risk assessment is important for fall prediction and fall prevention among older adults. In order to be applied in clinical practice, a fall risk assessment tool need to be regarded useful. The aim of this study was to evaluate healthcare professionals' user experience (UX) of the Fall Risk Assessment Tool (FRAT-up). Eight health care professionals working in a geriatric hospital department or in the primary health care system participated in a focus group and evaluated the tool. The healthcare professionals considered the FRAT-up tool to be novel and considered it useful in clinical practice. The tool can be used to get an extended knowledge and understanding of how to individually tailor a fall prevention intervention. It is suggested that for a better experience, the scale should be simplified and the tool should be integrated with the patient's medical record.

About one-third of persons over 65 are subject to at least one fall during a year, and many of them are subjected to health, psychological and financial consequences. A requirement to improve the effectiveness of preventive interventions is to timely identify subjects at higher risk. In this work we introduce the Farseeing Fall Risk Assessment Tool (FRAT-up), a software tool for evaluating the fall risk of a subject, based on known risk factors. The tool is based on probabilistic rules, generated automatically from a light ontology capturing the scientific findings about risk factors. FRAT-up has been tested on the In CHIANTI dataset, showing performances comparable with state-of-the-art tools.

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.

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.

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