Construction of Computational Logics

CCL - 6028

Work Area: Logics and Logic Programming

Keywords logic programming, constraint solving, theorem proving

Start Date: 24 July 1992 / Duration: 36 months / Status: running

[ participants / contact ]

Abstract The aim of CCL is to study the construction of computational logics from components. Emphasis is put on the combination of logics and constraints systems. CCL will cover the study of combinations of particular logics and constraints of particular interest, the investigation of new symbolic constraints and their combination, and the design of new theorem proving techniques, taking advantage of constraints.


CCL aims to:


All participants intend to cooperate in the above five areas. There will be short visits from one site to another, seminars, and meetings. Members will attend conferences whose themes are relevant to those of CCL. A workshop of all participants will be organised each year. These meetings may be open to other participants working in the area of constraint theorem proving and constraint logic programming.

Progress and Results

Barcelona: Definition of a precedence-based AC simplification ordering total on ground terms for theorem proving with ordering constraints. The analysis of modular correctness in the software development process independently of the specific logics underlying specification and programming.

CIS, Munich: Solvability of systems of equations and disequations over nested lists is decidable for a solution domain of finite trees containing nested lists.

COSYTEC: Combination of constraints over finite domains with linear constraints over rational numbers, in particular by using cutting plane methods. Combination of diophantine equations solving algorithms with finite domains constraint solving techniques based on consistency checking.

DFKI: Implementation of Oz, a higher-order concurrent constraint programming language. Complete satisfiability and entailment tests for the combination of rational tree constraints with membership constraints, and for the feature constraint system CFT.

Madrid: Extension of the CLP scheme to accommodate lazy functional programming. Semantics and implementation techniques for programming languages based on lazy narrowing combined with various higher-order features.

MPI: Investigation of the relationship between set constraints and the monadic class of first-order formulas. Combination of linear and non-linear constraint solvers over real numbers based on abstract interpretation methods.

Nancy: Design and implementation of logical framework providing a unified view of logic programming, theorem proving and constraint solving. Combination of unification procedures for theories that share constants. Solving equations in various AC-theories, Automated deduction in AC theories.

Orsay: A general framework for equational completion, and its implementation. Algorithms for solving symbolic constraints: theory of embedding, distributive unification, negation elimination. Combinations of rewrite rules, lambda-caculus, and type inference mechanisms.

TUM, Munich: Design and implementation in the generic theorem prover Isabelle of a fast unification algorithm for a subclass of lambda-terms.


The past two decades have seen a proliferation of different programming styles, including functional, logical, constraints-based and object-oriented. More recently, it has been recognised that these styles complement rather than exclude each other: each is suitable for particular problem domains. As a consequence, combining programming paradigms has emerged as a significant line of research in its own right, and has many potential applications in both industry and universities. CCL will work towards this "combination" goal, and hence has great potential. However, the group does not expect to achieve a general solution to the combination problems within the next three years.

Latest Publications

Information Dissemination Activies

The Proceedings of the 1st CCL workshop are available as report CRIN-93-R-023 from INRIA Lorraine and CRIN.

Papers from CCL partners have been accepted in several journals, among them Information and Computation (1), Journal of Symbolic Computation (1), Journal of Mathematical and Computer Modelling (1), Journal on Applicable Algebra in Engineering, Communication and Computing (1), Journal of Automated Reasoning (1).Members of CCL were invited to give presentations on topics investigated in CCL in various conferences, eg AMAST (H. Comon), Portugese logic programming conference (G. Smolka).

CCL will organise an international conference open to submissions which will take place in Munich in the Fall of 94. Constraints will be the major topic of this conference. The proceedings will be published by Springer Verlag. We have not decided yet whether the conference will be organised on a regular basis.

Further information about CCL is available from the CCL home page <URL:>.


Cosytec - F
Rue Jean Rostand 4
F - 91893 ORSAY Cedex


Technische Universität München - D
Max-Planck Institüt für Informatik - D
Ludwig Maximilians Universität - D
Universidad Politecnica de Catalunya - E
Universidad Complutense - E
INRIA - Lorraine - F
Université de Paris-Sud - F


Mr. M. Dincbas
tel +33/1-60 19 37 38
fax +33/1-60 19 36 20

LTR synopses home page LTR work area index LTR acronym index LTR number index LTR Working Groups index
All synopses home page all acronyms index all numbers index

CCL - 6028, August 1994

please address enquiries to the ESPRIT Information Desk

html version of synopsis by Nick Cook