CHR 2012

Ninth International Workshop on Constraint Handling Rules
Budapest, Hungary — September 4th, 2012

Introduction

The CHR 2012 Workshop will be held on September 4th, 2012 in Budapest (Hungary) at the occasion of ICLP 2012, the premier international venue for presenting research in logic programming.

The Constraint Handling Rules (CHR) language has become a major declarative specification formalism and implementation language for constraint reasoning algorithms and applications. Algorithms are often specified using inference rules, rewrite rules, sequents, proof rules, or logical axioms that can be directly written in CHR. Its clean semantics facilitates program design, analysis, and transformation. See the CHR website for more information.

The aim of the CHR workshop series is to stimulate and promote international research and collaboration on topics related to the Constraint Handling Rules language. The workshop is a lively, friendly forum for presenting and discussing new results, interesting applications, and work in progress. Previous Workshops on Constraint Handling Rules were organized in 2004 in Ulm (Germany), in 2005 in Sitges (Spain) at ICLP, in 2006 in Venice (Italy) at ICALP, in 2007 in Porto (Portugal) at ICLP, in 2008 in Hagenberg (Austria) at RTA, in 2009 in Pasadena (California, US) at ICLP, in 2010 in Edinburgh (Scotland, UK) at ICLP, and in 2011 in Cairo (Egypt), at the 2nd CHR summer school.

Topics of Interest

The workshop calls for full papers and short papers describing ongoing work on any aspect of CHR and related approaches. The following topics are relevant (this list is non-exhaustive):

Important dates

Submission Information

The four broad categories for submissions are:

All papers must describe original, previously unpublished research, and must not simultaneously be submitted for publication elsewhere. They must be written in English. Technical papers must not exceed 15 pages. The limit for short papers is 8 pages, as is the standard page limit for application papers, and system and tool papers. However, particularly strong contributions in the latter two areas may be submitted as technical paper as well.

All papers must be in the Springer LNCS format. General information about the Springer LNCS series and the LNCS authors' instructions are available at the Springer LNCS home page.

Submissions must be made via the EasyChair submission system.

Program

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.

The full workshop's program is available here.

Proceedings

The workshop proceedings will be made available as a technical report. Individual PDF versions of all accepted papers will be available on the program page or from the CHR bibliography.

Programme Committee

Workshop Coordinators

Contact: chr2012@easychair.org

Jon Sneyers
Department of Computer Science, K.U.Leuven
Leuven, Belgium
http://people.cs.kuleuven.be/~jon.sneyers/
Thom Frühwirth
Programmiermethodik und Compilerbau, Ulm University
Ulm, Germany
www.informatik.uni-ulm.de/pm/mitarbeiter/fruehwirth/