To see the other types of publications on this topic, follow the link: Langages de programmation logique.
Dissertations / Theses on the topic 'Langages de programmation logique'
Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles
Consult the top 50 dissertations / theses for your research on the topic 'Langages de programmation logique.'
Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.
You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.
Browse dissertations / theses on a wide variety of disciplines and organise your bibliography correctly.
1
Fronhöfer, Franz Bertram. "La logique dans la programmation : synthèse logique de programmes et langages de programmation logique." Grenoble INPG, 1989. http://www.theses.fr/1989INPG0047.
Full textAbstract:
Comparaison de plusieurs approches de la synthese de programmes. Presentation de deux etudes visant d'une part a l'affinement du raisonnement logique en forme non normale et d'autre part a la transformation de la logique de premier ordre en clauses de horn. Un langage logique qui unifie le raisonnement deductif et la programmation procedurale est propose
2
Ezequel, Philippe. "Décomposition en programmation logique." Montpellier 2, 1990. http://www.theses.fr/1990MON20100.
Full textAbstract:
On étudie dans cette thèse la décomposition de programmes logiques, c'est-à-dire le fait qu'un programme puisse être découpé en sous-programmes de telle sorte que le résultat de l'exécution indépendante de chacun des sous-programmes soit équivalent à l'exécution du programme entier. A cet effet, une nouvelle description des programmes logiques (en termes d'ensembles de buts, les comportements) est donnée. On prouve qu'elle est équivalente aux sémantiques classiques. On en déduit de nouvelles conditions nécessaires et suffisantes d'équivalence et de décomposabilité des programmes logiques. Une étude plus approfondie des comportements montre que certains de leurs buts, appelés donc générateurs, engendrent les autres, et qu'ils suffisent pour décrire opérationnellement le programme. L'existence d'une relation entre décomposabilité et buts générateurs est enfin examinée
3
Lafont, Yves. "Logiques, catégories et machines : implantation de langages de programmation guidée par la logique catégorique /." [Le Chesnay] : [Institut national de recherche en informatique et en automatique], 1988. http://catalogue.bnf.fr/ark:/12148/cb34935229k.
Full text
4
Denis, François. "Contribution à l'étude des sémantiques axiomatiques de Prolog." Lille 1, 1990. http://www.theses.fr/1990LIL10170.
Full textAbstract:
La sémantique opérationnelle des programmes Prolog(définis) la plus fréquemment étudiée fait implicitement l'hypothèse que ces programmes sont évalués par des interpréteurs idéaux (en largeur d'abord et équitables). En conséquence, les résultats théoriques très complets qui ont été obtenus jusqu'à présent ne s'appliquent pas aux interpréteurs standard usuels. Nous définissons de nouvelles sémantiques opérationnelles, adaptées aux interpréteurs standards ou plus généralement, décrivant un noyau calculable quel que soit l'interpréteur envisagé. Nous montrons ensuite que ces sémantiques peuvent être caractérisées axiomatiquement ; ces résultats constituent donc une version plus réaliste et plus générale des résultats classiques. Nous avons utilisé, au cours de cette étude, une technique de dédoublement des symboles de prédicats dont nous avons étudié systématiquement les rapports avec la logique trivaluée. Nous avons également démontré des théorèmes de complétude en logiques bivaluée et trivaluée s'appliquant à des classes générales de programmes logiques (comprenant bon nombre des traductions axiomatiques rencontrées en programmation logique) dans le cadre de la Théorie Équationnelle de Clark.
5
Yaacoub, Antoun. "Flux de l'information en programmation logique." Toulouse 3, 2012. http://thesesups.ups-tlse.fr/1787/.
Full textAbstract:
Cette thèse est développée dans le but d'aborder la question du flux de l'information en programmation logique. Les contributions de cette thèse peuvent être divisées en trois parties: 1. Flux de l'information en programmation logique: Nous proposons une base théorique de ce que pourrait être un flux de l'information en programmation logique. Plusieurs définitions de flux d'information (basées sur la réussite / échec, les substitutions réponses, bisimulation entre les arbres de résolution des buts logiques) sont évaluées et comparées. Des problèmes de décision sont donnés pour chaque définition et la complexité est étudiée pour certaines catégories de programmes logiques. 2. Bisimulation de buts logiques: Nous introduisons la notion de bisimulation entre les buts Datalog: deux buts Datalog sont bisimilaires par rapport à un programme Datalog donné lorsque leurs SLD-arbres, considérés comme des structures relationnelles, sont bisimilaires. Nous abordons le problème de décider si deux buts donnés sont bisimilaires à l'égard d'un programme donné. Lorsque les programmes sont hiérarchiques ou restricted, ce problème est décidable en 2EXPTIME. 3. Contrôle préventif de l'inférence dans les bases de données déductives: Nous proposons un mécanisme de sécurité sûr et précis pour les bases de données déductives basé sur la notion de flux de l'information dans la programmation logique<br>This thesis is developed in order to tackle the issue of information flow in logic programming. The contributions of this thesis can be split into three mains parts: 1. Information flow in logic programming: we propose a theoretical foundation of what could be an information flow in logic programming. Several information flow definitions (based on success/failure, substitution answers, bisimulation between resolution trees of goals) are stated and compared. Decision procedures are given for each definition and complexity is studied for specific classes of logic programs. 2. Bisimulation of logic goals: We introduce the concept of bisimulation between Datalog goals: two Datalog goals are bisimilar with respect to a given Datalog program when their SLD-trees, considered as relational structures, are bisimilar. We address the problem of deciding whether two given goals are bisimilar with respect to given programs. When the given programs are hierarchical or restricted, this problem is decidable in 2EXPTIME. 3. Preventive inference control for deductive databases: We propose a secure and a precise security mechanism for deductive databases based on the notion of information flow in logic programming
6
Blay-Fornarino, Mireille, and Anne-Marie Pinna. "Un modèle objet logique et relationnel : le langage Othelo." Nice, 1990. http://www.theses.fr/1990NICE4359.
Full textAbstract:
Cette thèse a pour but d'intégrer dans un système unique certains résultats de la programmation par objets, de la programmation en logique et de la programmation par relations. Ce système est alors capable de modéliser les connaissances du monde extérieur dans un formalisme permettant de les manipuler symboliquement. Cette thèse est constituée de trois parties principales. Définition d'un modèle objet abstrait dans lequel les opérations élémentaires sous-jacentes aux mécanismes mis en œuvre dans un langage à objets (création, héritage, envoi de message) sont redéfinissables par un programmeur. Un langage issu de ce modèle peut autoriser : la création d'objets de structures internes différentes pouvant communiquer entre eux ; la définition de modes d'héritage complexes ; l'expression des exceptions et des cas particuliers. Apports d'inférence déclarative au modèle objet. Le langage Othello est une implantation en Prolog du modèle abstrait dans laquelle les principaux mécanismes ont été reconsidérés afin d'attribuer aux objets des comportements logiques. Citons : la définition de méthodes polymorphes, l'envoi de message à objets anonymes, des combinaisons et du contrôle sur les méthodes dans un graphe d'héritage et des capacités intrinsèques à raisonner. Aspect relationnel de la connaissance. L’idée est d'utiliser l'approche objet pour décrire un langage de relations et ainsi faciliter l'expression des relations de dépendance et le maintien automatique de leur cohérence. Une des originalités de cette proposition est la prise en compte des modifications intervenant sur l'objet maitre pour rétablir de façon incrémentale la cohérence. Les liens de la hiérarchie proposée permettent de décrire les relations d'héritage et d'implanter une interface graphique. Une quatrième partie illustre ce travail par une application en thermique
7
MALLET, OLIVIER. "Interpretation abstraite appliquee a la compilation et la parallelisation en programmation logique." Palaiseau, École polytechnique, 1992. http://www.theses.fr/1992EPXX0011.
Full textAbstract:
L'interpretation abstraite est une technique puissante d'analyse semantique qui permet la detection de proprietes dynamiques. Elle repose sur la notion d'abstraction (ou approximation) qui remplace les elements du domaine habituel - dit concret - par ceux du domaine abstrait. Nous presentons une semantique deductive de prolog, qui approche la semantique operationnelle standard et possede une propriete de compositionnalite grace a l'utilisation de l'espace des termes quotiente par la relation de renommage et grace a une decomposition de l'operateur d'unification en deux parties independantes. Puis nous proposons pour cette semantique un interprete abstrait generique, c'est-a-dire qui necessite pour une analyse donnee un nombre tres limite d'informations decrivant le domaine et les operateurs abstraits. Cet interprete est implemente en c, fonctionne avec precision et efficacite, et n'est pas restreint aux treillis abstraits de hauteur finie. Nous utilisons ensuite cet outil pour detecter certaines familles de proprietes, et expliquons comment un compilateur ou un repartiteur de programmes prolog peut tirer parti de telles informations
8
Gandriau, Marcel. "CIEL classes et instances en logique /." Grenoble 2 : ANRT, 1988. http://catalogue.bnf.fr/ark:/12148/cb37613782d.
Full text
9
CAMP, OLIVIER. "Les contraintes en programmation logico-fonctionnelle : application au langage miles." Paris 6, 1994. http://www.theses.fr/1994PA066336.
Full textAbstract:
Depuis les annees 80 on s'est souvent penche sur l'integration des styles de programmation en logique et fonctionnelle. Le langage miles est le resultat d'une telle fusion. Il est obtenu en ajoutant a un noyau lisp les concepts d'un langage de programmation en logique: le non-determinisme, les variables logiques et l'unification. L'ajout de variables logiques dans un langage applicatif fait apparaitre de nouveaux objets: les expressions gelees. Dans cette these nous montrons comment celles-ci permettent, grace a l'unification, de definir des contraintes semblables a celles des clp. De plus, nous voyons comment on peut definir, en miles, un systeme de resolution gerant les contraintes numeriques du langage. Dans un premier temps nous nous focalisons sur les contraintes d'egalite. Nous etudions les algorithmes traditionnels de resolution de systemes lineaires et montrons comment ils doivent etre modifies pour permettre le traitement de contraintes d'egalite sur les reels. Nous montrons comment nous pouvons implanter ces algorithmes en miles pour obtenir un langage de programmation logico-fonctionnelle autorisant une utilisation active des contraintes d'egalite numeriques. Nous nous interessons ensuite aux contraintes d'inegalite numeriques du langage. Apres avoir montre comment une version modifiee de l'algorithme du simplex pouvait etre utilisee pour resoudre un systeme d'inequations lineaires de maniere incrementale, nous en proposons une definition en miles pour gerer les contraintes d'inegalite. Muni de ces deux systemes de resolution le langage miles devient un langage de programmation logico-fonctionnelle avec contraintes sur les reels. Il permet d'adopter les styles de programmation en logique avec contraintes et fonctionnel
10
Plaindoux, Didier. "Etude et conception d'un système logique orienté-objet parallèle fortement typé." Toulouse 3, 1997. http://www.theses.fr/1997TOU30315.
Full text
11
Moal, Frédéric. "Langage de biais en apprentissage symbolique." Orléans, 2000. http://www.theses.fr/2000ORLE2051.
Full textAbstract:
L'extraction de connaissances dans les bases de données (ECD) est un domaine de recherche actuellement très actif. Une problématique importante pour l'ECD est l'apprentissage supervisé, dont le but est de trouver une définition en intension d'un concept représenté par un ensemble d'exemples étiquetés comme appartenant ou non à ce concept. Dans un contexte relationnel, cette tâche, pour des raisons à la fois théoriques et pratiques, nécessite l'utilisation de biais pour adapter l'algorithme d'apprentissage aux caractéristiques du problème considéré. Nous proposons un cadre unifié et déclaratif pour la spécification et l'exploitation des biais sur l'espace des hypothèses. Notre approche repose sur la définition d'un nouveau formalisme, qui raffine les grammaires d'arbres par un langage de contraintes. Nous montrons notamment que ce formalisme permet de définir l'espace des hypothèses par unions et intersections de biais. Nous nous intéressons ensuite à l'exploration d'un tel espace, en étudiant deux approches, l'une déterministe et l'autre stochastique. Dans la première, nous proposons une nouvelle définition des opérateurs de raffinement sur les clauses utilisés en programmation logique inductive. Cette définition utilise explicitement l'espace des hypothèses et les biais, ce qui permet un élagage optimal lors de la recherche. Nous appliquons cette approche à l'ECD, en utilisant la structure de la base de données pour optimiser la base de recherche. Notre deuxième approche repose sur les algorithmes d'évolution. Nous montrons que le formalisme des grammaires d'arbres avec contraintes est particulièrement adapté à la spécification des biais en programmation génétique. Il étend en effet l'expressivité des formalismes existants, permet de modéliser les biais sur la population initiale, et de contrôler la validité des descendants lors des opérations génétiques. Nous proposons d'appliquer ce nouveau cadre pour l'induction de concepts exprimés en algèbre relationnelle.
12
Vittek, Marian. "Elan : un cadre logique pour le prototypage de langages de programmation avec contraintes." Nancy 1, 1994. http://www.theses.fr/1994NAN10372.
Full textAbstract:
La thèse décrit l'étude et l'implantation du langage ELAN qui permet de spécifier, sur une base uniforme de systèmes de calcul, différents langages de programmation logique et différents résolveurs de contraintes. ELAN est basé sur l'idée que la sémantique opérationnelle de langages de programmation logique dans le sens général du terme et la résolution de contraintes peuvent être décrites d'une façon uniforme en donnant la syntaxe des formules, l'ensemble des axiomes et l'ensemble des règles de déduction. Les deux processus peuvent être vus comme l'instance du meme schéma d'application des règles de réécriture (de déduction) sur des formules, suivant une stratégie permettant l'obtention d'une forme spéciale. La logique de réécriture, introduite par Jose Meseguer, peut être ainsi utilisée pour coder différentes logiques intéressantes. Afin de pouvoir spécifier des procédures de résolution, la thèse présente une notion de stratégie, obtenant ainsi des systèmes de calcul. Un système de calcul est alors défini par une signature décrivant la syntaxe, un ensemble de règles de réécriture définissant le mécanisme de déduction et une stratégie qui guide l'application des règles. La thèse décrit également l'implantation d'ELAN et quelques exemples de procédures de résolution réalises avec cette implantation, en particulier la sld-resolution, la surréduction, la surréduction basique, la surréduction paresseuse et l'unification syntaxique et commutative
13
Haemmerlé, Rémy. "Fermetures et modules dans les langages concurrents avec contraintes fondés sur la logique linéaire." Paris 7, 2008. http://www.theses.fr/2008PA077014.
Full textAbstract:
Cette thèse étudie l'internalisation dans les langages concurrents avec contraintes fondés sur la logique linéaire (LCC) d'un système de modules sans modification de la logique sous-jacente. Il en résulte un langage opérationnellement très simple et mono-paradigme qui incorpore nativement un grand nombre de concepts de programmation tels que le non déterminisme, les contraintes, l'affectation imperative, la gestion de la concurrence, les fermetures et l'encapsulation de code. Cette grande simplicité permet alors d'obtenir de façon directe une sémantique logique premier ordre. Dans la première partie de cette thèse nous montrons que les déclarations de procédures des langages LCC peuvent être supprimées au profit d'un nouveau type d'agent asks persistants tout en préservant la sémantique logique du langage. Nous montrons que le langage qui résulte de cette internalisation des déclarations fournit toute la puissance d'expression des fermetures des langages fonctionnels et des calculs de processus classiques à travers des encodages où les variables jouent le rôle de canaux de communication dynamiques. Dans la seconde partie nous définissons un système de modules pour cette classe de langages, dans lequel les modules peuvent être référencés par des variables. Nous démontrons que, grâce à ce système de modules, le masquage de code s'obtient alors par l'opérateur usuel de masquage des variables. Puis nous présentons un prototype d'implémentation d'une instance de ce système de modules et illustrons son utilisation en programmation avec contraintes<br>This thesis studies the internalization in the Linear logic Concurrent Constraint languages (LCC) of a module system without modifying the underlying logic. The languages resulting from this internalization have simple mono-paradigm semantics and embed numerous programming concepts such that non-determinism, constraints, imperative assignment, concurrence, closures et code encapsulation. This great simplicity of this approach allows to obtain directly first-order logical semantics. In the first part of this thesis, we show that the declarations usual in LCC languages can be taken out, to the benefit of a new "persistent ask" agent, while preserving the logical semantics of the language. We also show that the languages resulting from this internalization have all the expressive power of functional languages and usual process calculi. In the second part we define a module system for this class of languages, in which modules can be referenced by variables. We show then than the implementation hiding can be obtained with the usual variable hiding operator. Finally we present a prototype of implementation of one instance of this module system and illustrate its use in logical constraint programming
14
Codognet, Philippe. "Backtracking intelligent en programmation logique : de la théorie à l'implémentation et à l'application au parallélisme." Bordeaux 1, 1989. http://www.theses.fr/1989BOR10504.
Full textAbstract:
Proposition d'un cadre formel permettant une etude detaillee du probleme, puis d'une simplification de celui-ci en vue d'une implementation. Sa mise en uvre est ensuite exposee, suivie d'une evaluation de ses performances aussi bien vis-a-vis de prolog que des autres methodes de backfracking intelligent. Apres un etat de l'art des differentes recherches en programmation logique parallele, il est propose d'integrer du backfracking intelligent aux deux techniques de parallelisation les plus prometteuses
15
Hollant, Thierry. "Étude d'une approche objet pour la CAO électronique : application à la simulation logique." Lille 1, 1990. http://www.theses.fr/1990LIL10020.
Full textAbstract:
L'adéquation des concepts objets pour la réalisation d'environnements de conception assistée par ordinateur est étudiee au travers de la réalisation d'un simulateur logique en smalltalk. Si l'approche objet répond parfaitement aux besoins traditionnels de la cao, elle permet aussi une ouverture sur des fonctions plus originales, grâce à sa puissance de représentation des données et à ses capacités de traitement symbolique. La modularité et la ré-utilisabilité des fonctions développées amènent une forte productivité lors de l'écriture de logiciels. La rapidité de maquettage des interfaces utilisateurs garantit l'ergonomie et la convivialité, avec une présentation proche de la réalité des objets du monde réel. Les problèmes de performances, dus a une mauvaise adaptation de l'architecture des machines aux concepts objets, ne remettent pas en cause l'intérêt d'une telle approche
16
Echahed, Rachid. "Sur l'intégration des langages algébriques et logiques." Grenoble INPG, 1990. http://tel.archives-ouvertes.fr/tel-00338687.
Full textAbstract:
Ce mémoire présente l'étude d'une approche particulière des langages de programmation logico-fonctionnels, fondée sur la logique des clauses de Horn avec égalité. Nous définissons d'abord la syntaxe et la sémantique des programmes que nous considérons. La syntaxe est celle de la logique des clauses de Horn avec égalité. La sémantique est donnée par le plus petit e-modele de Herbrand associe a un programme. Nous nous intéressons ensuite au calcul dans ce langage. Nous proposons pour cela une nouvelle règle appelée sldei-resolution comme seule règle de calcul. Nous montrons sa cohérence, sa complétude ainsi que sa completude forte. La mise en œuvre de la règle sldei-resolution nécessite un algorithme de resolution d'équations. Nous étudions de tels algorithmes fondes sur la relation de surreduction, et améliorons ces algorithmes par l'utilisation de stratégies de surreduction. Cependant, ces stratégies ne sont pas complètes dans le cas général. Nous proposons alors des conditions suffisantes sur ces stratégies afin de préserver la complétude des algorithmes considérés. Nous caractérisons ensuite une classe de programmes, dits uniformes, pour lesquels l'utilisation de n'importe quelle stratégie de surreduction donne un algorithme complet de resolution d'équations. Nous donnons de plus une methode de vérification de l'uniformité d'un programme. Par ailleurs, nous proposons des conditions syntaxiques pour qu'un programme soit uniforme. Enfin, nous décrivons les principaux traits d'un langage de programmation fonde sur l'approche présentée dans ce mémoire, et l'implantation que nous avons réalisée
17
Janot, Stéphane. "Règles d'évaluation équitables en programmation logique." Lille 1, 1991. http://www.theses.fr/1991LIL10062.
Full textAbstract:
Les interpréteurs Prolog ne sont pas complets en général pour les échecs et pour les succès car ils sont basés sur un parcours de l'arbre de résolution en profondeur d'abord associé à une gestion des buts en pile. Cependant, la résolution SLD sur laquelle Prolog est basé est correcte et complète. L'utilisation d'une règle d'évaluation équitable―tout sous-but qui apparaît dans une dérivation infinie est effectivement sélectionné―permet d'obtenir tous les échecs finis et tous les succès finis d'un programme: s'il existe un arbre de dérivation SLD fini pour un programme P et un but B, alors tout arbre de dérivation équitable pour P et B est fini. Un interpréteur Prolog équitable permet donc d'éviter toutes les boucles liées à l'ordre d'évaluation des sous-buts. Nous étudions l'utilisation de règles d'évaluation équitables en Prolog, des aspects théoriques aux aspects pratiques. Deux modèles de règles d'évaluation équitables, Pile-indicée et Arbres-de-buts-indicés sont proposés. Ces stratégies de dérivation sont basées sur l'utilisation d'indices de dérivation pour contrôler l'ordre d'évaluation des sous-buts. Des implémentations efficaces de ces règles ont été réalisées. Les problèmes pratiques liés à l'utilisation d'un ordre d'évaluation différent sont pris en compte et nos interpréteurs équitables sont effectivement utilisables
18
Guérin, Jean-Luc. "Grafolog : un système de programmation logique et objets sans variables par le dessin." Compiègne, 1991. http://www.theses.fr/1991COMP393S.
Full textAbstract:
La thèse que nous défendons est que la programmation visuelle offre de nombreux avantages pour la représentation des connaissances logiques. C'est dans ce but que nous avons défini et implémenté le langage graphique Grafolog (graphique, objets, et logique) qui permet à un utilisateur de représenter graphiquement des relations entre objets logiques. L'utilisateur définit et interroge des connaissances en dessinant, dans un formalisme graphique unifié. Notre manuscrit commence par un état de l'art, illustre de nombreux exemples, sur la visualisation de programmes et la programmation visuelle. Dans cette présentation, nous essayons de réaliser un classement des différentes approches pouvant être rencontrées aujourd'hui dans ces deux domaines. Le chapitre suivant est consacré à une brève description du prolog orienté objet sous-jacent à notre système, U-Log, conçu et développé par Paul Y. Gloess à l'université de technologie de Compiègne. Le troisième chapitre décrit Grafolog en tant que langage graphique. La description de la sémantique de notre langage y est effectuée par référence au modèle objet logique D’U-Log. L'idée de base de Grafolog, consiste à représenter les objets logiques par des boites, et les relations entre objets par des flèches. Bien qu'apparemment très simple, ce formalisme s'avère d'une grande puissance expressive, tout en s'affranchissant complètement de l'utilisation de variables. Nous terminons ce chapitre par une discussion des différentes applications possibles de notre système: interface pour base de données, enseignement de prolog, mise au point et explication graphique. Ce dernier point est rendu possible par le dessin du schéma d'interférence D’U-Log en Grafolog. Le dernier chapitre concerne l'implémentation de notre système et plus particulièrement la manière dont a été réalisé le lien entre Grafolog et U-Log. En annexe, nous donnons un manuel d'utilisation de Grafolog dans sa version actuelle. Cette partie met l'accent sur l'interface graphique et les différents outils disponibles pour faciliter l'utilisation du langage graphique.
19
Rigotti, Christophe. "Structure des objets et raisonnements dans les langages de clauses : Application à l'optimisation sémantique de requêtes." Lyon, INSA, 1996. http://www.theses.fr/1996ISAL0036.
Full textAbstract:
Ce travail porte sur l'étude de l'intégration de la structure des objets dans les langages de clauses et son application dans le domaine des bases de données. Dans la première partie nous mettons en évidence trois familles de langages, correspondant à trois utilisations différentes de la structure des objets dans les raisonnements sur des clauses. Nous montrons, dans la seconde partie, que deux de ces formes de raisonnement peuvent être combinées, permettant ainsi d'utiliser simultanément la structure des objets comme contrainte au niveau des termes et comme information connue ou déduite. Nous construisons un tel outil de raisonnement pour lequel nous donnons une sémantique déclarative et une sémantique opérationnelle équivalente. Dans la troisième partie, nous employons ces possibilités de représentation et de raisonnement pour décrire et reformuler des requêtes dans les bases de données déductives orienté-objet. Dans ce contexte, nous construisons un cadre original d'optimisation sémantique de requêtes, dont l'intérêt principal est d'autoriser la combinaison de deux schémas d'optimisation complémentaires existants<br>We study the integration of abject structures in clauses and its application in the field of databases. In the first part, we describe three families of languages, corresponding to three kinds of reasoning over abject structures in clauses. In the second part, we point out that two of these reasoning schemes can be combined to use abject structures as constraints over terms and as known or deduced information. We design such a reasoning tool and provide its declarative and operational semantics. In the third part, we apply these representation and reasoning possibilities to describe and reformulate queries in deductive object-oriented databases. This leads to an original application: a novel framework for semantic query optimization, combining two complementary optimization schemes
20
Girlando, Marianna. "On the proof theory of conditional logics." Electronic Thesis or Diss., Aix-Marseille, 2019. http://www.theses.fr/2019AIXM0038.
Full textAbstract:
La thèse se place à l’intersection de trois sujets de recherche: logiques conditionnelles, théorie de la démonstration et sémantique de voisinage. La famille de logiques conditionnelles considérées provient des ouvrages de Stalnaker et Lewis. Elle est une extension de la logique classique propositionnelle avec un opérateur modal à deux places, qui exprime une notion affiné de conditionnalité. La sémantique de ces logiques est définie en termes de modèles de voisinage. Le but de la recherche est d’étudier la théorie de la démonstration des logiques conditionnelles, en précisant leur calculs des sequents. Les calculs définis sont des extensions du calcul des sequents de Gentzen; ils sont étiquetés, c’est à dire définis en enrichissant le langage, ou internes, qui rajoutent des connecteurs structurels aux sequents. La thèse est organisée en six chapitres. Le chapitre 1 présente les axiomes et la sémantique des logiques conditionnelles et le chapitre 2 introduit la théorie de la démonstration. Les contributions originelles au sujet sont traitées dans les chapitres 3 - 6. Le chapitre 3 introduit des calculs de sequents étiquetés basés sur la sémantique de voisinage pour les logiques conditionnelles préférentielles. Le chapitre 4 présente différents systèmes internes de calcul pour les logiques counterfactuelles, une sous-famille des logiques préférentielles. Le chapitre 5 analyse la relation parmi les systèmes de preuve en présentant les deux côtés d’une traduction entre un calcul étiqueté et un calcul interne. Finalement, au chapitre 6, les méthodes de la théorie de la démonstration conditionnelle sont appliqués à une logique épistémique multi-agente<br>This thesis can be ideally placed within the intersection of three research topics: conditional logics, proof theory and neighbourhood semantics. The family of logics under scope stems from the work of Stalnaker and Lewis, and extends classical propositional logic by means of a two-place modal operator, which expresses a fine-grained notion of conditionality. The semantics of these logics is modularly defined in terms of neighbourhood semantics. The research aim is to investigate the proof theory of conditional logics, by defining sequent calculi for them. The proof systems introduced are extensions of Gentzen’s sequent calculus; they are either labelled, defined by enriching the language, or internal, which add structural connectives to the sequents. Moreover, the calculi are standard: they are composed of a finite number of rules, each displaying a fixed number of premisses. The thesis is organized in six chapters. Chapters 1 contains an axiomatic and semantic overview of conditional logics, while chapter 2 is a short introduction to proof theory. The original contributions to the subject are presented in chapters 3 – 6. Chapter 3 introduces labelled calculi based on neighbourhood models for preferential conditional logics, and chapter 4 presents different internal proof systems covering counterfactual logics, a subfamily of preferential logics. Chapter 5 analyses the relationship between proof systems by presenting a mapping between a labelled and an internal calculus. Finally, the proof-theoretic methods developed for conditional logics are applied in chapter 6 to the multi-agent epistemic logic
21
Marquez, Alonso. "La résolution hiérarchisée, une solution au problème de la négation en programmation logique." Paris 11, 1988. http://www.theses.fr/1988PA112167.
Full textAbstract:
L'objectif de cette thèse est d'étendre à la logique des prélicats du premier ordre la notion de sémantique procédurale existante dans le langage prolog. Ceci permet d'augmenter l'efficacité et la clarté de la programmation en logique du premier ordre
22
Jacquenet, François. "Contribution à l'intégration de concepts et de mécanismes de langages avancés pour la programmation logico-fonctionnelle : le langage VEGA." Besançon, 1988. http://www.theses.fr/1988BESA2040.
Full textAbstract:
Caractérisation des concepts et des mécanismes de langages de programmation avances qui permettraient d'améliorer le développement d'applications orientées intelligence artificielle. Intégration cohérente de certaines de ces notions dans un langage de programmation expérimental appelé VEGA
23
Kauffmann, Hervé. "Multilog : utilisation de mondes en programmation logique pour représenter et manipuler des connaissances." Paris 6, 1986. http://www.theses.fr/1986PA066079.
Full textAbstract:
Multilog est un langage de programmation logique. Ses principales caractéristiques sont les suivantes : les connaissances sont réparties dans différents mondes; chaque monde a son propre mécanisme d'inférence, qui indique quelles inférences peuvent être faites à partir des clauses de la base de connaissances, et comment les faire; trois relations d'héritage permettent de relier les différents mondes: une relation d'héritage total, une relation d'héritage par défaut et une relation d'héritage avec exceptions. Les principales applications de multilog sont : le raisonnement hypothétique, la représentation de différents points de vue, le raisonnement non monotone, le raisonnement distribué.
24
Drissi, Talbi Abdenbi. "Cadre multi-niveaux de programmation logique et orientée objet : étude, extensions et réalisation." Rouen, 1996. http://www.theses.fr/1996ROUES033.
Full textAbstract:
Cette thèse propose un cadre de programmation hybride fondé sur la programmation logique (PL) et la programmation orientée objet (POO), et étendu par la résolution des contraintes linéaires en nombres naturels. Le langage LOP associé à ce cadre offre une programmation pouvant être statique ou dynamique, déclarative ou procédurale. Le système proposé se compose d'une hiérarchie à trois niveaux de programmation permettant une fusion progressive et non limitative de la PL et de la POO. Chacun de ces niveaux privilégie une facette du mariage de ces deux paradigmes. Le niveau de base, appelé NPO, propose une programmation par objets logiques statiques. Il préserve les avantages de la programmation en Prolog pur, tout en améliorant la structuration des programmes. Le second niveau, appelé NP1, est une extension de NPO par des aspects dynamiques de la POO adaptés à l'esprit de la programmation déclarative. NP1 propose une programmation à la fois dynamique et déclarative par objets logiques multi-états et par méthodes logiques multi-définitions. Le dernier niveau, appelé NP2, intègre des mécanismes de programmation qui sortent du cadre déclaratif fixe au niveau NP1. D'une part, il complète NP1 par des mécanismes de contrôle, nécessaire à la réalisation d'un grand nombre d'applications. D'autre part, il intègre un nouveau modèle de simulation discrète orientée processus, ou les calculs temporels et la gestion des processus sont effectués par un solveur de contraintes. Le langage LOP et son interpréteur sont entièrement conçus par objets et implantés en clos.
25
Legrand, Rémi. "Calcul relationnel et programmation en logique." Paris 6, 1987. http://www.theses.fr/1987PA066481.
Full textAbstract:
Presentation d'un systeme de programmation en logique base sur le calcul relationnel: description du langage sans variable graal et son extension relationnelle grel; definition des relations; introduction des indeterminees, decomposees en inconnues et gelees dans la programmation fonctionnelle; presentation de prolog et de ses contraintes; construction du langage logique relog a partir de grel, a l'aide d'un orienteur
26
Ngomo, Macaire. "Contribution à l'intégration de la programmation logique et de la programmation par objets : étude, conception et implantation." Rouen, 1996. http://www.theses.fr/1996ROUES039.
Full textAbstract:
Cette thèse prend place dans un projet interne de réalisation de langages à vocation multiple, intégrant plusieurs styles de programmation et adaptés au plus près à nos besoins en matière de conception et programmation des applications. Dans celle-ci, nous étudions les possibilités de combiner les aspects de deux paradigmes de programmation : la programmation logique et de la programmation par objets. Ces dernières années, ces deux paradigmes de programmation ont suscité un intérêt de plus en plus grand parce qu'ils offrent beaucoup d'avantages sur les méthodes traditionnelles de programmation. Dans cette thèse, nous proposons un nouveau modèle pour intégrer ces deux paradigmes de programmation, en mettant en avant l'aspect déclaratif de la programmation logique. Sur la base de ce modèle, nous développons un nouveau langage nommé OO-Prolog (object-oriented Prolog). Ce langage intègre de manière cohérente les grands mécanismes de la programmation logique et de la programmation par objets. Il est basé sur Delphia-Prolog et conçu suivant le modèle métaclasse/classe/instance inspiré du modèle ObjVlisp. L'héritage est dynamique et multiple, avec une sémantique non monotone. Une nouvelle méthode de résolution des conflits est proposée. Elle est basée sur la résolution non-déterministe. Un mécanisme de versions d'objets est proposé permettant de construire l'histoire d'un objet par unification et de la défaire par retour arrière. Ce mécanisme repose sur l'utilisation des structures de données incomplètes. L'aperçu d'une structure incomplète peut s'utiliser pour permettre l'entrée de nouvelles informations moyennant l'unification et donc de prévoir l'avenir. La lecture déclarative des programmes utilisant ces structures est immédiate. De façon opératoire, ces programmes se comprennent en termes de construction d'une structure par incrémentation. Un schéma d'extension de l'unification est proposé, prenant en compte le concept d'identificateur d'objet.
27
Bouquard, Jean-Louis. "Etude des rapports entre grammaires attribuees et programmation logique : application au test d'occurrence et a l'analyse statique." Orléans, 1992. http://www.theses.fr/1992ORLE2009.
Full textAbstract:
La relation entre programmation logique et grammaires attribuees est reprise de travaux precedents et adaptee de maniere a etre utilisee par la suite. Une premiere application concerne le test d'occurrnce. Une nouvelle propriete des annotations propres est etablie et un algorithme polynomial de determination de ces annotations est elabore. Ceci fournit un test efficace d'appartenance a une large classe de programmes non sujets au test d'occurence (nsto). Puis, une amelioration supplementaire est obtenue par une methode basee sur une transformation de programme. Ensuite, on effectue une comparaison entre, d'une part, l'execution de prolog par l'intermediaire de la machine abstraite de warren et, d'autre part, l'evaluation des attributs par le systeme fnc2. Il en ressort qu'un programme logique peut beneficier des optimisations elaborees sur les evaluateurs d'attributs s'il possede une propriete dite de decoration. Ceci nous amene a introduire la notion d'arguments decisifs d'un programme logique. Un algorithme polynomial de determination de ces arguments est construit, ce qui apporte la possibilite d'applications pratiques
28
He, Ying. "L'apprentissage des structures conditionnelles en informatique." Paris 5, 1991. http://www.theses.fr/1991PA05H076.
Full textAbstract:
Lors des acquisitions en pragrammation, des connaissances prealables peuvent servir de precurseurs; elles interagissent alors avec les concepts informatiques. Toutefois l'integration de ces connaissances anterieures exige la construction de representations mentales du dispositif informatique. Cette these a comme objectif de chercher a mettre en evidence, dans l'acquisition des structures conditionnelles, d'une part la nature des prerequis, d'autre part les interactions entre l'utilisation par des sujets de structures conditionnelles et les representations du fonctionnement du dispositif informatique. Nous avons travaille essentiellement avec des eleves en phase d'alphabetisation, c'est-a-dire la phase des 30 a 50 premieres heures d'enseignement. Les resultats montrent d'une part que des connaissances logiques sont des conditions necessaires de l'apprentissage des structures conditionnelles en informatique mais ne sont pas suffisantes; d'autre part de nombreux eleves utilisent les formes de la communication naturelle lors de la communication avec le dispositif informatique. Un modele de presupposition (le modele pres) est introduit pour rendre compte de la difference entes les connaissances logiques et la reussite dans des taches de programmation<br>During the acquisition of programming concepts, prior knowledge may serve as "precursor" and interacts with the concepts of computer science; nevertheless the integration of prior knowledge in the new frame requires the formation of mental representations on this device. In this work, a review is presented on the results concerning beginner's acquisitions. And two experiments on conditional structures (with 10th and 11th grade students) are reported: they show that logical knowledge is a prerequisite to the acquisitions of conditional structures but is not sufficient to insure acquisition. Properties of natural communication are used by many beginners when they need to handle dialog with an computer in programming tasks. A model, termed the pres-model is defined, which accounts for the discrepancy observed between logical knowledge and success on programming tasks
29
Bourzoufi, Abdelhafid. "Définition et évaluation d'une machine abstraite parallèle pour un modèle OU-parallèle multi-séquentiel de PROLOG." Lille 1, 1992. http://www.theses.fr/1992LIL10021.
Full text
30
Robert, de Saint Victor Isabelle. "Système déductif dans le contexte de données réparties." Lyon 1, 1988. http://www.theses.fr/1988LYO10084.
Full textAbstract:
La cooperation de prolog avec des bases de donnees est une strategie possible pour construire une base de connaissances. Elle permet d'utiliser l'acquis dans les domaines de l'inference par prolog et de la gestion des donnees avec les sgbds. Dans l'approche presentee, le dialogue entre prolog et les sgbds est realise par un processeur de communication. Son role est triple: 1) vehiculer l'information d'une maniere bidirectionnelle entre les deux systemes; 2) traduire les besoins en information, issus de prolog et exprimes en algebre relationnelle etendue, en requetes dans les langages de manipulation de donnees des sgbds; 3) gerer la repartition des donnees par un jeu d'operateurs algebriques et resoudre des requetes recursives
31
Cras, Jean-Yves. "Snail : une approche ensembliste pour l'intégration de types et fonctions en PROLOG." Paris 11, 1987. http://www.theses.fr/1987PA112323.
Full textAbstract:
Un nouveau paradigme de calcul appelé programmation ensembliste, est présente. La notion de programme ensembliste est définie et une théorie du modèle construite. Des règles d'inférence, correctes et complètes pour cette sémantique, sont données. Snail est une extension compatible de prolog dont la sémantique déclarative est celle de la programmation ensembliste
32
Pavillet, Gabriel. "Des langages de programmation à objets à la représentation des connaissances à travers le MOP : vers une intégration." Montpellier 2, 2000. http://www.theses.fr/2000MON20072.
Full textAbstract:
L'introduction du paradigme objet dans l'informatique a connu un succes et un essor considerable durant ces dix dernieres annees. L'objectif de nos travaux est d'etudier la possibilite et l'opportunite d'une integration de deux grands domaines de l'informatique, tous deux champs d'application de la notion d'objet : la programmation par objets (issue du genie logiciel) et la representation des connaissances par objets (issue de la representation des connaissances). La premiere partie de notre travail a consiste a etudier, a travers le probleme test de l'implementation des slots-booleens, divers langages a objets reflexifs, clos, power-classes et openc + +, extensibles grace a leur protocole de meta-objets (ou mop), dans le but de choisir le langage de programmation objet le plus adequat pour cette integration. En definitive, c'est le langage claire, ne possedant pas encore de mop, qui a ete retenu pour cette integration et nous avons specifie les diverses modifications a apporter a ce langage pour obtenir un mop extensible au-dessus de ce langage. Pour le systeme de representation de connaissances, c'est la logique de description fact, ayant un pouvoir d'expression important et d'excellentes performances qui a ete consideree pour l'integration. L'integration consiste a associer a chaque classe du langage, un concept de la logique de description, et a chaque objet un individu de la base de connaissances (et reciproquement). Elle se deroule en trois etapes : implementation de fact dans le langage claire, puis ajout d'une partie raisonnement de la abox sur cette implementation ; et finalement, a partir du systeme obtenu, specification des principes de l'integration en claire du systeme fact augmente d'une abox.
33
Maingaud, Séverine. "Certification de programmes impératifs en logique dynamique : le cas du lambda-calcul avec références." Paris 7, 2011. http://www.theses.fr/2011PA077200.
Full textAbstract:
Nous présentons un système formel de certification de fiabilité logicielle, MLDL, dédié à un lambda-calcul non typé contenant des références d'o/\ supérieur (MLimp). MLDL est basé sur une logique dynamique (DL) du second ordre dont le système déductif combine des étapes de déduction purement logiques et des étapes d'évaluation symbolique. Les modalités spécifiques de MLDL sont de trois types: les boîtes standard de DL sont adaptées à MLimp où tout programme est une expression, les updates permettent de représenter les modifications de la mémoire et un le v-lieur prend en charge l'allocation de nouvelles adresses. La thèse comporte deux volets : un volet syntaxique consacré à la présentation de MLDL, et un volet sémantique consacré à la construction d'un modèle de MLDL afin de prouver la cohérence du formalisme. Ce modèle est construit à partir d'un modèle dénotationnel de MLimp construit avec des techniques standard de résolution d'équations dans la catégorie des dcpo et la catégorie des cpo avec injections-projections. Nous développons également une théorie des actions de groupe sur les dcpo (appliquée en particulier au groupe des permutations d'adresses) ainsi que la relation de domination qui nous permettent de traiter les questions d'invariance liées à la manipulation des adresses mémoire<br>We present a formal System of software verification, MLDL, dedicated to an untyped S\lambdaS-calculus with higher-order references (MLimp) and call-by-value evaluation. MLDL follows a certification approach which consists in proving the correspondence between a program and its specification. MLDL is based on a second-order dynamic logic which combines purely logical deduction steps with symbolic evaluation. There are three types of modality in MLDL: the box of dynamic logic is adapted to MLimp where each program is an expression, updates represents local modifications of the memory and a specific binder (the v-binder) supports allocation of new memory cell. The thesis consists oftwo parts: a syntactic part devoted to the presentation ofMLDL and a semantic part devoted to the construction of a model of MLDL in order to prove the consistency of the formalism. The model ofMLDL is built on a denotational model of MLimp where congruent (through symbolic evaluation) programs belong to the same équivalence class. This denotational model is built with standard techniques ofsolving equations in the category ofdcpos and the category of cpos with injections- projections. We also develop a theory ofgroup action on the dcpo (especially applied to the group of permutations of addresses) and a notion of domination over programs and stores by a set of addresses. These new tools allow to deal with issues of well-foundness and invariance associated with the manipulation of memory locations
34
Grente, Theo. "Caractérisation et programmation en théorie des langages et en logique des classes de complexité efficace des automates cellulaires." Thesis, Normandie, 2020. http://www.theses.fr/2020NORMC214.
Full textAbstract:
Les automates cellulaires constituent le modèle de calcul parallèle et local par excellence.Comme pour tout modèle du parallélisme, leur programmation est réputée difficile. La puissance de calcul des automates cellulaires, modèle le plus simple du parallélisme, est attestée par le fait que nombre de problèmes significatifs sont calculés en temps minimal, appelé temps-réel, surautomate cellulaire.Principal résultat de cette thèse, on démontre des liens exacts (des équivalences) entre d’un côté la complexité descriptive, essentiellement la définissabilité en logique du second ordre existentiel sur des formules de Horn, de l’autre les classes de complexité en temps-réel des automates cellulaires.Au-delà de cette caractérisation en logique de la complexité en temps minimal, la thèse établit une méthode de programmation parallèle. Cette méthode consiste dans un premier temps à programmer dans nos logiques de Horn l’induction résolvant un problème, puis dans un secondtemps, à appliquer un processus automatique aboutissant au programme de l’automate cellulaire résolvant le problème. Pour justifier l’intérêt de la méthode, la thèse présente un ensemble de programmes logiques pour une variété représentative de problèmes classiques connus pour êtrecalculables en temps-réel sur automates cellulaires.Par ailleurs, toujours en passant par nos logiques, on prouve divers résultats liant le temps-réel des automates cellulaires et les grammaires formelles. Typiquement, tout langage généré par une grammaire algébrique et, plus généralement, une grammaire conjonctive d’Okhotin, est reconnu en temps-réel sur un automate cellulaire de dimension 2<br>Cellular automata constitute the model of parallel and local computation by excellence.As for any model of parallelism, their programming is known to be difficult. The computingpower of cellular automata, the simplest model of parallelism, is attested by the fact that manysignificant problems are computed in minimal time, called real-time, on cellular automata.The main result of this thesis is the demonstration of exact links (equivalences) between, on onehand, the descriptive complexity, essentially the definability in existential second order logic on Horn formulas, and, on the other hand, the real-time complexity classes of cellular automata.Beyond this characterization in logic of the complexity in minimal time, the thesis establishes a method of parallel programming. This method consists first of all in programming in our Horn ogics the induction solving a problem, then in a second step, in applying an automatic process leading to the program of the cellular automaton solving the problem. To justify the interest of the method, the thesis presents a set of logic programs for a representative variety of classical problems known to be computable in real-time on cellular automata.In addition, we prove various results linking the real time of cellular automata and formal grammars. Typically, any language generated by an algebraic grammar and, more generally, an Okhotin conjunctive grammar, is recognized in real-time on a 2-dimensional cellular automaton
35
Maakeb, Abd El Kader. "Conception et réalisation d'un couplage entre les langages de programmation en logique et les bases de données hétérogènes." Lyon 1, 1986. http://www.theses.fr/1986LYO10013.
Full text
36
Maakeb, Abd el Kader. "Conception et réalisation d'un couplage entre les langages de programmation en logique et les bases de données hétérogènes." Grenoble 2 : ANRT, 1986. http://catalogue.bnf.fr/ark:/12148/cb37599281m.
Full text
37
Lallouet, Arnaud. "Modularité, validation et parallélisme de données en programmation logique." Orléans, 1996. http://www.theses.fr/1996ORLE2012.
Full textAbstract:
La contribution de cette thèse est double: d'une part, il s'agit d'étudier le problème de la validation de propriétés déclaratives de programmes logiques dans un contexte compositionnel, d'autre part de proposer une extension de la programmation logique au parallélisme de données. L'absence de compositionnalité des sémantiques utilisées en programmation logique a engendré des difficultés a concevoir un système de modules qui lui seraient adapté, et donc des méthodes de validation modulaires. Nous nous proposons de répondre à cette question en définissant d'une part des extensions compositionnelles pour deux sémantiques classiques : la sémantique bien-fondée et la sémantique de Fitting, et d'autre part des méthodes de validation modulaires concernant des propriétés déclaratives pour ces deux sémantiques. L'assurance de la correction d'un programme est obtenue simplement à partir de la correction des modules le composant. L'application de ce formalisme est faite dans le cadre du système de modules de Godel et dans celui de la programmation logique inductive. Le parallélisme de données consiste à appliquer la même opération simultanément sur des données différentes. Nous présentons une proposition de langage de programmation logique, appelée DP-LOG intégrant les concepts du modèle de programmation à parallélisme de données. Il permet la manipulation globale de vecteurs et dispose d'une primitive de communication générale permettant la délocalisation d'une partie de la preuve. Nous lui donnons une sémantique déclarative et une sémantique opérationnelle. Une application possible est le prototypage de programmes massivement parallèles
38
CONRAD, THIERRY. "Equator : un langage de programmation logique type fonde sur l'unification equationnelle." Paris 11, 1990. http://www.theses.fr/1990PA112146.
Full textAbstract:
L'arrivee de prolog a constitue une avancee majeure dans le domaine des langages de programmation. Dans sa version de base, ce langage souffre toutefois de la pauvrete de son environnement de programmation. L'idee a la base de ce travail est d'etendre prolog de facon a le rendre plus sur et plus efficace. Nous pensons avoir contribue de facon originale a la realisation de cette idee grace a une technique baptisee typage equationnel. Cette approche a pour caracteristique essentielle d'unifier et donc de simplifier au maximum les concepts utilises. Nous exposons en detail nos motivations en enumerant un certain nombre de points constituant les faiblesses de prolog. Nous degageons de cela une idee directrice centree sur le typage qui doit permettre d'apporter des solutions de facon homogene. Nous decrivons le langage qui servira de support aux enrichissements proposes. Ce langage qui est un sur-ensemble de prolog est fonde sur la notion d'unification equationnelle. Le typage equationnel est defini et les proprietes de polymorphisme du langage sont etudiees. Un module d'inference de types qui complete notre systeme est egalement decrit. Nous proposons des exemples d'application et decrivons en detail une implementation du langage
39
Loddo, Jean-Vincent. "Généralisation des Jeux Combinatoires et Applications aux Langages Logiques." Phd thesis, Université Paris-Diderot - Paris VII, 2002. http://tel.archives-ouvertes.fr/tel-00008272.
Full textAbstract:
La théorie des jeux a développé, à ses débuts, une vocation pour les sciences sociales et économiques, avec des applications disparates, comme par exemple le traitement de données médicales. Elle apparaît aujourd'hui comme un paradigme de concepts et de techniques très général, dont le potentiel reste encore à exploiter en informatique. Dans cette thèse nous étudions une branche particulière, la théorie des jeux combinatoires (à deux joueurs), pour en tirer bénéfice dans le domaine, très actif, des sémantiques formelles des langages de programmation. D'un jeu, nous pouvons séparer l'aspect syntaxique, inhérent aux dénouements possibles des matchs, de l'aspect sémantique, inhérent aux prévisions sur le gagnant et la quantification de son gain (en termes d'un enjeu quelconque, tel que l'argent ou le préstige). Pour modeliser la notion de gain, la structure d'évaluation choisie ne doit pas forcément être celle des booléens (gagné ou perdu), ou celle des entiers naturels ou relatifs. Il suffit qu'elle vérifie des propriétés, assez faibles, garantissant l'existence d'une sémantique même lorsque le jeu donne lieu à des matchs infinis, comme dans le cas du jeu de la bisimulation entre processus concurrents, et du jeu de la programmation logique. Dans ce travail, nous étudions la caractérisation sémantique d'un langage logique (avec ou sans contrainte) en termes de jeu à deux joueurs. Au-delà du modèle intuitif des jeux, dont la valeur pédagogique mériterait d'être approfondie, une telle interprétation permet de réutiliser un des algorithmes les plus utilisés dans la théorie des jeux combinatoire, Alpha-Bêta, comme moteur de résolution pour les langages logiques. Les résultats récents et spectaculaires obtenus par les programmes d'échecs (souvenons-nous de la défaite du champion du monde Kasparov contre le programme Deep Blue d'IBM) témoignent d'une forme d'intelligence artificielle développée dans ces programmes qui peut être transposée et exploitée dans la résolution des langages logiques. La résolution d'interrogations existentielles conjonctives dans une théorie de clauses de Horn du premier ordre est en particulier concernée. En effet, la capacité d'Alpha-Bêta à simplifier le calcul ou, en d'autres termes, sa capacité à éliminer les coups inintéressants, n'est pas intimement liée à un type de jeu ou à un type de gain particuliers, mais demande juste des propriétés algébriques qui sont satisfaites dans le jeu de la programmation logique. La correction d'Alpha-Bêta est prouvée de façon formelle pour un éventail de structures très large. Les valeurs calculées pourront être aussi bien des entiers naturels, comme dans le cas du jeu d'échecs, que des substitutions ou des contraintes, comme dans le cas des langages logiques.
40
Diaz, Daniel Deransart Pierre. "Étude de la compilation des langages logiques de programmation par contraintes sur les domaines finis le système clp (FD) /." Le Chesnay : INRIA, 1995. ftp://ftp.inria.fr/INRIA/publication/Theses/TU-0329.ps.gz.
Full text
41
Oros, Hernandez Miguel Angel. "Conception, implantation et optimisation d'un langage à objets logiques." Bordeaux 1, 1995. http://www.theses.fr/1995BOR10599.
Full textAbstract:
En partant d'approches declaratives au probleme de l'extension de prolog a des objets, telles que les psi-termes de ait-kaci ou les termes a traits de backofen et smolka, nous proposons un nouveau langage d'acces logique incremental a des objets, qui est essentiellement une extension de datalog a des contraintes traduisant l'aspect objet. Nous etudions certains aspects d'optimisation, symbolique au niveau des contraintes, par rapport a une signature, physique au niveau des acces. Une restriction d'un langage ideal propose est implantee en common lisp sous le nom de u-log 3. Nous abordons egalement le probleme de la classification de predicats datalog, dans la perspective de pouvoir utiliser dans les contraintes des sortes ou des traits definis en logique, et pas simplement interpretes dans une base. Une methode exacte, basee sur la deduction naturelle, est proposee pour attaquer ce probleme indecidable, et implantee en prolog iii dans le prototype concept
42
Jourdan, Muriel. "Etude d'un environnement de programmation et de vérification des systèmes réactifs, multi-langages et multi-outils." Phd thesis, Université Joseph Fourier (Grenoble), 1994. http://tel.archives-ouvertes.fr/tel-00005099.
Full textAbstract:
Ce travail porte sur la programmation et la verification des systemes reactifs. Il consiste dans une premiere partie en la definition d'un langage mixte imperatif/declaratif, nomme ArgoLus, fonde sur les langages synchrones Argos et Lustre. Argos est un langage imperatif a base d'automates paralleles et hierarchises. Lustre est un langage declaratif fonde sur le modele flots de donnees. Le langage ArgoLus permet de melanger au niveau source ces deux langages. La definition des traductions structurelles d'ArgoLus en Argos ou en Lustre offre deux solutions interessantes pour mettre en oeuvre ce langage, tout en profitant des environnements deja existants. Dans un deuxieme temps la semantique d'Argos en termes de graphes temporises a ete definie. Initialement, celle-ci est definie en termes de systemes de transitions etiquetees. L'inconvenient de ce modele est lie au phenomene d'explosion du nombre d'etats qui limite les possibilites de verification formelle. Une des causes de cette explosion est la presence dans les programmes de compteurs d'occurrences d'evenement. Les graphes temporises sont des automates etendus avec des compteurs de temps, dont la taille est independante des valeurs limites des compteurs du programme. Par consequent, ils sont moins sensibles au phenomene d'explosion du nombre d'etats, d'ou une amelioration des possibilites de verification formelle. De plus, il est possible grace a ce modele d'exprimer des proprietes quantitatives faisant reference au temps. Enfin, un troisieme aspect de ce travail porte sur l'utilisation pour les systemes reactifs d'outils de verification formelle, non concus exactement pour ce type de systemes.
43
Piccolo, Mauro. "Linearity and beyond in demotational semantics." Paris 7, 2009. http://www.theses.fr/2009PA077202.
Full textAbstract:
Dans cette thèse, nous proposons une exploration de la notion de linéarité, dans plusieurs de ses aspects. Par le terme "linéarité" nous entendons tous les concepts plus au moins liés aux idées qui sont à l'origine de la Logique Linéaire de Girard. Plus précisément, dans cette thèse nous présentons le langage S1PCF, un langage de programmation sémantiquement linéaire. S1PCF est dénotationellement linéaire car il est conçu comme la contrepartie syntaxique des Fonctions Linéaires Stables des Espaces Cohérents. Nous étudions des modèles dénotationnels de S1PCF, nous montrons un résultat de full abstraction et nous discutons des extensions de ce langage. Nous présentons un modèle syntaxique de S1PCF en donnant un codage fidèle de ce langage de programmation dans un langage de processus appelé linProc. Nous poursuivons notre étude de la linéarité dans les langages de processus, en proposant la Ludique de Girard comme un outil mathématique abstrait pour étudier des propriétés importantes des processus, comme la liveness ou l'absence de deadlock. Nous donnons un modèle sémantique du pi-calcul linéaire dans une version modifiée de la Ludique conçue pour valider la règle du Mix. Enfin, nous allons au-delà de la linéarité en donnant une caractérisation logique de la stabilité, en utilisant les types intersections. Nous définissons deux systèmes d'assignation de type pour le lambda-calcul qui sont paramétriques sur une relation de cohérence entre types. Nous prouvons que ces systèmes donnent une caractérisation logique de deux classes intéressantes de modèles du lambda-calcul<br>In this thesis we propose an exploration of the notion of linearity in its many respects. By the term linearity, we in fact refer to different concepts, more or less related to the ideas underlying Girards Linear Logic. More specifically, in this thesis we present the language SlPCF, a semantically linear programming language. SlPCF is linear in a denotational sense since it is conceived to be the syntactical counterpart of Linear Stable Functions among Coherence Spaces. We study some denotational models of SlPCF, we show a full abstraction result and we discuss some extensions of this language. We present a syntactical model of SlPCF by giving a faithful translation of this programming language into a linear process language, called f/nProc. We continue our study of linearity in process languages by proposing Girard's Ludics as an abstract mathematical tool to study some important properties of processes, like liveness or deadlock-freeness. In particular we give a semantics model of linear pi-calculus into a modified version of Ludics, conceived to validate the Mix-rule. Finally, we go beyond linearity by giving a logical characterization of stability using intersection types. We define two intersection type assignment Systems for A-calculus, parametric with respect to a coherence relation between types. We show that such Systems give a logical characterization of two interesting classes of A-calculus models
44
Gaboardi, Marco. "Linéarité : un outil analytique pour l'étude de la complexité et de la sémantique des langages de programmation." Thesis, Vandoeuvre-les-Nancy, INPL, 2007. http://www.theses.fr/2007INPL099N/document.
Full textAbstract:
Dans la première partie, on propose un système de type pour le lambda-calcul, dans le style du calcul des séquents, nomme « Soft Type Assignment » (STA) qui est inspiré par la logique linéaire « soft ». STA a la propriété de réduction du sujet et est correct et complète pour les calculs en temps polynomial. Par la suite on propose un déduction naturelle, STA_N. Ce système est simple mais il a le désavantage que les variables dans le sujet peuvent être explicitement renommées. Pour résoudre ce problème, on propose le système STA_M, où les contextes sont des multi-ensembles, donc les règles pour renommer les variables peuvent être interdit. L’inférence de type pour STA_M ne semble pas décidable. On propose un algorithme qui pour chaque lambda-terme rend l’ensemble de contraintes que doivent être satisfait pour que le terme soit type. Pi est correct et complet. Ensuite on étend le lambda-calcul par des constantes booléennes et on propose le système STA_B. La particularité de STA_B est que la règle du conditionnel utilise les contextes de façon additive. Chaque programme de STA_B peut être exécuté, par une machine abstraite, en espace polynomial. De plus le système est aussi complet pour PSPACE. Dans la deuxième partie, on propose une restriction de PCF, nommée SlPCF. Ce langage est équipé avec une sémantique opérationnelle qui mélange l’appelle par nom et l’appelle par valeur et peut être interprèté en mode standard dans les espaces cohérents linéaires. SlPCF est complet pour les fonctions récursives, mais il n’est pas complet et donc il n’est pas fully abstract pour les espaces cohérents linéaires<br>In the first part, we propose, inspired by Soft Linear Logic, a type assignment system for lambda-calculus in sequent calculus style, named Soft Type Assignment (STA). STA enjoys the subject reduction property. and is correct and complete for polynomial time computations. Then, we propose a natural deduction named STA_N. While simple, STA_N has the disadvantage of allowing the explicit renaming of variables in the subject. To overcome to this problem, we propose another natural deduction system, named STA_M, where contexts are multisets, hence rules renaming variables can be avoided. The type inference for STA_M seems in general undecidable. We propose an algorithm Pi returning, for every lambda-term, a set of constraints that need to be satisfied in order to type the term. Pi is correct and complete. We extend the lambda-calculus by basic boolean constants and we propose the system STA_B. The peculiarity of STA_B is that the conditional rule treats the contexts in an additive way. Every STA_B program can be executed, through an abstract machine, in polynomial space. Moreover, STA_B is also complete for PSPACE. In the second part we propose a restriction of PCF, named SlPCF. The language is naturally equipped with an operational semantics mixing call-by-name and call-by-value parameter passing and it can be interpreted in linear coherence space in a standard way. SlPCF is recursive complete, but it is not complete, and thus not fully abstract, with respect to linear coherence spaces
45
Hao, Jin-Kao. "Combiner la programmation en logique et la résolution des contraintes par évaluation partielle : Conslog." Besançon, 1991. http://www.theses.fr/1991BESA2012.
Full textAbstract:
Cette these est une contribution a la programmation en logique avec contraintes (clp). Dans un systeme clp, nous distinguons deux aspects: l'inference logique qui est domaine independant et la resolution des contraintes qui est domaine dependant. Dans les systemes clp existants, ces deux aspects sont etroitement lies (integration forte), ce qui pose des problemes d'implantation, d'extensibilite et de performance. Dans cette these, apres une analyse de ces problemes, nous etudions une approche visant a realiser une integration faible de l'inference logique et de la resolution des contraintes. Nous proposons dans ce cadre une architecture modulaire pour la construction de systemes clp, en faisant abstraction au niveau langage, des domaines de calcul. La modularite assure qu'un tel systeme est relativement facile a construire et extensible. L'architecture facilite la realisation d'implantations efficaces, en evitant des traitements repetitifs mais aussi en permettant l'utilisation de techniques de resolution de contraintes existantes. Le prototype conslog est presente pour valider l'approche proposee. Conslog est un systeme clp (extensible) dans les domaines finis entiers positifs. Il comporte deux composants independants: un evaluateur partiel qui effectue les inferences logiques et collecte les contraintes, et un solveur qui resout les contraintes collectees. Ce prototype operationnel, implante en prolog nous a permis d'experimenter differentes techniques de resolution de contraintes sur de nombreux exemples. Nos travaux apportent une vue nouvelle sur la construction des systemes clp
46
Mounir, Alaoui Amine. "Raisonnement temporel pour la planification et la reconnaissance de situations." Toulouse 3, 1990. http://www.theses.fr/1990TOU30154.
Full textAbstract:
Le travail presente dans ce memoire propose une contribution au raisonnement sur le temps et sa prise en compte en intelligence artificielle pour la description d'actions et de situations dans des taches de planification et de surveillance. Notre travail a porte tout d'abord sur l'etude et la realisation d'un systeme de gestion de relations temporelles symboliques efficace appele ixtet et qui travaille sur des instants comme representation de base du temps. L'algorithme proposee est complete, de faible complexite, et non monotone. Ce gestionnaire de relations temporel a ete pris comme base d'un systeme de raisonnement temporal complet permettant l'utilisation d'assertions (t, p) ou p est une proposition et t, sa qualification temporelle. Ixtet a ensuite ete utilise dans deux applications. La premiere: un systeme de planification presentant un formalisme qui permet deux niveaux de granularite (actions et taches) pour la description des operateurs. Il utilise un ensemble d'axiomes du domaine pour la deduction des effets induits indirectement par les actions et taches. Il gere une description des buts et des evenements dans une structure temporelle plus complexe que la simple conjonction. Un ensemble de regles de comportement peuvent etre mises en uvre pour diriger la reactivite et la dynamique du systeme. Un systeme de pretraitement des actions et taches permet l'alleger le travail du planificateur proprement dit. Les algorithmes de planification correspondants ont ete developpes et illustres sur des exemples. La seconde: un systeme de reconnaissance de situations complexes en milieu evolutif presentant un formalisme qui permet de decrire une situation comme un ensemble de faits ou evenements temporellement contraints. Les situations ainsi decrites sont pretraitees hors-ligne de facon a etre reconnues le plus efficacement par la suite par le systeme de reconnaissance de situations qui est amene a travail
47
LEGROS, EMMANUEL. "Tests de satisfiabilite dans un langage de programmation en logique avec contraintes ensemblistes." Besançon, 1993. http://www.theses.fr/1993BESA2024.
Full textAbstract:
Ce travail porte sur l'integration des contraintes symboliques sur des ensembles hereditairement finis dans les langages de programmation en logique, conformement au modele clp (constraint logic programming). Nous definissons dans cette these la structure d'un langage de programmation en logique avec contraintes sur des ensembles hereditairement finis (clps), disposant des operateurs d'egalite, d'appartenance, de non-appartenance, d'inclusion et enfin, d'union et d'intersection. Nous montrons que le modele standard de la programmation en logique (unification dans l'univers de herbrand) est inadapte en raison du caractere np-complet de l'unification ensembliste. Nous proposons au travers de clps une approche differente fondee non plus sur l'unification, mais sur le controle de consistance des contraintes. Le prototype clps a entierement ete developpe en prolog. Il implante d'une part des algorithmes de consistance partielle specifique aux contraintes ensemblistes, d'autre part des algorithmes d'enumeration des valeurs capables de resoudre les contraintes ensemblistes. Dans ce contexte, l'unification ensembliste est vue comme une contrainte d'egalite, qui a la maniere des autres contraintes ensemblistes, est retardee tant qu'il n'est pas possible de la resoudre de maniere deterministe. Nous utilisons le langage clps pour resoudre un probleme industriel de genie logiciel (banc de validation)
48
Gervet, Carmen. "Intervalles ensemblistes en programmation logique par contraintes : definition formelle et concrete d'un langage." Besançon, 1995. http://www.theses.fr/1995BESA2040.
Full textAbstract:
Les techniques de satisfaction de contraintes ont ete recemment introduites en programmation logique en vue d'etendre le domaine d'application des langages de programmation en logique. Les langages existants, bases sur ces techniques, considerent des contraintes arithmetiques appliquees a des variables prenant leur valeur dans des domaines d'entiers. Cela rend difficile une modelisation concise et naturelle ainsi qu'une resolution efficace de certains problemes combinatoires np-complets, de nature ensembliste. Nous proposons une solution qui consiste a etendre la notion de domaine d'entiers a celle de domaine ensembliste (ensemble d'ensembles). Nous specifions un domaine ensembliste par un intervalle dont les bornes inferieure et superieure sont des ensembles connus, ordonnes par l'inclusion ensembliste. Nous definissons la structure formelle et concrete d'un nouveau langage de programmation en logique par contraintes sur domaines ensemblistes, appele conjunto. Conjunto comprend les symboles d'operations ensemblistes usuels (,, /) interpretes sous une forme relationnelle (s s#1 = s#2,) et la relation d'inclusion (). De plus il pourvoit un ensemble des contraintes appelees contraintes graduees (ex. Fonction de cardinalite) qui associent a un ensemble un terme arithmetique. Cela nous permet de traiter les problemes d'optimisation en appliquant une fonction de cout aux termes mesurables, i. E. Arithmetiques, associes aux termes ensemblistes. La resolution des contraintes dans conjunto est basee sur des techniques de satisfaction de contraintes par reduction d'intervalles etendues au traitement des contraintes ensemblistes. Ainsi, la contribution principale de cette these concerne la definition de regles de transformation au sein d'un algorithme generique, qui inferent la consistance locale des contraintes du langage en reduisant les intervalles ensemblistes. Un ensemble d'applications de recherche operationnelle et de mathematiques combinatoires ont ete developpees avec conjunto, illustrant ainsi les forces du langage en terme de rapport expressivite/efficacite
49
Massat, Jean-Luc. "Algorithmes d'énumération et résolution de contraintes booléennes dans un langage de programmation logique." Aix-Marseille 2, 1993. http://www.theses.fr/1993AIX22004.
Full textAbstract:
L'objet de ce travail est d'ameliorer le traitement de l'algebre de boole dans les langages de programmation logique avec contraintes. Pour ce faire, nous proposons d'utiliser un algorithme de resolution de type enumeration implicite. Cet algorithme recherche les solutions d'un systeme en explorant un arbre binaire. A chaque nud de cet arbre, le systeme courant est simplifie de maniere a decouvrir les impasses plus rapidement. Cette simplification est basee sur la detection locale d'egalites simples (egalites entre variables ou variable et constante). Nous proposons egalement une version incrementale de cet algorithme ainsi que deux algorithmes plus specifiques pour detecter les variables qui ne peuvent prendre qu'une seule valeur et produire les solutions d'un systeme sur un sous-ensemble des variables. Malgre les tres nettes ameliorations apportees par ces algorithmes, le probleme general reste intraitable. Il est donc souhaitable d'offrir un moyen declaratif pour controler la complexite des algorithmes de resolution. Dans ce cadre, nous introduisons une nouvelle relation que nous appelons pseudo-egalite. Le but de cette relation est de creer des liaisons faibles pour deconnecter des sous-systemes independants et ainsi eviter l'explosion combinatoire des algorithmes de resolution. Cette deconnexion n'est pas totale et des informations pertinentes peuvent passer d'un sous-systeme a un autre. Pour donner une semantique declarative a cette relation, nous presentons une nouvelle structure dont le domaine est compose de suites infinies construites sur 0,1. Nous montrons que les algorithmes issus de l'algebre de boole sont utilisables pour resoudre des contraintes dans cette structure et nous donnons une forme normale qui garantit la coherence
50
Diaz, Daniel. "Etude de la compilation des langages logiques de programmation par contraintes sur les domaines finis : le système clp (FD)." Phd thesis, Université d'Orléans, 1995. http://tel.archives-ouvertes.fr/tel-00981853.
Full textAbstract:
Ce travail porte sur la compilation des langages de programmation logique par contraintes sur les domaines finis (DF). Plutôt que d'adopter l'approche usuelle considérant le résolveur comme une boîte noire nous avons choisi l'approche boîte de verre de P. Van Hentenryck. Dans celle-ci, le résolveur gère une seule contrainte primitive. Toutes les contraintes complexes (équations, contraintes symboliques...) sont traduites en des appels de contraintes primitives. Le résolveur est ainsi simple et homogène. De plus, l'utilisateur peut définir ses propres contraintes en termes de cette primitive. Cette primitive nous permet de définir une machine abstraite pour la compilation des contraintes DF. En outre, le traitement d'une seule primitive permet de définir des optimisations globales dont bénéficient toutes les contraintes de haut niveau. Toutes ces idées sont détaillées et aboutissent à la définition du langage clp (FD). L'étude des performances de clp (FD) montre que cette approche est très efficace, meilleure en tous cas que les résolveurs boîtes noires. Nous étudions également les aptitudes de clp (FD) à résoudre des contraintes booléennes car elles sont un cas particulier des DF. Là encore clp (FD) se compare très bien avec des résolveurs spécialisés. Nous nous intéressons enfin à la détection de la satisfaction des contraintes pour permettre à l'utilisateur de spécifier des calculs dirigés par les données (plutôt que par les instructions). Ce travail débouche donc tout naturellement sur l'implantation des langages concurrents.