navigation

 


Résumés des communications acceptées à JFPLC'2001

Il y a 18 papiers acceptés (17 résumés disponibles)

 

 


   Refining the Basic Constraint Propagation Algorithm
Auteur(s) :   Christian Bessière ( COCONUT group LIRMM CNRS (UMR 5506))   Jean-Charles Régin ( ILOG)

Résumé : La propagation de contraintes est au coeur de tous les solveur avec contraintes. Il est donc important d effectuer cette propagation de la façon la plus efficace possible, ce qui justifie l'utilisation des meilleurs algorithmes. Mais la simplicité d intégration est aussi une des préoc-cupations quand on implémente un algorithme dans un solveur. Cet article s intéresse à AC-3, qui est l'algorithme de cohérence d arc le plus simple. Nous proposons deux améliorations de AC-3 qui préservent autant que possible sa facilité d intégration (pas de structures de données complexes à maintenir pendant la recherche), tout en apportant un gain sensible en temps. Une des améliorations proposées dispose en plus de bonnes propriétés théoriques.

Abstract: Constraint propagation is the main feature of any constraint solver. This is thus of prime importance to manage constraint propagation as efficiently as possible, justifying the use of the best algorithms. But the ease of integration is also one of the concerns when implementing an algorithm in a constraint solver. This paper focuses on AC-3, which is the simplest arc con-sistency algorithm known so far. We propose two refinements that preserve as much as possible the ease of integration into a solver (no heavy data structure to be maintained during search), while giving some noticeable improvements in efficiency. One of the proposed refinements is analytically compared to AC-6, showing interesting properties.

Mots clés : programmation par contraintes, propagation de contraintes, cohérence d'arc

Keywords: constraint satisfaction problems, constraint propagation, arc consistency


   A Theoretical Analysis of the Average Time-Complexity of Domain-Heuristics for Arc-Consistency Algorithms
Auteur(s) :   M.R.C. van Dongen ( Department of Computer Science, University College Cork)

Résumé : Les algorithmes de cohérence d'arc sont largement utilisés pour réduire l'espace de recherche des CSPs (Constraint Satisfaction Problems). Ils utilisent des tests de supports pour connaître les propriétés des CSPs. Ils utilisent des heuristiques d'arc pour sélectionner la contrainte à utiliser et des heuristiques de domaines pour le test support suivant. Nous allons étudier la complexité temporaire moyenne de deux algorithmes de cohérence d'arc L et D qui ne diffèrent que par leur domaine heuristique. L utilise une heuristique lexicographique et D une heuristique qui préfère un test de support double. Pour des domaines a et b de dimensions suffisantes, nous utiliserons une limite inférieure de 2a + 2b + O(1) pour L et une limite supérieure de 2 max(a,b) + 2 pour D. Nous prouverons qu'il n'y a pas d'algorithme qui puisse sauver plus de deux tests en moyenne que D.

Abstract: Arc-consistency algorithms are widely used to prune the search-space of constraint satisfaction problems (CSPs). They use support-checks to find out about the properties of CSPs. They use arc-heuristics to select the constraint to be used and domain-heuristics to select the values to be used for the next support-check. We will investigate the average time-complexity of two arc-consistency algorithms L and D which only differ in their domain-heuristic. L uses a lexicographical heuristic and D a heuristic which prefers double-support check. For sufficiently large domain-sizes a and b we will provide a lower bound of approximately 2a + 2b + O(1) for L and upper bound of 2 max(a,b) + 2 for D . We will prove that no algorithm can save more than two checks more on average than D.

Mots clés : Satisfaction de Contraintes, Cohérance d'Arc, Complexité Temporaire Moyenne

Keywords: Constraint Satisfaction, Arc-Consistency, Average Time-Complexity


   An Algorithm for Fast Recognition of Connected Row-Convex Constraint Networks
Auteur(s) :   Enhong CHEN   Zhenya ZHANG   Xufa WANG ( Department of Computer Science and Technology University of Science and Technology of China)   Kazuyuki AIHARA ( Department of Mathematical Engineering and Information Physics Faculty of Engineering, University of Tokyo)

Abstract: Many constraint satisfaction problems that arise in practice place special restrictions on the structure of constraints or the form of the constraints, allowing them to be solved efficiently. For identification of such tractable constraints, much work has been devoted to the study of special classes of constraints or constraint networks. This paper provides a standardized form for Connected Row-Convex (CRC) constraint based on related work on CRC constraint networks. In addition to an analysis of the basic characteristics of the standardized form, a fast algorithm for the recognition of CRC constraint networks based on a recognition algorithm of the Row-Convex (RC) constraint networks and an indexed matrix representation of constraints is presented. If we denote n as the number of variables in a constraint network and d as the maximum size of the domain of all variables, the time complexity of the algorithm is O(n 3 d 2 ) which is the optimum time complexity for the recognition of CRC constraint network.

Keywords: constraint network, row convexity, connected row convexity, standardized form, indexed matrix.


   High-Level Reformulation of Constraint Programs
Auteur(s) :   Brahim Hnich   Pierre Flener ( Computer Science Division Department of Information Science Uppsala University)

Résumé : Nous proposons un jeu de règles de reformulation pour modèles de problèmes de satis-faction de contraintes exprimés dans notre langage de haut niveau ESRA pour programmation par contraintes, qui est plus expressif que OPL et qui est compilé en OPL. Ces règles automatisables donnent des modèles souvent très similaires à ce qu un modélisateur humain aurait essayé, comme par exemple le passage d'un pur programme par contraintes à un programme linéaire entier. Comme, pour un solveur donné et une instance donnée d'un problème, il est très difficile de déterminer quel modèle est le meilleur, nous maintenons qu'un outil supportant nos règles de reformulation devrait utiliser un jeu d'instances d'entraînement. En effet, ceci est la seule voie pour garantir que la reformulation effectivement choisie soit rentable, du moins pour les instances dans la distribution sousjacente aux instances d'entraînement.

Abstract: We propose a set of reformulation rules for models of constraint satisfaction problems that are written in our high-level constraint programming language ESRA, which is more ex-pressive than OPL and is compiled into OPL. These automatable rules achieve models that are often very similar to what a human modeller would have tried, such as switching from a pure constraint program to an integer linear program. Since, for a given solver and a given instance of a problem, it is very hard to figure out which model is the best, we advocate that tool support of our reformulation rules should operate with a set of training instances. Indeed, this is the only way of guaranteeing that the actually chosen reformulation pays off, at least for instances within the distribution underlying the training instances.

Mots clés : Programmation par contraintes, modélisation de haut niveau, reformulation.

Keywords: Constraint programming, high-level modelling, reformulation.


   Recherche adaptative et contraintes musicales
Auteur(s) :   Charlotte Truchet   Carlos Agon   Gérard Assayag ( IRCAM)

Résumé : Cet article présente un environnement de résolution de contraintes (CSP) musicales, basé sur le langage visuel OpenMusic. Nous présentons notamment une implémentation d'un algorithme de recherche locale, appelé recherche adaptative, dans le domaine musical. La recherche adaptative reprend le principe de résolution par optimisation d'une fonction de coût, mais en affinant la notion de coût de manière à tenir compte du poids de chaque variable. Nous montrons qu un algorithme incomplet est particulièrement bien adapté dans le cas des CSP musicaux. Les premiers résultats expérimentaux sur des problèmes musicaux réels sont satisfaisants, notamment en temps de calcul.

Abstract: We propose an environment for musical constraint solving, in the visual programming language OpenMusic. We describe an implementation of a local search algorithm, called adap-tive search, in the musical field. Adaptive search refines the concept of cost function by taking into account the weight of each variable. We show that an incomplete algorithm is well adapted for musical problems. The first experimental results on real musical problems are satisfying, including in terms of computation time.

Mots clés : programmation par contraintes, CSP, recherche locale, recherche adaptative, con-traintes musicales, composition assistée par ordinateur, séries tous intervalles

Keywords: constraint programming, CSP, local search, adaptive search, musical constraints, computer assisted composition, all-interval series


   Symétries pour les modèles finis des théories de la logique du premier ordre
Auteur(s) :   Gilles Audemard   Belaid Benhamou ( Laboratoire d'Informatique de Marseille Centre de Mathématiques et d'Informatique 39, Rue Joliot Curie - 13453 Marseille cedex 13)

Résumé : La génération de modèles et de contre modèles finis pour des théories de la logique du premier ordre est une notion complémentaire à la démonstration automatique. Les méthodes de génération de modèles finis exploitent certaines symétries pour élaguer l'espace de recherche. Les systèmes FALCON, SEM et FMSET, utilisent l'heuristique LNH(Least Number Heuristic) de Jian ZHANG qui consiste a conserver les symétries existant entre les individus des domaines de la formule de départ. Bien qu'intéressantes, ces symétries triviales disparaissent sitôt qu'on avance dans la recherche de la solution. Les individus utilisés dans l'interprétation partielle deviennent non symétriques au sens LNH. Or, d'autres symétries existent abondamment sur ces éléments. Nous étudions, dans ce papier un cadre plus général de la symétrie pour les modèles finis, nous montrons que la symétrie LNH est un cas particulier de ce cadre. Nous Donnons quelques résultats sur les symétries et proposons une méthode de détection dynamique de ces dernières. Nous expliquons ensuite comment utiliser ces symétries en les combinant avec celle de LNH pour améliorer l'efficacité des générateurs de modèles finis. Enfin, Une étude expérimentale et comparative de la méthode SEM avec et sans l'apport des symétries est faite sur des problèmes intéressants en mathématiques.

Abstract: Finite modele search for first order logic theories is a complementary alternative to automated deduction. Systems like Falcon, SEM and FMSET use the LNH(Least Number Heuristic) heuristic to eliminate some trivial symmetries. Such symmetries are worthful, but their exploitation is limited to the first levels of the model search tree, since they desappear as soon as the first cells have been instanciated. We study in this paper a more general notion of symmetry than LNH and provide some exploitations which we combine with it to optimize the symmetry use and increase the model search efficiency. The method SEM with and without symmetry is experimented on several interesting mathematic problems to show the advantage of symmetry.

Mots clés : Modèles Finis, Symétries

Keywords: Finite models, Symmetries


   A Confluent Extension of Lafont's Interaction Nets
Auteur(s) :   Satoshi Matsuoka ( Department of Electrical and Computer Engineering, Faculty of Engineering, Nagoya Institute of Technology)

Résumé : Le système de réseaux d'interaction, qui a été présenté par Lafont, peut être considéré comme genre de langage de programmation en logique. Le système est localement confluent: les calculs sont déterministes et si un réseau d'interaction a la forme normale, alors toutes les réductions à la forme normale ont la même longueur. Dans cet article, nous présentons une extension du système de réseaux d'interaction, qui est toujours localement confluent. Nous montrons le codage des réseaux additifs de preuve de Girard dans le système étendu de réseaux d'interaction.

Abstract: The interaction nets system, which was introduced by Lafont, can be considered as a kind of logic programming language. The system is locally confluent: the computations are deterministic and if a interaction net has the normal form, then all the reductions to the normal form have the same length. In this paper, we present an extension of the interaction nets system, which is still locally confluent. We show the encoding of Girard's additive proof nets into the extended interaction nets system.

Mots clés : Réseaux d'interaction, Réseaux de preuve, Unification garde

Keywords: Interaction Nets, Proof Nets, Guarded Unification


   Optimal models and optimal trajectories in logical dynamics
Auteur(s) :   Areski Nait Abdallah ( Department of Computer Science University of Western Ontario )

Résumé : Il a été montré précédemment [NAI'95, NAI'00] que le raisonnement du sens commun peut être analysé comme un mouvement à travers un espace abstrait d'états d'information par-tielle. Ce mouvement est gouverné par des principes variationnels analogues à ceux utilisés en mécanique classique des systèmes physiques. Dans cet article nous montrons que ce lien entre le raisonnement sur information partielle et la mécanique classique semble tout à fait solide. Nous donnons des fonctions Lagrangiennes pour le raisonnement du sens commun sur des sytèmes statiques et des systèmes dynamiques, dont les problèmes de projection temporelle tels le Yale Shooting Problem. Nous montrons que la solution de ces problèmes de raisonnement du sens commun se réduit à la minimisation du Lagrangien associé sur l'espace des modèles partiels. Ces résultats suggèrent que le raisonnement du sens commun peut se réduire à un problème de programmation mathématique, consistant en la minimisation d'une fonction Lagrangienne sur un espaces abstraits d'états cognitifs.

Abstract: In earlier publications [NAI'95, NAI'00], it was shown that commonsense reasoning can be analyzed as motion through an abstract space of partial information states. Such a motion is governed by variational principles akin to those used in the classical mechanics of physical systems. How deep is this link between reasoning with partial information and classi-cal mechanics? In this paper we show that the link seems quite strong. We exhibit Lagrangian functions for com-monsense reasoning, akin to those used in physics. General Lagrangian functions for both static and dynamic systems are given, thus covering temporal projection problems such as the Yale Shooting Problem. Our results strongly suggests that commonsense reasoning may be reduced to a mathematical programming problem, consisting of minimizing a Lagrangian function on an abstract space of cognitive states.

Mots clés : Logique partielle, dynamique logique, résolution de contraintes, fonctions Lagrang-iennes, raisonnement du sens commun, programmation en logique.

Keywords: Partial logic, logical dynamics, constraint solving, Lagrangian functions, common-sense reasoning, logic programming.


   Programmation concurrente par contraintes explicitement répartie
Auteur(s) :   Nicolas Romero ( Laboratoire d'Informatique Fondamentale d'Orléans Université d'Orléans)

Résumé : Cet article présente un formalisme pour la programmation concurrente par contraintes explicitement répartie, basé sur le cadre de la programmation concurrente par contraintes de Saraswat (cc). Les calculs deviennent répartis : le store de contraintes unique est remplacé par des sites encapsulant un store local et des processus. Un site peut être créé dynamiquement et se déplacer pendant un calcul. Plusieurs sites coexistent en général durant un calcul, indépendants les uns des autres, sauf les sites interconnectés par l'intermédiaire d'interfaces. De plus, le formalisme présenté autorise le contrôle de l'exécution des processus dans les sites par suspension et activation. Ces extensions donnent naissance à un cadre de programmation puissant. La syntaxe et une sémantique opérationnelle sont définies, et des exemples d'utilisation sont donnés.

Abstract: This paper presents a formalism for explicit distributed concurrent constraint pro-gramming, based on Saraswat s concurrent constraint programming framework (cc ). Our cal-culus makes cc distribution- and time-aware: instead of dealing with an unique global con-straint store, it is based on the notion of location. Each location encapsulates a local store and some processes acting on it. It is dynamically created during a computation and can move as a whole on its own initiative to be interfaced with other locations. We also discuss the ability to detect local store modifications, and to start and suspend locations, to obtain multiform time awareness. We finally present several examples to show that these minimal changes lead to a powerful distributed concurrent constraint framework.

Mots clés : programmation concurrente par contraintes, répartition, agents mobiles

Keywords: concurrent constraint programming, distribution, mobile agents


   Recherche coopérative et Nogood Recording
Auteur(s) :   Cyril Terrioux ( LIM - Equipe INCA)

Résumé : Dans le cadre du problème de satisfaction de contraintes, nous proposons un nou-veau schéma de recherche parallèle coopérative. La coopération est réalisée en échangeant des nogoods (instanciations qui ne peuvent être étendues en une solution). Nous associons un processus à chaque solveur et nous introduisons un gestionnaire de nogoods, afin de réguler les échanges de nogoods. Chaque solveur emploie l'algorithme Forward-Checking avec No-good Recording. Nous ajoutons à l'algorithme une phase d'interprétation qui limite la taille de l'arbre de recherche suivant les nogoods reçus. Les solveurs diffèrent par l'emploi d'heuris-tiques distinctes pour le choix des variables et/ou des valeurs. l'intérêt de cette approche est démontré expérimentalement. En particulier, nous obtenons des accélérations linéaires ou su-perlinéaires pour des problèmes consistants comme pour des problèmes inconsistants, jusqu à une dizaine de solveurs.

Abstract: Within the framework of constraint satisfaction problem, we propose a new scheme of cooperative parallel search. The cooperation is realized by exchanging nogoods (instantiations which can t be extended to a solution). We associate a process with each solver and we intro-duce a manager of nogoods, in order to regulate exchanges of nogoods. Each solver runs the algorithm Forward-Checking with Nogood Recording. We add to algorithm an interpretation s phase, which limits the size of search tree according to received nogoods. Solvers differ from each other in ordering variables and/or values by using different heuristics. The interest of our approach is shown experimentally. In particular, we obtain linear or superlinear speed-up for consistent problems, like for inconsistent ones, up to about ten solvers.

Mots clés : problème de satisfaction de contraintes, recherche parallèle, coopération, nogood.

Keywords: constraint satisfaction problem, parallel search, cooperation, nogood.


   Impact de la Programmation Logique Parallèle et par Contraintes sur l'Ingénierie des Systèmes Multi-Agents
Auteur(s) :   Abdelfettah Hasbani   Olivier Guinaldo ( IUT Clermont-Ferrand - LIMOS)

Résumé : Dans cet article, après une brève présentation de l'environnement « VALID », un environnement pour la spécification et la validation des systèmes réactifs, nous nous intéressons à la génération de programmes d'applications BeBOP (Parallel-NU-Prolog) à partir des spécifications formelles issues de VALID. La validité de ces programmes est fondée sur le principe de développement par raffinement successif et preuve associée. Si le langage BeBOP est le langage cible idéal pour VALID, il n'est pas aussi connu que ses cousins Prolog norme iso. Nous donnons par conséquent comme perspectives quelques éléments de réflexions sur la modélisation d'agents dans un langage de type Prolog iso muni d'un prédicat de retardement de but (freeze par exemple en Prolog IV).

Abstract: In this paper, after a concise presentation of the environment for reactive systems engineering « VALID », we are interesting to the prototype of Parallel-Nu-Prolog program generation from the formal specification outcome of VALID. The target code validation is based on vertical refinments from semi-graphical description (high level specification). If the BeBOP language is ideal for VALID, its not too be acquainted with other Prolog iso norm. We then gives like a perspectives some areas for agents modelisation in a language as Prolog iso equiped with freeze predicat such in Prolog VI.

Mots clés : spécification formelle, systèmes réactifs, systèmes multi-agents, validation, programmation logique parallèle et par contraintes.

Keywords: formal specification, reactive systems, multi-agent systems, validation, parallel and constraint logic programming.


   Amélioration de la complexité des kB-consistances
Auteur(s) :   Lucas BORDEAUX   Eric MONFROY   Frédéric BENHAMOU ( Institut de Recherche en Informatique de Nantes)

Résumé : Les kB-consistances forment la classe de consistances fortes utilisées en programmation par contraintes d'intervalles. Nous décrivons et justifions formellement diverses améliorations techniques de l'algorithme naïf de kB-consistance. Notre contribution est double : d'une part nous présentons un algorithme de 3B-consistance de complexité en temps optimale O(md2n), ce qui améliore la complexité théorique connue d'un facteur n (m est le nombre de contraintes, n le nombre de variables et d'est le nombre d'éléments du plus grand intervalle de la boîte considérée). D'autre part, nous montrons qu'il est possible d'améliorer la borne supérieure de temps dans le cas général. Ces résultats sont obtenus sans augmentation excessive de la complexité en espace.

Abstract: kB-consistencies form the class of strong consistencies used in interval constraint programming. We survey, prove, and give theoretic motivations to some technical improve-ments to a naive kB-consistency algorithm. Our contribution is twofold: on the one hand, we introduce an optimal 3B-consistency algorithm whose time-complexity of O(md2n) improves the known bound by a factor n (m is the number of constraints, n is the number of variables, and d is the maximal size of intervals of the box). On the other hand, we prove that improved bounds on time complexity can effectively be reached for stronger values of k. These results are obtained with very affordable overheads in terms of space.

Mots clés : Contraintes d'intervalles, consistances fortes

Keywords: Interval constraints, strong consistency techniques


   Programmes Logiques avec Contraintes Typés Vérifier les coercions de domaines et la méta-programmation à travers le sous-typage
Auteur(s) :   Emmanuel Coquery   François Fages ( INRIA Rocquencourt)

Résumé : Nous proposons un système de types prescriptif général avec polymorphisme paramé-trique et sous-typage pour la programmation logique avec contraintes. l'objectif de ce système de types est la détection statique d'erreurs de programmation. Il introduit une discipline de ty-page simple pour les programmes logiques avec contraintes et les modules, tout en autorisant d'une part les coercions usuelles entre les domaines de contraintes et, d'autre part, le typage de la méta-programmation, grâce à la flexibilité du sous-typage. La propriété de subject re-duction représente la cohérence du système de types vis-à-vis du modèle d'exécution : si un programme est bien typé , alors toutes les dérivation commençant par un but bien typé sont bien typées . Cette propriété est prouvée vis-à-vis du modèle d'exécution abstrait de programmation par contraintes procédant par accumulation de contraintes, les opérations de substitutions nécessitant quant à elles de conserver les contraintes de types sur les variables à l'exécution. Nous décrivons notre implantation du système pour la vérification de types et l'inférence de types. Nous exposons nos résultats expérimentaux sur la vérification de type des bibliothèques de Sicstus Prolog et de quelques autres programmes Prolog.

Abstract: We propose a general prescriptive type system with parametric polymorphism and subtyping for constraint logic programs. The aim of this type system is to detect programming errors statically. It introduces a type discipline for constraint logic programs and modules, while maintaining the capabilities of performing the usual coercions between constraint do-mains and of typing meta-programming predicates, thanks to the flexibility of subtyping. The property of subject reduction expresses the consistency of the type system w.r.t. the execution model: if a program is well-typed , then all derivations starting in a well-typed goal are again well-typed . That property is proved w.r.t. the abstract execution model of constraint programming which proceeds by accumulation of constraints, whereas the operations of substi-tution need to keep type constraints on variables at run-time. We describe our implementation of the system for type checking and type inference. We report our experimental results on type checking the libraries of Sicstus Prolog and other Prolog programs.

Mots clés : programmation, logique, contraintes, prescriptif, type, sous-typage, paramétrique

Keywords: programing, logic, constraints, precriptive type, subtyping, parmetric


   Parametric Descriptive Types for (C)LP
Auteur(s) :   Wlodzimierz Drabent *,**   Jan Maluszynski *   Pawel Pietrzak *,*** ( * Linköping University, Dept. of Computer and Information Science
** Institute of Computer Science, Polish Academy of Sciences
*** Institute of Computing Science, Poznan University of Technology
)

Résumé : Cet article introduit un concept de correction partielle d'un programme logique avec contraintes, relativement à une spécification parametrique. Selon la tradition de typage descriptif, nous utilisons un langage de specification qui étend le formalisme bien connu des "discriminative term grammars". L'extension introduit des paramètres qui décrivent la nature polymorphique des programmes. Nos spécifications font référence à la sémantique "call-success" des programmes, avec l'intention d'approximer les sémantiques dans un sens bien défini. Ces spécifications peuvent etre considérées comme des types directionnels, polymorphes et descriptifs. Nous présentons une technique pour vérifier la correction des programmes relativement à ces specifications. Un protoype implémentant cette technique pour un sous ensemble de CHIP, le langage de progammation par contraintes, est brièvement décrit. l'incorrection d'un programme résultera toujours d'un échec de vérification de type qui localisera le fragment du code responsable de cet échec.

Abstract: The paper introduces a concept of (partial) correctness of a constraint logic program with respect to a parametric specification. Following the tradition of descriptive typing we use a specification language which extends the well-known formalism of discriminative term gram-mars. The extension introduces parameters to describe polymorphic nature of programs and base symbols to deal with constraint domains. Our specifications refer to the call-success se-mantics of programs, with the intention to approximate the semantics in some precisely defined sense. They can be seen as descriptive polymorphic directional types. We present a technique for checking correctness of programs with respect to such specifications. A prototype tool im-plementing this technique for a subset of CHIP constraint programming language is briefly described. Incorrectness of a program will always result in a type checking failure, locating the responsible fragment(s) of the program.

Mots clés : Programmation en logique et par contraintes, Typage descriptif, Typage paramétrique, Correction de programme

Keywords: Constraint logic programming, Descriptive types, Parametric types, Program correctness


   HyperPro Un environnement intégré de documentation pour la PLC
Auteur(s) :   AbdelAli Ed-Dbali ( LIFO - Université d'Orléans)   Pierre Deransart ( INRIA-Rocquencourt)   Mariza A. S. Bigonha   José de Siqueira   Roberto da S. Bigonha ( DCC-UFMG)

Résumé : Le but de cet article est de présenter certaines fonctionnalités du système HYPERPRO. HYPERPRO est un environnement de développement integré pour la PLC (programmation en logique et par contraintes) qui offre deux aspects du développement d'un programme : le codage en PLC et la documentation. Un document HYPERPRO est donc une combinaison de code et de sa documentation. La partie édition d'HYPERPRO est basé sur le système Thot. HYPERPRO est un éditeur WYSIWYG qui offre des facilités de navigation hypertexte, de manipulation de versions d'un même programme, d'extraction de vues projections selon des critères spécifiques. Il offre également l'exportation de document vers plusieurs formats courants (ps, html, latex, ...) ainsi que la gestion des indexes. HYPERPRO a été conçu pour la PLC mais il peut aussi bien être adapté à d'autres paradigmes de programmation.

Abstract: The purpose of this paper is to present some functionalities of the HYPERPRO System. HYPERPRO is a hypertext tool that offers a way to handle two basic aspects: Constraint Logic Programming (CLP) documentation and development and text editing. For text editing it is based on the Thot system. A HYPERPRO program is a Thot document written in a report style. HYPERPRO offers navigation and editing facilities, such indexes, document views and projections. It also offers document exportation. Projection is a mechanism for extracting and exporting relevant pieces of code according to specific criteria. Indexes are necessary to find the references and occurences of a relation in a document, i.e., where its predicate definition is found and where a relation is used in other programs or document versions and to translate hypertexts links into paper references. HYPERPRO has been designed for logic programming but it can be adapted to other programming paradigms as well.

Mots clés : PLC, programmation littéraire, gestion de versions, édition structurée, hypertexte, documentation, spécification

Keywords: CLP, literate programming, version managment, structured editor, hypertext, docu-mentation, specification


   cTI : un outil pour l'inférence de conditions optimales de terminaison pour Prolog
Auteur(s) :   Fred Mesnard ( Iremia, Université de La Réunion, France )   Ulrich Neumerkel ( Université Technique de Vienne, Autriche )   Etienne Payet ( Iremia, Université de La Réunion, France )

Résumé : La terminaison est un aspect crucial de la vérification de programmes. Cet article pro-pose un outil pour inférer des conditions suffisantes de terminaison à partir du texte de tout programme Prolog. Nous adoptons pour cela une approche ascendante du problème pour es-sayer de caractériser, pour chaque relation définie dans le programme, l'ensemble des classes de requêtes qui terminent universellement pour la règle de sélection Prolog. Nous décrivons l'architecture de notre implantation nommée cTI. Nous évaluons notre système sur une soixan-taine de programmes dont les tailles varient de quelques à plusieurs centaines de clauses. Enfin, nous présentons nos travaux en cours concernant la détection de l'optimalité des conditions de terminaison.

Abstract: Termination is a crucial aspect of program termination. This paper describes our tool named cTI for inferring sufficient termination conditions from any Prolog program text. We adopt a bottom-up approach where we try to characterize, for each relation defined in a program, the set of universally left-terminating queries. We present the architecture of our implementation. We benchmark cTI against sixty programs which sizes range from a few to several hundred clauses. At last, we discuss our current work on checking the optimality of terminating conditions.

Mots clés : programmation logique, terminaison, analyse statique.

Keywords: logic programming, termination, static analysis.


   Preuves de programmes logiques par induction et coinduction
Auteur(s) :   Sorin Craciunescu ( INRIA Rocquencourt)

Résumé : Dans cet article nous nous intéressons aux preuves d' équivalence de programmes logiques par rapport à l'ensemble des succès et des échecs finis. Les programmes sont écrits dans le langage CLP auquel on a ajouté la quantification universelle (CLP forall). Après avoir présenté sa syntaxe et sémantique on introduit un système de preuve basé sur l'induction et la logique classique du premier ordre qui permet de démontrer que les succès d'un programme sont inclus dans ceux d'un autre et on démontre sa correction. On présente son système dual basé sur la coinduction pour les échecs finis et on montre que les deux systèmes sont équivalents en utilisant une transformation de programmes basée sur la négation.

Abstract: In this paper we focus on proofs for logic programs, specifically equivalence with respect to the set of successes and finite failures. The programs are writen in CLP to which we add the universal quantifier (CLP forall). We first introduce its syntax and semantics then we present a proof system based on induction and the first order classical logic in which one can prove that some program s successes are included in an other s and we prove its soundness. We introduce its dual system based on coinduction for the finite failues and we prove that the two systems are equivalent by using a negation-based program transformation.

Mots clés : équivalence de programmes, système de preuve, induction, coinduction, program-mation logique, contrainte, CLP, quantification universelle

Keywords: program equivalence, proof system, induction, coinduction, logic programming, constraint, CLP, universal quantifier

 

line
© INRIA (pour toute question ou suggestion sur le site écrire à A. ED-DBALI)

Informations pratiques (Hôtels, Restos, Transports, ...)Appel à démos et postersBulletin d'inscriptionNouveautés sur le siteAccueilWelcomeRésumés des communicationsConférenciers invitésInstructions aux auteursComité de programme et d'organisationProgramme scientifiqueAppel à communications Lieu de la conférence coordonnées