Topic for a 6 months Internship stage at INRIA (2009)

CHRREF: Towards a Generic Framework to Generate and Visualize Explanatory Traces of Constraint Solving and Rule-Based Reasoning

Constraint solving and rule-based reasoning are among the most versatile and historically successful paradigms to allow both declarative programming and knowledge representation. Their main strength is to combine the agility of fast prototyping with the robustness of formal verification through logically founded execution models. Their main weakness and key barrier to wider adoption by the software industry lies in the fact that most efforts to incorporate user-friendly reasoning explanation facilities in constraint solvers and rule engines have failed to tackled the key issues of engineering methodology and architecture, genericity and formal foundations.

Tackling these issues has been the focus of successive cooperative projects involving the group CONTRAINTES at INRIA-Rocquencourt, the last one being the ongoing C4RBCP (Components for Rule-Based Constraint Programming). The goal of the internship is to carry out the first steps towards component-based engineering a generic framework to generate and visualize explanatory traces for constraint solving and rule-based reasoning.

The very first step of this research will consist in specifying a refined operational semantics of the language CHR^Ú (Constraint Handling Rule with Disjunctions) in the fluent calculus. This semantics will then be abstracted into a base observational semantics (also in the fluent calculus), which could serve as a formally founded, generic middleware to connect reusable, explanatory trace generation and visualization components for a variety of constraint solvers and rule engines. The last step of the internship will consist in proposing architectural design patterns that leverage in synergy the concepts of observational semantics, tracer drivers and platform-independent component assemblies to engineer efficient and easy to extend constraint and rule based reasoning explanation generation and visualization facilities.

In this research, the choice of CHR^Ú and the fluent calculus is motivated by their following distinctive characteristics:

- CHR^Ú supports solving constraint systems over arbitrary domains;

- CHR^Ú elegantly integrates and/or subsumes the main rule paradigms: term rewriting rules, production rules, event-condition-action rules and constraint logic programming rules;

- The fluent calculus is a versatile yet easy to learn axiomization in classical first-order logic of computational processes based on action-triggered state changes;

- The fluent calculus natively incorporates the concept of process trace (called a situation);

- The FLUX (FLUent eXecutor) engine efficiently and provably correctly both reason about and execute processes specified in the fluent calculus;

- The FLUX engine can be ported to pure CHR^Ú, opening the door for the pair CHR^Ú/Fluent Calculus to constitute a self-contained generic basis for constraint solving, rule-based reasoning and the generation of explanatory traces for both.