The development of applications with intelligent virtual agents (IVA) often comes with integration of multiple complex components. In this article we present the Agents United Platform: an open source platform that researchers and developers can use as a starting point to setup their own multi-IVA applications.

This paper presents progress and challenges in developing a platform for multi-character, argumentation based, interaction with a group of virtual coaches for healthcare advice and promotion of healthy behaviours. Several challenges arise in the development of such a platform, e.g., choosing the most effective way of utilising argumentation between the coaches with multiple perspectives, handling the presentation of these perspectives and finally, the personalisation and adaptation of the platform to the user types. In this paper, we present the three main challenges recognized, and show how we aim to address these.

Goal-setting is a frequently adopted strategy in behaviour change coaching. When setting a goal, it is important that it is understood and agreed upon by all parties, and not simply accepted as-is. We present here a dialogue game for multi-party goal-setting, in which multiple health coaches can contribute in order to find a goal that is acceptable to both the patient, and the coaches themselves. Our proposed game incorporates three important aspects of goal-setting and health coaching, (1) coaches can query each other's proposed goals, (2) the patient takes ownership of the goal, and (3) the patient themselves can propose goals.

A modern way of life needs a modern way of coaching. Despite the proliferation of ICT solutions for personalized health care, there is still no easy way to provide older adults with integrated coaching services. In this paper we introduce the concept of Council of Coaches — a radically new virtual coaching concept based on multiple autonomous, embodied virtual coaches, which form together a personal council that fulfills the needs of older adults in an integrated way. In this concept, coaching takes the form of an open dialog in which clients co-construct together with a selected number of coaches their own plans to go for a healthier lifestyle. Virtual coaches are presented to users by means of embodied conversational social characters. We discuss technical and social challenges on the path towards realizing the Council of Coaches concept, a radically new view of health coaching that involves the state of the art in human-computer interaction, natural dialogue, and argumentation technology.

Virtual humans need to be persuasive in order to promote behaviour change in human users. While several studies have focused on understanding the numerous aspects that influence the degree of persuasion, most of them are limited to dyadic interactions. In this paper, we present an evaluation study focused on understanding the effects of multiple agents on user's persuasion. Along with gender and status (authoritative & peer), we also look at type of focus employed by the agent i. e., user-directed where the agent aims to persuade by addressing the user directly and vicarious where the agent aims to persuade the user, who is an observer, indirectly by engaging another agent in the discussion. Participants were randomly assigned to one of the 12 conditions and presented with a persuasive message by one or several virtual agents. A questionnaire was used to measure perceived interpersonal attitude, credibility and persuasion. Results indicate that credibility positively affects persuasion. In general, multiple agent setting, irrespective of the focus, was more persuasive than single agent setting. Although, participants favored user-directed setting and reported it to be persuasive and had an increased level of trust in the agents, the actual change in persuasion score reflects that vicarious setting was the most effective in inducing behaviour change. In addition to this, the study also revealed that authoritative agents were the most persuasive.

The simulation of mathematical reasoning has been a driving force throughout the history of Artificial Intelligence research. However, despite significant successes in computer mathematics, computers are not widely used by mathematicians apart from their quotidian applications. An oft-cited reason for this is that current computational systems cannot do mathematics in the way that humans do. We draw on two areas in which Automated Theorem Proving (ATP) is currently unlike human mathematics: firstly in a focus on soundness, rather than understandability of proof, and secondly in social aspects. Employing techniques and tools from argumentation to build a framework for mixed-initiative collaboration, we develop three complementary arcs. In the first arc – our theoretical model – we interpret the informal logic of mathematical discovery proposed by Lakatos, a philosopher of mathematics, through the lens of dialogue game theory and in particular as a dialogue game ranging over structures of argumentation. In our second arc – our abstraction level – we develop structured arguments, from which we induce abstract argumentation systems and compute the argumentation semantics to provide labelings of the acceptability status of each argument. The output from this stage corresponds to a final, or currently accepted proof artefact, which can be viewed alongside its historical development. Finally, in the third arc – our computational model – we show how each of these formal steps is available in implementation. In an appendix, we demonstrate our approach with a formal, implemented example of real-world mathematical collaboration. We conclude the paper with reflections on our mixed-initiative collaborative approach.

We present a dialogue game representation of Lakatos's theory of justification and discovery in mathematics and describe our implementation of the game. As well as demonstrating a new domain for dialogue games, this could provide the basis for systems which can be used to aid mathematicians in their work.

Abstract Refinement is a powerful mechanism for mastering the complexities that arise when formally modelling systems. Refinement also brings with it additional proof obligations—requiring a developer to discover properties relating to their design decisions. With the goal of reducing this burden, we have investigated how a general purpose automated theory formation tool, HR, can be used to automate the discovery of such properties within the context of the Event-B formal modelling framework. This gave rise to an integrated approach to automated invariant discovery. In addition to formal modelling and automated theory formation, our approach relies upon the simulation of system models as a key input to the invariant discovery process. Moreover we have developed a set of heuristics which, when coupled with automated proof-failure analysis, have enabled us to effectively tailor HR to the needs of Event-B developments. Drawing in part upon case study material from the literature, we have achieved some promising experimental results. While our focus has been on Event-B, we believe that our approach could be applied more widely to formal modelling frameworks which support simulation.