T1a: Automated Theorem Proving in the First-order TPTP World (Geoff Sutcliffe, University of Miami)
9:00 - 10:30, Thursday, 19th October
ABSTRACT: The TPTP World is a well known and established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems for classical logics. The data, standards, and services provided by the TPTP World have made it increasingly easy to build, test, and apply ATP technology. This tutorial reviews the core features of the TPTP World, describes key service components of the TPTP World and how to use them for automated reasoning in first-order logic. Bring a laptop!
T1b: Automated Reasoning in Higher-order and Non-classical Logics (Christoph Benzmüller, FU Berlin)
11:00 - 12:30, Thursday, 19th October
ABSTRACT: In this tutorial, I will demonstrate a generic approach to automate a wide range of non-classical logics (propositional and quantified) using theorem proving systems for classical higher-order logic (HOL). Our particular focus in this tutorial will be on (quantified) modal and deontic logics. We will present shallow semantical embeddings of such logics in meta-logic HOL. One motivation thereby is to turn off-the-shelf proof assistants for HOL, such as Isabelle/HOL, into proof assistants for these object logics in such a way that both intuitive interactive proof as well as proof automation are supported. Additionally, TPTP compliant automated theorem proving systems (such as LEO-II) can be used for reasoning in the embedded object logics, either directly or indirectly from systems like Isabelle/HOL via the Sledgehammer tool.
T2: Affective Computing and Virtual Agents (Christine Lisetti, Florida International University)
14:00 - 16:00, Thursday, 19th October
ABSTRACT: Affective computing explores the computational nature of affective phenomena, such as emotions, moods, personality, and attitudes, and their role in human intelligence, communication and decision-making. Affective computing research is highly interdisciplinary in nature: it lies at the intersection of Artificial Intelligence (AI) and Human-Computer Interaction (HCI) from computer science, emotion theories from Psychology, and social interaction theory from Communication. Insights derived from affective computing research have been applied to build virtual social agents that can interact naturally with humans with verbal and non-verbal communication, in a variety of contexts involving socio-emotional content, e.g., health counseling, computer games, intelligent tutoring systems. In this tutorial, we will study some of the main topics involved in building socially and emotionally competent virtual agents, that can:
- sense the affect, preferences, and personality of their interlocutor
- make decisions that are socially acceptable
- interact with humans within the domain knowledge
- display some emotional and social competence
- learn to tailor and adapt their interactive styles