Intelligent Robotics International Symposium

Abstracts

"Constructive reverse mathematics: an introduction and recent results"
(by Ishihara)

Abstract: We review some results in Friedman-Simpson program, classical reverse mathematics, and axioms and their consequences in varieties of constructive mathematics: intuitionistic mathematics, constructive recursive mathematics and Bishop's constructive mathematics. Then we propose constructive reverse mathematics with countable choice to classify theorems in the varieties of constructive mathematics by logical principles etc., and we refine it without assuming countable choice to compare some results in constructive reverse mathematics with results in classical reverse mathematics. Finally, we present some recent results on the binary expansion and the intermediate value theorem.


Separating convex sets (joint work with Gregor Svindland)
(by Berger)

Abstract: It is well-known that two disjoint compact convex sets can be strictly separated by a linear functional. We discuss to which extent this functional can be effectively constructed.


Constructive existence via the Minimalist Foundation
(by Maietti)

Abstract: A key distinct feature of constructive mathematics is that its provable existential statements are equipped with a program computing their witness.

By using the two-level structure of the Minimalist Foundation for constructive mathematics introduced in joint work with G. Sambin in [3] and completed in [1], we analyze various formulations of existential quantification in constructive type theory.

Then, by using [2] we relate them to choice principles and by using [4] also to extraction of programs from constructive proofs.

[1] M.E. Maietti. A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic, 160(3):319-354, 2009.

[2] M.E. Maietti and G. Rosolini. Relating quotient completions via categorical logic. In Dieter Probst and Peter Schuster (eds.), "Concepts of Proof in Mathematics, Philosophy, and Computer Science". Ontos Mathematical Logic. Walter de Gruyter, Berlin. To appear.

[3] M.E. Maietti and G Sambin. Toward a minimalist foundation for constructive mathematics. In L. Crosilla and P. Schuster, editor, From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics, number 48 in Oxford Logic Guides, pages 91-114. Oxford University Press, 2005.

[4] M.E. Maietti and S. Maschio. An extensional Kleene realizability semantics for the Minimalist Foundation. In Post-proceedings TYPES'14 in Leibniz International Proceedings in Informatics (LIPIcs), 2015


An Algebra for graphs with bounded tree width: axiomatization, WQO, and regularity
(by Ogawa)

Abstract: TBD


Untyped Confluence In Dependent Type Theories
(by Jouannaud)

Abstract:We investigate techniques based on van Oostrom's decreasing diagrams that reduce confluence proofs to the checking of critical pairs in the absence of termination properties, which are useful in dependent type calculi to prove confluence on untyped terms. These techniques are applied to a complex example originating from practice: a faithful encoding, in an extension of LF with rewrite rules on objects and types, of a subset of the calculus of inductive constructions with a cumulative hierarchy of predicative universes above Prop. The rules may be first-order or higher-order, plain or modulo, non-linear on the right or on the left. The first-order rules are assumed terminating and confluent modulo some theory, while the higher-order ones --which contain beta-reduction-- are assumed to be non-terminating and their parallel critical pairs must satisfy a versoion of van Oostrom's decreasing diagram condition. The variables which are non-linear in lefthand sides are assumed to take their values in confined basic subtypes (in our example, the natural numbers).


Verification of some algorithms within self-modifying programs
(by Bonfante)

Abstract: TBD


On Predicate Refinement Heuristics in Program Verification with CEGAR
(by Terauchi)

Abstract: Many of the modern program verifiers are based on the predicate abstraction with CEGAR method, The method looks for a sufficient inductive invariant to prove the given property of the given program by iteratively accumulating predicates that are obtained by analyzing spurious counterexamples, and predicate refinement heuristics like Craig interpolation are used for this purpose. In this talk, we overview our recent work on predicate refinement heuristics in CEGAR. Specifically, we show that a certain strategy for choosing predicates can guarantee the convergence of CEGAR at a modest cost. We also show that choosing small refinements guarantees fast convergence under certain conditions.


Analysing Logical Structures of Legal Texts and Its Application
(by Nguyen)

Abstract: Analyzing logical structures of texts is important to understanding natural language, especially in the legal domain, where legal texts have their own specific characteristics. Recognizing logical structures in legal texts does not only help people in understanding legal documents, but also in supporting other tasks in legal text processing.

In this talk, we present a new task, learning logical structures of paragraphs in legal articles, which is studied in research on Legal Engineering. The goals of this task are recognizing logical parts of law sentences in a paragraph, and then grouping related logical parts into some logical structures of formulas, which describe logical relations between logical parts.

We present a two-phase framework to learn logical structures of paragraphs in legal articles. In the first phase, we model the problem of recognizing logical parts in law sentences as a multi-layer sequence learning problem, and present a CRF-based model to recognize them. In the second phase, we propose a graph-based method to group logical parts into logical structures. We consider the problem of finding a subset of complete subgraphs in a weighted-edge complete graph, where each node corresponds to a logical part, and a complete subgraph corresponds to a logical structure. We also present an integer linear programming formulation for this optimization problem.

In addition to show the advantages of analyzing legal structure, we present an application of question answering and textual entailment recognition for the legal domain. We present our system participated in COLIFE 2015 competition.


From Computational Linguistics to Computational Socio-Linguistics: Predicting Review Helpfulness and Predicting Power Relationships in Social Networks
(by Ittoo)

Abstract: My talk will be divided into 2 parts, each focusing on a research area that I am currently pursuing in the domain of Natural Language Processing (NLP). The 2 areas can be broadly classified as “computational socio-linguistics”.

The first research stream has its roots in the well-known and now mature area of opinion mining/sentiment analysis. While there has been a plethora of earlier studies devoted to the development of opinion mining techniques, the key question of what makes a customer review helpful/useful has been largely overlooked. This is the question that I plan to address in this talk. In particular, I will describe several machine learning approaches, using SVM and Random Forest, which attempt to exploit deep linguistic features, such as argumentative patterns, to predict review helpfulness. Datasets include reviews from Amazon.com and Yelp.

The second research stream is still nascent and is rooted in social network analysis. My aim here is to predict (and establish) social relationships between members in social networks. Specifically, I will focus on “power relationships” in multi-party meetings/discourses, i.e. detecting who has more power, and thus, exerts a higher degree of influence in multi-party discourses. Potential applications include detecting ring-leaders in terror groups/gangs and determining if the outcomes of negotiations were reached under coercion/influence. I focus on Twitter data, in the domain of fashion (where power/influence is of utmost importance). I will present several features, derived from discourse (structure and content) and from psycholinguistics, to detect these power relationships. In addition, I will discuss the challenges in the task of detecting power relationships, which partially explain our inconclusive results thus far. Furthermore, I will present centrality measures, which could supplement the discourse and psycholinguistic features in order to improve the accuracy in predicting power relationships.


Agent, Epistemology, and AI
(by Tojo)

Abstract: In this talk, we will present fundamentals of Dynamic Epistemic Logic (DEL) where we show how our knowledge and belief are changed by agent communication. Especially, we expound how its action model contributes to the belief change of each agent, being different from Public Announcement Logic (PAL). Then, we apply the notion to subtle differences of the result of agent communication, e.g., what is informed, what is known to each other, and what is aware of for each agent. En route, we discuss the reliability of information source, including the notion of communication channel. Thereafter, we apply the idea to analyze several legal cases, and try to explain the predictability of causality in them.


Efficient legged locomotion robots based on limit cycle walking
(by Chong/Asano)

Abstract: Limit cycle walking is a novel approach to natural and energy-efficient legged locomotion of robotic walkers. In this talk, we introduce several simple limit-cycle walkers that can walk on level ground with small power supply. Our latest research developments are also reported.


Mobile and Smart Cyber Physical systems platforms: a focus on UAVs at Loria.
(by Ciarletta)

Abstract: Smart systems are all around us, from Smart Homes to Smart Cities, Smart Grids to Smart Transportation Systems. More and more mobile autonomous systems (and robots) will be integrated in these environnement. We have looked at these complex "Cyber-Physical Systems" from different points of view, and for several years we have developed a UAV/drone research platform at Loria.This talk will present this platform, some results and the ongoing/future work and potential collaboration.

Our initial goals with the platform were to both:

- provide a real test bed, demonstration and teaching platform for several fields of computer science (and beyond)

- and work on formation flight and flocking of autonomous robots from both the embedded software and the inter-system communication.

We are using our drones as a catalyst and a point of integration. For example, we are using them collectively as mobile nodes of wireless sensors and actuators to conduct environmental survey, and also studying them individually as typical use case of embedded real-time network. During the course of our projects, we've also developed our own UAVs for such targets as the Outback Joe Search and Rescue Challenge or for difficult hybrid environment (aerial, surface) with the Hydradrone.In the end, a very large spectrum of research and engineering question is provided through this platform: from HCI, AI, to networking and real-time/safety issues that need collaborative efforts to be solved.


WearAmI - Wearable and Ambient Intelligence Make Assistive Robots Smarter
(by Sgorbissa)

Abstract: The presentation describes the initial outcomes of the ongoing EU project WearAmI. WearAmI aims at integrating, within an intelligent environment, advanced robotic systems as well as distributed and wearable sensors (e.g., sensors embedded in watches, belts, etc.), with the goal of assisting elderly people and - in general - persons with reduced mobility needing assistance in daily activities.

Assistive robotics and other technologies for ambient assisted living are expected to have a groundbreaking impact on the society, and have been the subject of dedicated calls for project proposals both in Japan and in the EU. Most state-of-the-art approaches rely on the information provided by devices distributed in the environment (e.g., cameras, presence sensors, RFID antennas and tags) in order to "understand" the current situation, and consequently provide information to robots or to a monitoring system (e.g., to detect emergencies and other events, and react accordingly).

Unfortunately, traditional approaches have limitations: in particular, distributed sensors can reliably detect "where" inhabitants are located within the house and try to infer their intentions, but do not usually provide reliable information about "what" inhabitants are exactly doing. Indeed, being capable of distinguishing between different motions (e.g., brushing teeth or drinking a glass of water; falling down or purposely kneeling down to search for something under the bed) is fundamental for the robot or for the monitoring system to take decisions, and therefore this issue must be carefully dealt with.

The presentation discusses novel approaches and technological solutions in order to successfully merge and interpret the information provided by distributed and wearable sensors, to the end of making assistive robots more aware about the current situation, and consequently improving their performance in delivering services.


Probabilistic Machine Learning in Robotics
(by Low)

Abstract: In this talk, I will describe a few recent efforts in our research group to exploit a rich class of probabilistic machine learning models called the Gaussian process predictive models for robotic problems/applications such as active learning/sensing (aka adaptive sampling or information/data gathering) and localization.


Reconstruction of proof scores with a CafeOBJ proof assistant
(by Ogata)

Abstract: TBD


Design of the TLA+ Proof System
(by Merz)

Abstract: TLA+ is a specification language based on Zermelo-Fraenkel set theory and linear time temporal logic.　System verification is supported by the TLC model checker and by TLAPS, the TLA+ Proof System.　TLAPS consists of an interpreter for a language for writing explicit, hierarchical proofs, and interfaces to several automatic proof backends, including first-order provers, SMT solvers, and a decision procedure for propositional temporal logic. I will explain some of the challenges in designing TLAPS, including a rewrite system for encoding formulas of untyped set theory into multi-sorted first-order logic. (joint work with Damien Doligez, Leslie Lamport, Tomer Libal, and Hern将｡n Vanzetto)


Automating the First-Order Theory of Rewriting
(by Middeldorp)

Abstract: The first-order theory of rewriting is decidable for finite left-linear right-ground rewrite systems. We present FORT, a new tool that implements the decision procedure, which is based on tree automata techniques, for this theory. The tool offers the possibility to synthesize rewrite systems that satisfy properties that are expressible in the first-order theory of rewriting. In the talk, which is based on joint work with Franziska Rapp, we explain the decision and synthesis algorithms and demonstrate the tool.


Confluence and Critical-Pair-Closing Systems
(by Hirokawa)

Abstract: In this talk we introduce critical-pair-closing systems which are aimed at analyzing confluence of term rewriting systems. Based on the notion two new confluence criteria are presented. One is a generalization of weak orthogonality based on relative termination, and another is a partial solution to the RTA Open Problem #13. This presentation is based on joint work with Michio Oyamaguchi.