Workshop Program

CHR 2012

10h55: Workshop opening
11h00: Ester Martínez, M. Teresa Escrig and Angel P. Del Pobil. Qualitative Velocity Model: Representation, Reasoning and Application
Abstract: On the way to autonomous systems, one of the key issues concerns spatial reasoning for solving problems dealing with uncertainty. From the starting point of human nature, information must be represented in a way that any system can reason with imprecise knowledge about different physical aspects and make correct decisions from them. Keeping this idea in mind, this paper presents the qualitative model of velocity including representation, reasoning process and a real robotic application.
11h30: János Csorba, Zsolt Zombori and Péter Szeredi. Pros and Cons of Using CHR for Type Inference
Abstract: We report on using logic programming and in particular the Constraint Handling Rules extension of Prolog to provide static type analysis for the Q functional language. We discuss some of the merits and difficulties of CHR that we came across during implementation of a type inference tool.
12h00: Henning Christiansen. An adaptation of Constraint Handling Rules for Interactive and Intelligent Installations
Abstract: Constraint Handling Rules, CHR, have proved to be effective for a large range of reasoning task, which is also interesting in different sorts of interactive installations. Typically, such an installation involves a large number of cooperating software components that need to refer to a common knowledge. Using CHR's constraint stores for knowledge representation may be appealing from a theoretical point of view, but suffers from the inherent limitation of CHR, that a constraint store disappears immediately after a query has been evaluated.

An extension to CHR is proposed, which allows different processes to reason over and maintain a common knowledge base represented as text files containing constraints. Constraints are automatically read from and written to the files before and after a query has been executed, which means that the intended style of programming deviates only very little from traditional CHR programming.
12h30: Alia El Bolock, Amira Zaki and Thom Frühwirth. Substitution-based CHR Solver for Bivariate Binomial Equation Sets
Abstract: Various methods for solving non-linear algebraic systems exist, as this question is amongst the most popular in both the realm of mathematics and computation. As most of these methods use approximations, this work focuses on finding and directly solving a tractable subset. Bivariate binomial systems of non-linear polynomial equations were chosen and solved through simulating the by hand method, using the declarative logic programming language Constraint Handling Rules. Substitution methods and different equation notations are used to extend the solvability of the subset.
13h00 - 14h00: Lunch Break
14h00: Amira Zaki, Thom Fruehwirth and Ilvar Geller. Parallel Execution of Constraint Handling Rules on a Graphical Processing Unit
Abstract: Graphical Processing Units (GPUs) consist of hundreds of small cores, collectively operating to provide massive computation capabilities. The aim of this work is to utilize this technology to execute Constraint Handling Rules (CHR) which are inherently parallel. A translation scheme is defined to transform a subset of CHR to C++, then to use a GPU to fire the rules on all combinations of constraints. As proof of concept, the scheme was performed on several CHR examples.
14h30: Rémy Haemmerlé. Coinductive Proof over Streams as CHR Confluence Proofs
Abstract: Coinduction is an important theoretical tool for defining and reasoning about unbound data structures (such as streams, graphs, infinite trees, rational numbers ...), and infinite-behavior systems. Confluence is a fundamental property of {C}onstraint {H}andling {R}ules ({CHR}) since, as in other rewriting formalisms, it guarantees that the computations are not dependent on rule application order, and also because it implies the logical consistency of the program declarative view. In this paper, we illustrate how the confluence of CHR can be used to prove universal coinductive properties. In particular, we give several examples of bisimulation proofs over streams.
15h00: Veronica Dahl and Juan Emilio Miralles. Womb Grammars: Constraint Solving for Grammar Induction
Abstract: We present Womb Grammars, a novel constraint-based framework implemented in CHRG and particularly useful for inducing, from known linguistic constraints that describe phrases in a language called the source, the linguistic constraints that describe phrases in another language, called the target. We present as well an application that uses as source an existing language fairly related to the target. Next we propose and motivate an intriguing research thread that uses as source language a (non-natural but coupled with our framework, generatively very powerful) universal language of our own device. Finally, we discuss further ramifications of our work.