Tesi: "Démonstration automatisée de théorèmes"

1

Amaniss, Ali. "Méthodes de schématisation pour la démonstration automatique". Nancy 1, 1996. http://www.theses.fr/1996NAN10092.

Testo completo

Abstract (sommario):

Ce travail se situe dans le cadre de la déduction automatique. Il traite d'une méthode, appelée la schématisation, utilisée pour remédier à des problèmes d'expressivité, d'efficacité et de divergence. La schématisation est un moyen de représentation finie d'ensembles infinis d'objets. Ceux-ci peuvent se retrouver dans différents domaines de l'informatique. Le but de notre travail est l'étude de cette méthode d'un point de vue théorique et pratique. D’un point de vue théorique, nous avons situé les classes de schématisation existantes dans la hiérarchie des langages d'arbres après les avoir comparé entre elles. Chose qui nous a permis de proposer des classes plus expressives que toutes les classes proposées jusqu'ici et qui sont intéressantes pour la déduction automatique. D’un point de vue pratique, nous avons proposé plusieurs algorithmes de manipulation de schématisations. Nous avons surtout introduit la notion de problème d'inclusion pour lequel nous avons donné un algorithme que nous avons applique à la généralisation inductive d'ensembles infinis de termes. Cet algorithme peut trouver d'autres applications dans le génie logiciel, la réécriture et le calcul des processus. Nous avons ensuite améliore l'algorithme classique de généralisation inductive dans ses cas d'échec en utilisant les I-termes puis les B-termes. Les algorithmes proposés peuvent être vus comme des procédures de construction automatique, respectivement, des I-termes et des B-termes.

Gli stili APA, Harvard, Vancouver, ISO e altri

2

Mzali, Jalel. "Méthodes de filtrage équationnel et de preuve automatique de théorèmes". Nancy 1, 1986. http://www.theses.fr/1986NAN10387.

Testo completo

Abstract (sommario):

Implantation de différentes méthodes de démonstration automatique basées sur un algorithme de completion rapide appelé SKB et un algorithme de complétion qui privilégie la règle de simplification par rapport à celle de superposition, nous étudions cet algorithme et son implantation. Étude du filtrage pour la simplification et la réécriture des termes

Gli stili APA, Harvard, Vancouver, ISO e altri

3

Herzig, Andreas. "Raisonnement automatique en logique modale et algorithmes d'unification". Toulouse 3, 1989. http://www.theses.fr/1989TOU30115.

Testo completo

Abstract (sommario):

Il est montre que pour des logiques modales propositionnelles et quantifiees, des formes normales simples peuvent etre obtenues par des methodes de type skolemisation. Par consequent, des procedures automatiques de demonstration comme le principe de resolution, peuvent etre definies. Pour le premier ordre, une correspondance est etablie entre chaque logique modale et une theorie equationnelle particuliere. L'extension de l'algorithme d'unification classique permet alors la mecanisation de la demonstration dans cette logique

Gli stili APA, Harvard, Vancouver, ISO e altri

4

Noyer, Yves. "Trois études sur l'implantation des matrices en FoCaL, les preuves quantitatives et la réutilisation des preuves". Paris 6, 2010. http://www.theses.fr/2010PA066495.

Testo completo

Abstract (sommario):

Cette thèse part de la volonté d'implanter une bibliothèque de matrices dans l'environnement de développement sûr FoCaLize. Nous donnons une spécification dans laquelle toutes les matrices sur un même anneau commutatif unitaire sont vues comme des éléments d'une algèbre unitaire unique. Dans un tel contexte, les opérateurs d'addition et de multiplication sont des fonctions totales. Cela permet de les coder par des méthodes récursives dans un type de données ne tenant pas compte de la dimension des matrices. Nous recherchons ensuite des spécifications dans la bibliothèque FoCaLize vue comme une base de données de formules du premier ordre. La recherche d'une spécification aboutit s'il existe une formule de la bibliothèque dont l'information cherchée soit une conséquence dans le fragment de la logique du premier ordre des preuves ``quantitatives''. Celles-ci n'utilisent que les règles de quantification du calcul des séquents et se terminent par la règle axiome. Nous établissons un critère nécessaire et suffisant pour la réussite de notre recherche, retrouvant ainsi un résultat connu que nous affinons cependant. Nous donnons deux formalisations équivalentes de notre critère. Nous caractérisons l'admissibilité de la règle de coupure dans notre fragment par une méthode que nous pensons originale. Nous mettons en évidence une condition pour qu'une modification des symboles fonctionnels et relationnels dans un séquent du premier ordre permette d'obtenir un nouveau séquent possédant une preuve quantitative. Nous utilisons ce résultat pour proposer une méthode de réutilisation de preuve par analogie. Nous décrivons comment utiliser ces résultats dans le cadre de FoCaLiZe.

Gli stili APA, Harvard, Vancouver, ISO e altri

5

Larchey-Wendling, Dominique. "Preuves, réfutations et contre-modèles dans des logiques intuitionnistes". Nancy 1, 2000. http://www.theses.fr/2000NAN10158.

Testo completo

Abstract (sommario):

Les logiques sont de puissants outils qui permettent la spécification de systèmes informatiques et la preuve de l'adéquation de leurs implantations avec ces spécifications. Dans le cadre des logiques sous-structurelles, nous mettons en place des outils de démonstration automatique et de construction de contre-modèles. Ces logiques intègrent la notion de ressource ; au niveau de la recherche de preuve, la gestion des ressources permet la mise en place de procédures plus efficaces ; au niveau de l'interprétation sémantique, la notion de ressource permet de construire des modèles fidèles et complets. Nous établissons un lien entre la notion syntaxique de réfutation et la notion sémantique de contre-modèle. Nous en déduisons des méthodes de démonstration de la propriété des modèles finis ainsi que des algorithmes de construction de contre-modèles. En logique intuitionniste propositionnelle, la gestion fine de ressources permet d'en déduire une implantation efficace de la recherche de preuves. En logique intuitionniste linéaire, les modèles à base de ressources permettent une preuve élégante de la propriété des modèles finis. Nous établissons un lien entre la sémantique des ressources et la sémantique à base de réseaux de Petri, ce qui permet de raffiner les résultats de complétude partiels connus jusqu'alors
Logics can be used as powerful tools for specifying computer systems and proving the soundness of their implementations with respect to these specifications. In the field of substructural logics, we develop tools and methods for automated deduction and counter-model generation. These logics involve the notion of resource : at the level of proof-search, the management of resources enables more efficient procedures : at the semantic level, resource models provide sound and complete interpretations. We develop a link between the syntactic notion of refutation and the semantic notion of counter-model. We deduce methods for proving the finite model property and algorithms for implementation of a proof-search procedure, based on a fine management of resources. In intuitionistic linear logic, resource based models constitute the core of an elegant proof of the finite model property. Furthermore, we establish a link between resource models and Petri net based models, from which we improve the proeceding partial completness results

Gli stili APA, Harvard, Vancouver, ISO e altri

6

Cubadda, Christophe, e Marie-Dominique Mousseigne. "Variantes de l'algorithmes de sl-résolution avec retenue d'informations : démonstration de l'équivalence entre sl-résolution et production et démonstration de la validité de la variante des impasses et de la variante de remontée d'impasses". Aix-Marseille 2, 1988. http://www.theses.fr/1988AIX22063.

Testo completo

Abstract (sommario):

En depit des nombreuses strategies ameliorant l'algorithme de sl resolution, beaucoup d'informations redondantes et inutiles etaient generees, notamment lors d'echec d'effacement de litteraux. Un algorithme, appele slri, est propose. Il tient compte de ces informations. Il est demontre que l'arbre de recherche de cet algorithme est inclus dans l'arbre de recherche de la sl resolution

Gli stili APA, Harvard, Vancouver, ISO e altri

7

Pichardie, David. "Interprétation abstraite en logique intuitionniste : extraction d'analyseurs Java certifiés". Rennes 1, 2005. http://www.theses.fr/2005REN1S183.

Testo completo

Abstract (sommario):

Nous nous intéressons dans cette thèse à la preuve formelle de correction des analyses statiques. Nous nous basons sur la théorie de l'interprétation abstraite qui présente une analyse statique comme une sémantique approchée d'un programme. Nous utilisons l'assistant de preuve Coq qui permet d'extraire le contenu calculatoire d'une preuve constructive. L'implémentation Caml certifiée d'une analyse peut ainsi être extraite de la preuve d'existence, pour tout programme, d'une approximation correcte de la sémantique concrète de ce programme. Nous présentons un cadre théorique fondé sur l'interprétation abstraite et permettant le développement formel d'une large gamme d'analyses statiques. Une bibliothèque Coq de construction modulaire de treillis est ensuite proposée. Des preuves complexes de terminaison de calcul itératif de point fixe peuvent ainsi Ítre construites par simple composition de foncteurs. Plusieurs cas d'études pour l'analyse de programme en bytecode Java sont présentés.

Gli stili APA, Harvard, Vancouver, ISO e altri

8

Puitg, François. "Preuves en modélisation géométrique par le calcul des constructions inductives". Université Louis Pasteur (Strasbourg) (1971-2008), 1999. http://www.theses.fr/1999STR13032.

Testo completo

Abstract (sommario):

Cette étude présente un nouveau développement de techniques formelles de spécification et de preuve en modélisation géométrique. Le modèle topologique des cartes combinatoires est axiomatisé dans le calcul des constructions inductives (CCI), une théorie des types bien adaptée à la mécanisation des mathématiques en logique d'ordre supérieur. Une hiérarchie de types abstraits spécifiant les cartes combinatoires est construite et validée par des preuves inductives de consistance et de complétude dans le système Coq, un assistant à la preuve implantant le CCI. Un prototype certifié est obtenu par l'extraction automatique d'algorithmes fonctionnels des preuves constructives de leur correction. Des difficultés classiques en spécification formelle et preuve de théorèmes - comme la cohabitation d'objets et de leur généralisation dans la même hiérarchie, la gestion élégante du sous-typage, la complétion de relations et d'objets partiels, la confrontation des approches constructive et observationnelle, et la symétrisation de relations - sont abordées, non seulement sur le plan des spécifications formelles et de la preuve, mais aussi du point de vue de l'extraction. Grâce notamment à la nouvelle notion de quasi-face, des questions délicates de modélisation géométrique - comme la notion de face, l'énoncé d'un critère de planarité, la preuve de la formule d'Euler et d'un théorème de Jordan topologique - sont ainsi résolues d'une façon originale et incontestable, offrant une grande pénétration des fondements topologiques de la modélisation géométrique et une profonde compréhension du modèle. Une méthodologie de spécification et de preuve applicable à d'autres domaines est enfin proposée.

Gli stili APA, Harvard, Vancouver, ISO e altri

9

Cruanes, Simon. "Extending superposition with integer arithmetic structural induction and beyond". Palaiseau, Ecole polytechnique, 2015. https://tel.archives-ouvertes.fr/tel-01223502.

Testo completo

Abstract (sommario):

Le concept central de théorème désigne une assertion justifiée par un argument irréfutable agencé selon des règles formelles, qu'on appelle une preuve. Prouver des théorèmes est utile à la fois en Informatique et en Mathématiques. Cependant, beaucoup de théorèmes utiles, tels que ceux engendrés par la vérification formelle qu'un programme respecte une spécification, sont trop pénibles et inintéressants pour mériter l'attention d'experts humains; plusieurs décennies de recherches ont donc été consacrées au domaine de la démonstration automatique. La Superposition est une technique efficace permettant de prouver les théorèmes exprimés en logique du premier ordre avec égalité (en bref, la capacité de remplacer mutuellement deux objets égaux dans n'importe quelle expression). Pourtant, la Superposition montre ses limites dans beaucoup de cas où des théories spécifiques ou du raisonnement par récurrence sont nécessaires. Dans cette thèse, nous développons de nouvelles extensions à la Superposition; nous soutenons que cette dernière se prête bien à l'ajout de règles d'inférence et de mécanismes de raisonnement supplémentaires. Tout d'abord, nous développons un système d'inférence qui donne à la Superposition les moyens de raisonner dans l'arithmétique linéaire entière, une théorie activement utilisée et étudiée dans d'autres domaines de la preuve automatique tels que SMT (Satisfiabilité Modulo Théories). L'arithmétique peut également permettre des encodages vers la logique du premier ordre plus efficaces pour les structures discrètes totalement ordonnées, par exemple, la logique temporelle. Nous définissons ensuite un mécanisme permettant aux prouveurs fondés sur la Superposition de raisonner par récurrence sur des types algébriques (naturels, listes, arbres binaires, etc. ) Le raisonnement par récurrence est très courant en Mathématiques et en Informatique, mais son intégration dans les systèmes de preuve dédiés à la logique du premier ordre a été peu étudiée. Enfin, nous présentons un système de détections de théories axiomatiques capable de déceler la présence de structures algébriques connues dans un ensemble de formules. Ce système rappelle la manière dont un mathématicien qui étudie un nouvel objet peut découvrir que ce dernier relève d'une structure connue comme les groupes — ce qui lui permet de mobiliser ses connaissances sur cette théorie. Cette thèse comprend également une part importante de travail d'implémentation : toutes les contributions listées ci-dessus ont été incorporées dans une bibliothèque et un prouveur automatique, Zipperposition; tous deux sont écrits en OCaml et publiés sous licence libre
The central concept of theorem designates a claim backed by an irrefutable argument that follows formal rules, called a proof. Proving theorems is very useful in both Computer Science and Mathematics. However, many theorems are too boring and tedious for human experts (for instance, theorems generated to ensure that software abides by some specification); hence the decades-long effort in automated theorem proving, the field dedicated to writing programs that find proofs. Superposition is a very competitive technique for proving theorems in the language of first-order logic with equality over uninterpreted functions (in a nutshell, being able to replace equals by equals in any expression). Even then, Superposition falls short for many problems that require theory-specific reasoning or inductive proofs. In this thesis, we aim at developing new extensions to Superposition. Our claim is that Superposition lends itself very well to being grafted additional inference rules and reasoning mechanisms. First, we develop a Superposition-based calculus for integer linear arithmetic. Linear Integer Arithmetic is a widely studied and used theory in other areas of automated deduction, in particular SMT (Satisfiability Modulo Theory). This theory might also prove useful for problems that have a discrete, totally ordered structure, such as temporal logic, and that might be encoded efficiently into first-order logic with arithmetic. Then, we define an extension of Superposition that is able to reason by structural induction (natural numbers, lists, binary trees, etc. ) Inductive reasoning is pervasive in Mathematics and Computer Science but its integration into general purpose first-order provers has not been studied much. Last, we present a theory detection system that, given a signature-agnostic description of algebraic theories, detects their presence in sets of formulas. This system is akin to the way a mathematician who studies a new object discovers that this object belong to some known structure, such as groups, allowing her to leverage the large body of knowledge on this specific theory. A large implementation effort was also carried out in this thesis; all the contributions presented above have been implemented in a library and a theorem prover, Zipperposition, both written in OCaml and released under a free software license

Gli stili APA, Harvard, Vancouver, ISO e altri

10

Peltier, Nicolas. "Nouvelles techniques pour la construction de modèles finis et infinis en déduction automatique". Grenoble INPG, 1997. http://tel.archives-ouvertes.fr/tel-00004960.

Testo completo

Abstract (sommario):

Nous étudions des méthodes de recherche simultanée de refutation et de modèle. Nous proposons une méthode pour la construction de modèles finis réduisant de façon importante l'espace de recherche des approches existantes. Nous nous intéressons ensuite à la recherche de modèles infinis. Nous étendons les méthodes RAMC (Refutation And Model Construction) et RAMCET (Refutation And Model Construction with Equational Tableaux) définie par R. Caferra et N. Zabel en introduisant de nouvelles règles et stratégies. Ces extensions augmentent strictement les capacités de la méthode, à la fois pour la recherche de preuve et de contre-exemple. Nous montrons que les méthodes proposées sont des procédures de décision uniforme pour une large clase de formules logiques. Ensuite, nous proposons et étudions de nouveaux formalismes pour représenter les modèles: les termes avec exposants entiers et les automates d'arbres. Nous prouvons la décidabilité de la théorie du premier ordre sur les termes avec exposants. Nous proposons également une nouvelle approche pour la découverte et l'utilisation de l'analogie en recherche simultanée de preuve et de contre-exemple et nous montrons comment utiliser la méthode RAMC en Programmation Logique (pour étendre les capacités des interpréteurs, détecter, voire corriger des erreurs dans les programmes etc. ). Enfin, nous décrivons le système RAMC-ATINF implémentant certaines des idées proposées et nous donnons quelques résultats expérimentaux
In this thesis, we present several new techniques for model building in Automated Deduction. In the first part, we propose a general method for building finite models that favourably compares with the most powerful existing finite model builders. In the second part, we investigate methods for simultaneous search for refutations and (infinite, Herbrand) models. We improve the methods RAMC (Refutation And Model Construction) and RAMCET (Refutation And Model Construction with Equational Tableaux) defined by R. Caferra and N. Zabel by defining new rules and strategies. These extensions strictly increase the capabilities of the methods both for model building and unsatisfiability detection. We show that some of the proposed methods are uniform decision procedures for a wide range of decidable classes. We show the limits of the formalism of equational constraints, previously used for representing Herbrand models, and we propose to extend it by including terms with integer exponents (I-terms) and tree automata. As a new result, we prove the decidability of the first-order theory of I-terms. Fourthly, we study some applications of our work: we present a new approach for discovering and using analogy in simultaneous search for refutations and models, and we show how to use the method RAMC in Logic Programming (for extending logic program interpreters, detecting and correcting errors in logic programs etc. ). Finally we describe the system RAMC-ATINF implementing our approach and we report some experiments showing the practical capabilities of our method

Gli stili APA, Harvard, Vancouver, ISO e altri

11

Clérin-Debart, Françoise. "Théories équationnelles et de contraintes pour la démonstration automatique en logique multi-modale". Caen, 1992. http://www.theses.fr/1992CAEN2001.

Testo completo

Abstract (sommario):

Nous étudions dans ce travail des méthodes de déduction automatique pour la logique multi-modale. Dans une première partie les logiques multi-modales considérées contiennent un nombre fini de paires d'opérateurs modaux. Dans la dernière partie les opérateurs modaux peuvent être indexés par des termes d'une logique à sortes ordonnées. Dans les deux cas les opérateurs modaux sont de type KD, KD4, KT, KT4 ou KF. Les formules de la logique multi-modale sont traduites dans une logique du premier ordre à sortes ordonnées. Dans le premier cas la logique utilisée est munie d'une théorie équationnelle. Dans le deuxième cas, nous utilisons en plus une théorie de contraintes. Pour la déduction automatique les méthodes utilisées sont adaptées de la E-résolution de Plotkin et de la résolution contrainte de Frisch. Les théories équationnelles utilisées possèdent un opérateur associatif mais les termes obtenus par traduction possèdent une structure très particulière (appelée ici propriété PR) et un procédé adapté de skolémisation permet de conserver cette structure. Une étude de l'unification associative pour les termes possédant cette propriété est faite pour l'algorithme de Plotkin et pour des algorithmes utilisant des règles de transition. Les algorithmes proposés terminent et calculent des ensembles complets d'unificateurs, qui sont, dans ce cas, finis.

Gli stili APA, Harvard, Vancouver, ISO e altri

12

Shminke, Boris. "Applications de l'IA à l'étude des structures algébriques finies et à la démonstration automatique de théorèmes". Electronic Thesis or Diss., Université Côte d'Azur, 2023. http://www.theses.fr/2023COAZ4058.

Testo completo

Abstract (sommario):

Cette thèse contribue à une recherche de modèles finis et à la démonstration automatisée de théorèmes, en se concentrant principalement, mais sans s'y limiter, sur les méthodes d'intelligence artificielle. Dans la première partie, nous résolvons une question de recherche ouverte à partir de l'algèbre abstraite en utilisant une recherche automatisée de modèles finis massivement parallèles, en utilisant l'assistant de preuve Isabelle. À savoir, nous établissons l'indépendance de certaines lois de distributivité abstraites dans les binaires résiduels dans le cas général. En tant que sous-produit de cette découverte, nous apportons un client Python au serveur Isabelle. Le client a déjà trouvé son application dans les travaux d'autres chercheurs et de l'enseignement supérieur. Dans la deuxième partie, nous proposons une architecture de réseau neuronal génératif pour produire des modèles finis de structures algébriques appartenant à une variété donnée d'une manière inspirée des modèles de génération d'images tels que les GAN (réseaux antagonistes génératifs) et les autoencodeurs. Nous contribuons également à un paquet Python pour générer des semi-groupes finis de petite taille comme implémentation de référence de la méthode proposée. Dans la troisième partie, nous concevons une architecture générale de guidage des vérificateurs de saturation avec des algorithmes d'apprentissage par renforcement. Nous contribuons à une collection d'environnements compatibles OpenAI Gym pour diriger Vampire et iProver et démontrons sa viabilité sur des problèmes sélectionnés de la bibliothèque TPTP (Thousand of Problems for Theorem Provers). Nous contribuons également à une version conteneurisée d'un modèle ast2vec existant et montrons son applicabilité à l'incorporation de formules logiques écrites sous la forme clausal-normale. Nous soutenons que l'approche modulaire proposée peut accélérer considérablement l'expérimentation de différentes représentations de formules logiques et de schémas de génération de preuves synthétiques à l'avenir, résolvant ainsi le problème de la rareté des données, limitant notoirement les progrès dans l'application des techniques d'apprentissage automatique pour la démonstration automatisée de théorèmes
This thesis contributes to a finite model search and automated theorem proving, focusing primarily but not limited to artificial intelligence methods. In the first part, we solve an open research question from abstract algebra using an automated massively parallel finite model search, employing the Isabelle proof assistant. Namely, we establish the independence of some abstract distributivity laws in residuated binars in the general case. As a by-product of this finding, we contribute a Python client to the Isabelle server. The client has already found its application in the work of other researchers and higher education. In the second part, we propose a generative neural network architecture for producing finite models of algebraic structures belonging to a given variety in a way inspired by image generation models such as GANs (generative adversarial networks) and autoencoders. We also contribute a Python package for generating finite semigroups of small size as a reference implementation of the proposed method. In the third part, we design a general architecture of guiding saturation provers with reinforcement learning algorithms. We contribute an OpenAI Gym-compatible collection of environments for directing Vampire and iProver and demonstrate its viability on select problems from the Thousands of Problems for Theorem Provers (TPTP) library. We also contribute a containerised version of an existing ast2vec model and show its applicability to embedding logical formulae written in the clausal-normal form. We argue that the proposed modular approach can significantly speed up experimentation with different logic formulae representations and synthetic proof generation schemes in future, thus addressing the data scarcity problem, notoriously limiting the progress in applying the machine learning techniques for automated theorem proving

Gli stili APA, Harvard, Vancouver, ISO e altri

13

Benhammadi, Farid. "La gestion des préférences en logique des défauts". Angers, 1999. http://www.theses.fr/1999ANGE0008.

Testo completo

Abstract (sommario):

Ce travail porte sur la gestion des préférences explicites en logique des défauts et nous nous sommes essentiellement intéressés à la problématique de déduction automatique. Pour ce faire, nous avons défini une nouvelle approche pour caractériser les extensions prioritaires pour les théories de défauts ordonnés. De cette facon, nous avons obtenu deux résultats : un nouveau calcul d'extensions prioritaires qui nous a permis d'avoir une méthode de calcul d'extensions plus efficace, une approche du raisonnement crédule en logique des défauts ordonnée basé sur deux schémas de vérification différents. Le premier s'appuie sur un algorithme de transformation de preuves classiques en preuves prioritaires et le second sur la préservation de priorités et des ensembles de blocage de défauts. Nous montrons enfin comment la technologie Prolog peut être utilisée pour implanter le raisonnement crédule en logique des défauts avec priorités.

Gli stili APA, Harvard, Vancouver, ISO e altri

14

Lazrek, Azzeddine. "Étude et réalisation de méthodes de preuve par récurrence en logique équationnelle". Vandoeuvre-les-Nancy, INPL, 1988. http://www.theses.fr/1988NAN10380.

Testo completo

Abstract (sommario):

Développement d'un outil puissant pour la programmation logique et/ou fonctionnelle et pour la démonstration automatique. L’objectif principal est l'étude et la mise en œuvre d'une méthode de preuve de théorèmes inductifs dans l'algèbre initiale d'une variété équationnelle. La méthode étudiée est la synthèse de la méthode de preuve par consistance et de celle basée sur la réductibilité inductive. Le deuxième objectif est l'étude de la complétude relative, souhaitable dans la conception et la correction des spécifications algébriques structurées et requise par la méthode de preuve par consistance

Gli stili APA, Harvard, Vancouver, ISO e altri

15

Juban, Laurent. "Sur les problèmes de complexité en déduction automatique : base de Hilbert, modèles uniques et minimaux". Nancy 1, 1999. http://www.theses.fr/1999NAN10254.

Testo completo

Abstract (sommario):

Dans cette thèse, nous nous sommes intéressés à la complexité de certains problèmes dans le cadre de la déduction automatique. Nous étudions la complexité de comptage de la base de Hilbert d'un système d'équations diophantiennes linéaires homogène. La base de Hilbert d'un système d'équations diophantiennes linéaires homogène est l'ensemble de ses solutions entières minimales à coefficients positifs. Nous donnons une borne inférieure et une borne supérieure pour la complexité de ce problème en montrant que le comptage de la base de Hilbert est #P-difficile et appartient à la classe #NP. De plus, nous étudions la complexité de certaines variantes de ce problème quand le nombre d'occurrences de chaque variable est restreint dans le système. Nous étudions également le problème de la reconnaissance de la base de Hilbert. Nous étudions le problème de la base de Hilbert où les coefficients sont donnés en notation unaire. Nous prouvons que le problème de la minimalité d'une solution pour un système d'équations diophantiennes linéaires homogène est un problème coNP-complet au sens fort. De plus, nous montrons qu'étant donné un ensemble de vecteurs, le problème de savoir si cet ensemble représente la base de Hilbert d'un système donné en entrée est polynomialement équivalent au problème de savoir si cet ensemble représente la base de Hilbert d'un système quelconque. Nous nous sommes également intéressés au problème de l'unicité d'un modèle pour un formule propositionnelle. Nous donnons un théorème dichotomique pour ce problème en énumérant de façon exhaustive les instances polynomiales de celui-ci
In this thesis we are interested in the complexity of sorne problems in the framework of automated deduction. We study the computational complexity of counting the Hilbert basis of a homogeneous system of linear diophantine equations. The Hilbert basis of a homogeneous system of linear Diophantine equations over non-negative integers is the set of aIl non-zero vectors that are minimal solutions. We establish lower and upper bounds for the complexity of this problem, by showing that counting the Hilbert basis is #P-hard and belongs to the class #NP. Moreover, we investigate the complexity of variants obtained by restricting the number of occurrences of the variables in the system. We also study the problem of recognizing the Hilbert basis. We analyze the problem of the Hilbert basis where the coefficients are given in unary notation. We prove that deciding whether a given solution belongs to the Hilbert basis of a given system is a coNP-complete problem in the strong sense. Furthermore, we show that given a linear Diophantine system and a set of solutions, as king whether this set represents the Hilbert basis of the system is polynomialy equivalent to the problem of deciding whether a glven set of vectors constitutes the Hilbert basis of an unknown linear Diophantine system. We also study the unique satisfiability problem that consists of deciding if there exists a unique solution to a given propositional formula. We give a dichotomy theorem for this problem by partitioning the instances of the problem between the polynomial-time solvable and coNP-hard cases

Gli stili APA, Harvard, Vancouver, ISO e altri

16

Curien, Régis. "Outils pour la preuve". Nancy 1, 1995. http://docnum.univ-lorraine.fr/public/SCD_T_1995_0007_CURIEN.pdf.

Testo completo

Abstract (sommario):

Le but de cette thèse est de fournir des outils permettant à la déduction automatique de réutiliser les résultats déjà obtenus. En effet, la preuve par analogie consiste à construire de nouvelles preuves à partir de preuves existantes. Il faut dans un premier temps reconnaître que le problème à résoudre est semblable à un problème déjà résolu, puis, transformer la solution existante, pour obtenir une solution du nouveau problème. L'approche adoptée consiste à définir formellement des relations liant deux formules logiques du premier ordre - celle dont nous possédons une preuve est appelée référence - pour en déduire une méthode automatique de transformation de la preuve de référence en une preuve de la nouvelle formule. Le concept d'analogie est très puissant, mais aussi très intuitif. Ainsi, pour le formaliser, nous l'avons réduit à des concepts plus simples afin de les automatiser. Nous avons défini quatre relations liant les formules, que nous appelons similitudes. Ces similitudes considèrent les propriétés de la logique propositionnelle, les propriétés des quantificateurs, le renommage des fonctions et prédicats et les propriétés associatives-commutatives des connecteurs logiques. Un outil fondamental pour la reconnaissance de ces similitudes est un algorithme de filtrage du second ordre modulo AC. La complétude et la terminaison de cet algorithme montrent la décidabilité du problème de filtrage AC du second ordre. Les transformations de preuves correspondant à ces similitudes sont données pour les preuves par expansion introduites par Miller et Pfenning. Cette représentation possède des propriétés très intéressantes pour l'analogie. Pour dépasser le stade des similitudes, nous utilisons le calcul de différence, qui utilise les échecs du filtrage. Nous montrons que lorsque la différence entre les deux formules considérées est simple, nous pouvons espérer une méthode complète d'analogie. Enfin, nous montrons, dans le cas général, et à partir d'exemples, comment l'analogie peut être envisagée par l'étude de la différence.

Gli stili APA, Harvard, Vancouver, ISO e altri

17

Rusinowitch, Michaël. "Démonstration automatique par des techniques de réécritures". Nancy 1, 1987. http://www.theses.fr/1987NAN10358.

Testo completo

Abstract (sommario):

Introduction à la logique du premier ordre et aux systèmes de réécriture. Étude de quelques ordres de simplification. Arbres sémantiques transfinis. Stratégies de paramodulation. Complétude en présence de règles de réduction. Stratégies de superposition. Ensembles complets de règles d'inférence pour les axiomes de régularité

Gli stili APA, Harvard, Vancouver, ISO e altri

18

Smirnova, Elena. "Développement et réalisation d'algorithmes traitant des données floues dans des logiques plurivalentes". Paris 12, 2002. http://www.theses.fr/2002PA120031.

Testo completo

Abstract (sommario):

Le but de cette thèse est de développer et d'implémenter un système de recherche automatique de la déduction des séquents dans les logiques plurivalentes. Le premier chapitre décrit la logique plurivalente de Post, étendue par l'opération de comparaison logique, dite aussi la logique des comparaisons. La structure des niveaux logiques, la syntaxe et la sémantique sont décrits dans cette partie ainsi que le calcul et la description du système des axiomes. Le deuxième chapitre est destiné à présenter une méthode de reconnaissance des axiomes dans la logique des comparaisons et un algorithme, réalisant cette méthode. Il est prouvé que cet algorithme a une complexité cubique. Dans le chapitre 3 il y a une présentation de l'algorithme principal de recherche d'inférences dans la logique des comparaisons. On décrit la particularité de la déduction dans ce type de logique par rapport à la logique classique. On propose aussi des méthodes d'optimisation du processus de recherche de la déduction des séquents pour obtenir des dérivations les plus courtes
This thesis presents an automated sequent derivation system for multi-valued logics. As an example of multi-valued logic, an extension of Post's Logic with linear order is considered and described in chapter 1. The basic ideas and main algorithms used in this system are presented in this chapter. One of the important parts of the derivation algorithm is a method designed to recognize axioms ofa given logic. This method, described in a chapter 2, uses a symbolic computation method for establishing the solvability of systems of linear inequalities of a special type. It is proved that this algorithm has cubic complexity. The main algorithm for deduction search is described in the third chapter. It is shown that derivation in multilevel logics with linear order has some particularities in comparison with derivation in classic logic, concerning preferences of infcrence rule application. Some methods for inference rule searching and for optimization ofdeduction process are also proposed in this work

Gli stili APA, Harvard, Vancouver, ISO e altri

19

Notin, Jean-Marc. "Recherche et construction de preuves en logique non-commutative". Nancy 1, 2004. http://www.theses.fr/2004NAN10183.

Testo completo

Abstract (sommario):

La logique NL étend la logique linéaire en y ajoutant des connecteurs non-commutatifs. Sa particularité vient des interactions entre les connecteurs commutatifs et non-commutatifs. Une première étude nous a conduit à analyser ces interactions dans le cadre des réseaux de preuve. Leur prise en compte lors de la recherche de preuves par composition (construction) nécessite l'introduction de structures spécifiques (labels, graphes de dépendances). Nous proposons ainsi plusieurs algorithmes de construction de réseaux de preuve pour le fragment multiplicatif de NL. Une autre approche étudiée est celle de la recherche de preuves par décomposition, mise en oeuvre en particulier dans le cadre des méthodes des connexions. En utilisant des labels associés aux sous-formules, et des contraintes exprimées sur ces labels, nous proposons une caractérisation par les connexions pour MNL. La méthode des connexions associée peut être vue comme un nouvel algorithme de construction de réseaux de preuve
Partially commutative logics allow to express properties mixing concurency and sequentiality. Thus, the logic NL extends linear logic with non-commutative connectives. The characteristic of NL comes from the interactions between commutative and non-commutative connectives. A first study led us to analyze these interactions within the framework of proof nets. Taking such interactions into account during top-down proof search (proof nets construction) requires the introduction of specific structures (labels, dependency sets). Thus, we propose several algorithms for building proof nets in the multiplicative fragment of NL (MNL). Another studied approach is bottom-up proof search, in particular within the framework of connection methods. By using labels associated with the subformulas, and constraints expressed on these labels, we propose a connection characterization for MNL. The associated connection method can be seen like a new algorithm for proof nets construction in MNL

Gli stili APA, Harvard, Vancouver, ISO e altri

20

Deplagne, Eric. "Système de preuve modulo récurrence". Nancy 1, 2002. http://docnum.univ-lorraine.fr/public/SCD_T_2002_0240_DEPLAGNE.pdf.

Testo completo

Abstract (sommario):

Les méthodes et systèmes de preuve par récurrence sont très diverses. Les méthodes les plus générales sont difficiles à automatiser. Les systèmes automatiques parfois difficiles à justifier. Cette thèse établit au niveau des preuves un lien entre récurrence noethérienne et récurrence par réécriture, ce qui permettra la coopération de systèmes dans un mode sceptique où la preuve est vérifiée grâce à l'isomorphisme de Curry-Howard. Le formalisme de la déduction modulo est étendu au traitement de congruences conditionnelles dont l'évaluation tient compte du contexte. De plus, l'ordre de récurrence qui ne peut pas être compatible avec la congruence, est rendu protecteur, c'est-à-dire qu'il bloque l'application de la congruence. La preuve par récurrence par réécriture est vue comme le résultat de l'internalisation en déduction modulo des hypothèses de récurrence, ce qui permet d'expliquer certains comportements de la méthode de récurrence par réécriture
Methods and systems for proof by induction are very different. The most general methods are difficult to automatize. Automated systems are sometimes difficult to justify. This thesis establishes at proof level a link between noetherian induction and induction bt rewriting, which will enable systems to cooperate in a skeptical mode in which the proof is verified thanks to the Curry-Howard isomorphism. The formalism of deduction modulo is extended to conditional congruences which are evaluated with respect to a context. Moreover,the induction ordering, which cannot be compatible with the congruence, is made protective, which means that it blocks the application of the congruence. Proof by induction by rewriting is seen as the result of the internalization of induction hypotheses in deduction modulo, which enables to explain some of the behavior of the induction by rewriting method

Gli stili APA, Harvard, Vancouver, ISO e altri

21

Chetali, Boutheïna. "Vérification formelle des systèmes parallèles décrits en Unity à l'aide d'un outil de démonstration automatique". Nancy 1, 1996. http://docnum.univ-lorraine.fr/public/SCD_T_1996_0037_CHETALI.pdf.

Testo completo

Abstract (sommario):

Cette thèse est consacrée à l'utilisation des méthodes formelles de spécification et de vérification dans le cadre des techniques déductives basées sur la preuve de theorèmes. En particulier, nous nous intéressons à la spécification et à la vérification mécanique de programmes parallèles décrits en Unity à l'aide du démonstrateur du Larch, LP. Nous décrivons la formalisation et la mécanisation de la logique et de la méthodologie d'Unity à l'aide d'un outil de démonstration automatique du premier ordre et à large spectre tel que LP et à leur mise en oeuvre dans des exemples utiles et conséquents. Nous formalisons dans un premier temps la syntaxe et la sémantique d'Unity dans l'environnement de LP en choisissant comme outil formel la plus faible pré-condition introduite par Dijkstra. Cette modélisation comprend la représentation syntaxique concrète des objets prédicats, de la notation de programmation et des prédicats temporels de Unity dans une logique du premier ordre. Nous décrivons la construction et la validation d'une base de faits basée sur l'approche des spécifications LSL. Nous proposons une méthodologie de preuve incrémentale basée sur l'utilisation d'un démonstrateur pour la vérification mécanisée dans le but à la fois d'aider à la mise au point des preuves et à la réutilisation des preuves. Nous illustrons l'approche proposée à l'aide de trois études de cas. La vérification formelle mécanique d'un protocole de communication à travers des canaux défectueux met en évidence la méthodologie utilisée pour montrer des propriétés de sûreté et de vivacité et comment un démonstrateur peut être effectivement utilisé pour détecter des failles dans la spécification. La vérification du problème des lecteurs rédacteurs illustre un aspect important dans l'utilisation des démonstrateurs, à savoir la réutilisation et la mécanisation des preuves. Enfin, la vérification d'un protocole de contrôle d'un ascenseur permet de comparer notre approche à celle utilisée avec le démonstrateur d'ordre supérieur HOL.

Gli stili APA, Harvard, Vancouver, ISO e altri

22

Méry, Daniel. "Preuves et sémantiques dans des logiques de ressources". Nancy 1, 2004. http://www.theses.fr/2004NAN10160.

Testo completo

Abstract (sommario):

Les logiques de ressources sont de puissants outils de spécification de propriétés. Dans le cadre d'une théorie mathématique des ressources, nous élaborons des méthodes de preuve qui capturent l'interaction entre les ressources par l'intermédiaire de labels et de contraintes. Nous présentons la logique BI qui, avec son interprétation en termes de partage de ressources, est un noyau commun à beaucoup de logiques de ressources. Nous développons des méthodes de preuve par tableaux et par connexions, avec construction de contre-modèles, pour le fragment cohérent de BI. Nous étendons nos méthodes de preuve à la totalité du fragment propositionnel de BI, dont nous montrons la décidabilité ainsi que la propriété des modèles finis. Nous proposons de nouvelles sémantiques complètes pour BI et spécialisons nos méthodes à la logique intuitionniste et intuitionniste linéaire multiplicative. Nous étudions les variantes affines et booléennes de BI ainsi que la logique des pointeurs
Resource-aware logics are powerful tools for specifying properties. In the context of a mathematical theory of resources, we build proof-search methods which capture the dynamic interactions between resources by means of labels and constraints. We present the BI-logic which, due to its resource-sharing interpretation, appears as the logical kernel of a wide range of resource logics. We develop tableau-based and connection-based proof-search methods, with counter-model generation facilities, for the consistent fragment of BI. We extend our proof methods to the whole fragment of propositional BI, showing that it is decidable and has the finite model property. We propose new complete semantics for BI and specialize ou methods to intuitionistic logic and intuitionistic multiplicative linear logic. We study the affine and boolean variants of BI and their links with the pointer logic

Gli stili APA, Harvard, Vancouver, ISO e altri

23

Mengin, Jérôme. "Raisonnement par défaut : résolutions de conflits et priorités". Paris 11, 1994. http://www.theses.fr/1994PA112101.

Testo completo

Abstract (sommario):

L'un des thèmes actuels de recherche en intelligence artificielle concerne la formalisation de certains types de raisonnement, en vue d'une automatisation. Cette thèse s'intéresse au raisonnement dit par défaut, à partir de connaissances incomplètes. Après une revue de plusieurs travaux sur ce sujet, la thèse présente un formalisme permettant de tenir compte, de manière intuitive, de préférence parmi les connaissances à inférer par défaut. Ce formalisme est basé sur la notion de résolution de conflits. L'intérêt de ce formalisme réside dans sa souplesse, qui permet de l'appliquer dans plusieurs domaines. Il permet en particulier de capturer des concepts utilisés dans de nombreuses autres logiques formalisant le raisonnement par défaut, et de combiner ces concepts entre eux ainsi que de les utiliser en présence de préférence. Dans la dernière partie, la thèse présente un algorithme permettant d'automatiser la forme de raisonnement capturé par ce formalisme. Cet algorithme est une adaptation d'un algorithme de résolution de conflits utilisé dans le domaine du diagnostic. Enfin, la thèse présente un algorithme permettant de calculer les inconsistances en logique des défauts, ce qui permet alors d'implémenter un démonstrateur de théorèmes pour cette logique

Gli stili APA, Harvard, Vancouver, ISO e altri

24

Khan, Muhammad Uzair. "A study of first class futures : specification, formalisation, and mechanised proofs". Nice, 2011. http://www.theses.fr/2011NICE4003.

Testo completo

Abstract (sommario):

Futures enable an efficient and easy to use programming paradigm for distributed applications. A future is a placeholder for result of concurrent execution. Futures can be first class objects; first class futures may be safely transmitted between the communicating processes. Consequently, futures spread everywhere. When the result of a concurrent execution is available, it is communicated to all processes which received the future. In this thesis, we study the mechanisms for transmitting the results of first class futures; the future update strategies. We provide a detailed semi-formal specification of three main future update strategies adapted from ASP-calculus; we then use this specification for a real implementation. We study the efficiency of the three update strategies through experiments. Ensuring correctness of distributed protocols, like future update strategies is a challenging task. To show that our specification is correct, we formalise it together with a component model. Components abstract away the program structure and the details of the business logic ; this paradigm thus facilitates reasoning on the protocol. We formalise in Isabelle/HOL, a component model comprising notions of hierarchical components, asynchronous communications, and futures. We present the basic constructs and corresponding lemmas related to structure of components, and formal operational semantics of our components in presence of a future update strategy; proofs showing correctness of future updates are presented. Our work can be considered as a formalisation of ProActive/GCM, and shows the correctness of the middleware implementation
Les futurs fournissent une modèle de programmation efficace pour le développement des applications distribuées. Un futur est une objet temporaire qui représente le résultat d’une exécution concurrente. Les futurs peuvent être des objet de «première classe», et ainsi être transmis en toute sécurité entre les processus communicants. En conséquence, les futures se propagent partout dans le système. Lorsque le résultat d’une exécution simultanée est disponible, il est communiqué à tous les processus qui ont reçu le futur. Nous étudions les mécanismes de transmission des résultats des futurs; les "stratégies pour mise à jour des futurs". Nous fournissons une spécification semi-formelle détaillée, de trois principales stratégies. Nous utilisons ensuite cette spécification pour une véritable implémentation et nous étudions l’efficacité des trois stratégies. C’est une tâche difficile d’assurer la correction des protocoles distribués. Pour montrer que notre spécification est correcte, nous la formalisons avec un modèle de composants. Les composants abstraient la structure du programme ; ce paradigme facilite donc le raisonnement sur le protocole. Nous formalisons dans Isabelle/HOL un modèle de composants comprenant des notions de composants hiérarchiques, les communications asynchrones, et les futurs. Nous présentons les constructions de base et des lemmes liés à la structure des composants. Nous présentons une sémantique formelle des nos composants en présence d’une stratégie de mise à jour de futurs ; Les preuves montrant la correction de notre stratégie sont présentées. Notre travail peut être considéré comme une formalisation de ProActive / GCM

Gli stili APA, Harvard, Vancouver, ISO e altri

25

Coscoy, Yann. "Explication textuelle de preuves pour le calcul des constructions inductives". Nice, 2000. http://www.theses.fr/2000NICE5428.

Testo completo

Abstract (sommario):

Ce travail concerne la présentation des preuves formalisées dans le calcul des constructions inductives. Le calcul des constructions est un [lambda]-calcul typé introduit par Th. Coquand et G. Huet. Il permet un codage fonctionnel des preuves d'ordre supérieur par l'isomorphisme de Curry-Howard. Nous étudions dans ce manuscrit une variante de ce formalisme étendue par Ch. Paulin et B. Werner. Nous décrivons une fonction réversible traduisant les termes de preuve du formalisme en des textes mathématiques en français. Dans le premier sens, du [lambda]-terme vers la langue naturelle, cette traduction est une présentation de la preuve. Elle comporte une phase de sélection des informations avec organisation du discours puis une phase de verbalisation. Dans l'autre sens, du texte vers le [lambda]-terme, il s'agit d'une validation. Le texte est analysé syntaxiquement puis évalué comme un script de système de preuve. La réversibilité de la fonction de présentation permet de garantir formellement que les démonstrations produites en français sont des preuves formelles. Elles peuvent de fait être validées par un processus automatique

Gli stili APA, Harvard, Vancouver, ISO e altri

26

Das, Barman Kuntal. "Type theoretic semantics for programming languages". Nice, 2004. http://www.theses.fr/2004NICE4029.

Testo completo

Abstract (sommario):

La sémantique des langages de programmation donne la signification des constructions de programme. Les sémantiques opérationnelle et dénotationelle sont les deux principales approches pour la sémantique de langage de programmation. La sémantique opérationnelle est habituellement donnée par des relations inductives. La sémantique dénotationelle est donnée par des fonctions partielles. Mettre en application la sémantique dénotationelle à l’intérieur de la théorie des types est difficile car cette théorie ne supporte que les fonctions totales. Dans cette thèse nous développons une sémantique fonctionnelle pour un petit langage impératif à l’intérieur de la théorie des types et montrons son équivalence avec la sémantique opérationnelle. Nous exploitons ensuite cette sémantique fonctionnelle pour obtenir un outil plus direct de recherche de preuve, tout en développant une manière de décrire et manipuler des expressions inconnues dans le calcul symbolique des programmes pour le développement formel de preuve. Dans une troisième partie, nous adressons le problème de coder des programmes complexes à l’intérieur de la théorie des types et nous montrons comment éviter les limitations des conditions de garde telle qu’elles sont employées dans le calcul des constructions inductives
Semantics of programming languages gives the meaning of program constructs. Operational and denotational semantics are two main approaches for programming languages semantics. Operational semantics is usually given by inductive relations. Denotational semantics is given by partial functions. Implementing the denotational semantics inside type theory is difficult as the type theory expects total functions. In this dissertation we develop a functional semantics for a small imperative language inside type theory and show its equivalence with operational semantics. We then exploit this functional semantics to obtain a more direct proof search tool, while developing a way to describer and manipulate unknown expressions, in the symbolic computation of programs for formal proof development. In a third part, we address the problem of encoding complex programs inside type theory and we show how to circumvent the limitations of guardedness conditions as the are used in the Calculus of Inductive Constructions

Gli stili APA, Harvard, Vancouver, ISO e altri

27

Laporte, Vincent. "Vérification d’analyses statiques pour langages de bas niveau". Thesis, Rennes 1, 2015. http://www.theses.fr/2015REN1S078/document.

Testo completo

Abstract (sommario):

L'analyse statique des programmes permet d'étudier les comportements possibles des programmes sans les exécuter. Les analyseurs statiques sont employés par exemple pour garantir que l'exécution d'un programme ne peut pas produire d'erreurs. Ces outils d'analyse étant eux-mêmes des programmes, ils peuvent être incorrects. Pour accroître la confiance que l'on peut accorder aux résultats d'une telle analyse, nous étudions dans cette thèse comment on peut formellement établir la correction de l'implantation d'un tel analyseur statique. En particulier, nous construisons au moyen de l'assistant à la preuve Coq des interpréteurs abstraits et prouvons qu'ils sont corrects ; c'est-à-dire nous établissons formellement que le résultat de l'analyse d'un programme caractérise bien toutes les exécutions possibles de ce programme. Ces interpréteurs abstraits s'intègrent, dans la mesure du possible, au compilateur vérifié CompCert, ce qui permet de garantir que les propriétés de sûreté prouvées sur le code source d'un programme sont aussi valides pour la version compilée de ce programme. Nous nous concentrons sur l'analyse de programmes écrits dans des langages de bas niveau. C'est-à-dire des langages qui ne fournissent que peu d'abstractions (variables, fonctions, objets, types…) ou des abstractions que le programmeur a loisir de briser. Cela complexifie la tâche d'un analyseur qui ne peut pas s'appuyer sur ces abstractions pour être précis. Nous présentons notamment comment reconstruire automatiquement le graphe de flot de contrôle de programmes binaires auto-modifiants et comment prouver automatiquement qu'un programme écrit en C (où l'arithmétique de pointeurs est omniprésente) ne peut pas produire d'erreurs à l'exécution
Static analysis of programs enables to study the possible behaviours of programs without running them. Static analysers may be used to guarantee that the execution of a program cannot result in a run-time error. Such analysis tools are themselves programs: they may have bugs. So as to increase the confidence in the results of an analysis, we study in this thesis how the implementation of static analysers can be formally proved correct. In particular, we build abstract interpreters within the Coq proof assistant and prove them correct. Namely, we formally establish that analysis results characterize all possible executions of the analysed program. Such abstract interpreters are integrated to the formally verified CompCert compiler, when relevant ; this enables to guarantee that safety properties that are proved on source code also hold for the corresponding compiled code. We focus on the analysis of programs written in low-level languages. Namely, languages which feature little or no abstractions (variables, functions, objects, types…) or abstractions that the programmer is allowed to break. This hampers the task of a static analyser which thus cannot rely on these abstractions to yield precise results. We discuss in particular how to automatically recover the control-flow graph of binary self-modifying programs, and how to automatically prove that a program written in C (in which pointer arithmetic is pervasive) cannot produce a run-time error

Gli stili APA, Harvard, Vancouver, ISO e altri

28

Hintermeier, Claus. "Déduction avec sortes ordonnées et égalités". Nancy 1, 1995. http://docnum.univ-lorraine.fr/public/SCD_T_1995_0182_HINTERMEIER.pdf.

Testo completo

Abstract (sommario):

Cette thèse est dédiée au développement de langages de spécification formels, de leur sémantique opérationnelle sous forme de systèmes de réécriture décorés et des outils de preuves associés. Nous définissons les logiques Rn et Gn, qui sont des logiques à clauses de Horn égalitaires avec prédicat d'appartenance, adaptées à la spécification et à la programmation polymorphique d'ordre supérieur avec sous-typage dynamique et paramétrique, des fonctions strictes et partielles et une sémantique initiale basée sur la théorie des ensembles. Puis, nous introduisons les termes décorés, qui représentent une structure de données bien adaptées aux spécifications et programmes équationnels typés. Ils permettent d'intégrer le raisonnement égalitaire, les fonctions partielles et le typage dynamique de termes.

Gli stili APA, Harvard, Vancouver, ISO e altri

29

Garcia, Françoise. "Etude et implémentation en ML/LCF d'un système de déduction pour logique algorithmique". Paris 7, 1985. http://www.theses.fr/1985PA077119.

Testo completo

Abstract (sommario):

Contribution aux problèmes de validation du logiciel et d'implémentation de systèmes de preuve. Une première partie est consacrée à l'étude d'une logique des programmes, une seconde a la mise en œuvre d'un outil logiciel d'aide à la déduction dans ce système formel

Gli stili APA, Harvard, Vancouver, ISO e altri

30

Bensaid, Hicham. "Utilisation des schématisations de termes en déduction automatique". Phd thesis, Université de Grenoble, 2011. http://tel.archives-ouvertes.fr/tel-00618531.

Testo completo

Abstract (sommario):

Les schématisations de termes permettent de représenter des ensembles infinis de termes ayant une structure similaire de manière finie et compacte. Dans ce travail, nous étudions certains aspects liés à l'utilisation des schématisations de termes en déduction automatique, plus particulièrement dans les méthodes de démonstration de théorèmes du premier ordre par saturation. Après une brève étude comparée des formalismes de schématisation existants, nous nous concentrons plus particulièrement sur les termes avec exposants entiers (ou I-termes). Dans un premier temps, nous proposons une nouvelle approche permettant de détecter automatiquement des régularités dans les espaces de recherche. Cette détection des régularités peut avoir plusieurs applications, notamment la découverte de lemmes nécessaires à la terminaison dans certaines preuves inductives. Nous présentons DS3, un outil qui implémente ces idées. Nous comparons notre approche avec d'autres techniques de généralisation de termes. Notre approche diffère complètement des techniques existantes car d'une part, elle est complètement indépendante de la procédure de preuve utilisée et d'autre part, elle utilise des techniques de généralisation inductive et non déductives. Nous discutons également les avantages et les inconvénients liés à l'utilisation de notre méthode et donnons des éléments informels de comparaison avec les approches existantes. Nous nous intéressons ensuite aux aspects théoriques de l'utilisation des I-termes en démonstration automatique. Nous démontrons que l'extension aux I-termes du calcul de résolution ordonnée est réfutationnellement complète, que l'extension du calcul de superposition n'est pas réfutationnellement complète et nous proposons une nouvelle règle d'inférence pour restaurer la complétude réfutationnelle. Nous proposons ensuite un algorithme d'indexation (pour une sous-classe) des I-termes, utile pour le traitement des règles de simplification et d'élimination de la redondance. Finalement nous présentons DEI, un démonstrateur automatique de théorèmes capable de gérer directement des formules contenant des I-termes. Nous évaluons les performances de ce logiciel sur un ensemble de benchmarks.

Gli stili APA, Harvard, Vancouver, ISO e altri

31

Boyer, Benoît. "Réécriture d'automates certifiée pour la vérification de modèle". Rennes 1, 2010. http://www.theses.fr/2010REN1S211.

Testo completo

Abstract (sommario):

Cette thèse s'intéresse à la vérification de programmes modélisés sous forme de systèmes de règles de réécriture. La vérification de propriétés est basée sur une analyse statique semi-automatique qui construit une sur-approximation, représentée par un automate d'arbres, de l'ensemble des termes atteignables. L'analyse est paramétrée par une abstraction qui doit être suffisamment précise pour que la propriété attendue puisse être vérifiée. Or, il est difficile de construire une telle abstraction à priori. On propose un mécanisme original de raffinement automatique par élagage de l'automate d'arbres lorsque la sur-approximation calculée, trop imprécise, est susceptible de contenir de fausses alarmes. Non seulement l'analyse s'applique à la vérification de propriétés de sûreté par non-atteignabilité, mais on montre qu'elle peut être adaptée afin de vérifier des propriétés temporelles, notamment sur le graphe des appels de méthodes d'un programme Java. Enfin, les outils réalisant cette analyse reposent sur des implémentations optimisées, clairement éloignées de la spécification originale. Pour accroître la confiance en ces outils, on fournit un vérificateur chargé de la validation de leurs résultats à posteriori. La spécification et la correction de ce validateur sont formulées et démontrées dans l'assistant de preuves Coq
This thesis addresses the verification of programs, symbolized as term rewriting systems. Program properties are verified using a semiautomatic static analysis that returns a tree automaton recognizing an over-approximation of reachable terms. This analysis is parameterized by an abstraction that has to be precise enough to check the expected property. However, it is generally hard to give such an abstraction to the analysis. Using tree automaton pruning, we propose an original mechanism of automatic refinement, which allows us to avoid false alarms that are contained in the over-approximation. The technique is initially designed to check safety properties by unreachability. We show how to extend it to check temporal properties, especially for properties about the graph of method calls for a Java program. Finally, to increase their performance, the tools performing this analysis are very optimized and their implementation is quite far from of the original specification. To trust the results of these tools, we provide a checker that is in charge of validating the results. The specification and the correction of the checker are designed and proved in the proof assistant Coq

Gli stili APA, Harvard, Vancouver, ISO e altri

32

Fallot, Laurent. "Une aide interactive à la construction de preuves en logique du premier ordre". Bordeaux 1, 1989. http://www.theses.fr/1989BOR10526.

Testo completo

Abstract (sommario):

Le systeme formel implante s'inspire de la deduction naturelle, s'approchant de l'ecriture des preuves dans un texte mathematique courant. Les resultats prouves peuvent etre sauvegardes et utilises ulterieurement comme regles d'inference pour d'autres preuves

Gli stili APA, Harvard, Vancouver, ISO e altri

33

Fissore, Olivier. "Terminaison de la réécriture sous stratégies". Nancy 1, 2003. http://www.theses.fr/2003NAN10176.

Testo completo

Abstract (sommario):

L'objectif de cette thèse est l'étude et la réalisation d'outils pour prouver la terminaison de programmes à base de règles utilisant des stratégies. Partant d'une méthode originale permettant de prouver par induction la terminaison de la réécriture innermost, nous avons amélioré et étendu ce processus de preuve à la stratégie outermost puis aux stratégies locales. Ces processus de preuve ont été implantés dans un outil nommé CARIBOO. Des langages tels qu'ELAN permettent à l'utilisateur de définir ses propres stratégies, par combinaison des règles du programme au moyen d'opérateurs adaptés. Nous avons élaboré une méthode de preuve de terminaison de ces stratégies, basée sur un processus automatique de simplification. Enfin, nous avons adapté notre processus de preuve inductif original à la preuve de la terminaison faible d'un programme, qui fournit à la fois la preuve de l'existence d'une évaluation terminante de toute donnée et un algorithme d'évaluation de cette donnée
The aim of this thesis is to study and develop tools for proving termination of rule-based languages using strategies. Starting from an original method for proving, by induction, the termination of innermost rewriting, we enhanced and extended this method to the outermost and local strategies. These proof processes have then been implemented in a tool, named CARIBOO. Such languages as ELAN make it possible for the programmer to define his own strategies, by combining rules of the program with appropriate strategy operators. We came up with a method allowing to prove termination of such strategies, based on an automatic simplification process. Finally, our original inductive proof process has been adapted to show weak termination of programs. This new process provides both the proof of termination of at least one evaluation of any data and an evaluation algorithm for this data

Gli stili APA, Harvard, Vancouver, ISO e altri

34

Trojet, Mohamed Wassim. "Approche de vérification formelle des modèles DEVS à base du langage Z". Aix-Marseille 3, 2010. http://www.theses.fr/2010AIX30040.

Testo completo

Abstract (sommario):

Le cadre général dans lequel se situe cette thèse concerne l’amélioration de la vérification et la validation des modèles de simulation par l'intégration des méthodes formelles. Notre approche consiste à doter les modèles DEVS d’une approche de vérification formelle basée sur le langage Z. DEVS est un formalisme qui permet la description et l'analyse du comportement des systèmes à évènements discrets, c'est à dire, les systèmes dont le changement d'état dépend de l'occurrence d'un évènement. Un modèle DEVS est essentiellement validé par la simulation qui permet de vérifier si celui ci décrit bien le comportement du système. Cependant, la simulation ne permet pas de détecter la présence d’une éventuelle inconsistance dans le modèle (un conflit, une ambiguïté ou une incomplétude). Pour cela, nous avons intégré un langage de spécification formelle dans le formalisme DEVS connu sous le nom de Z. Cette intégration consiste à: (1) transformer un un modèle DEVS vers une spécification Z équivalente et (2) vérifier la consistance de la spécification résultante utilisant les outils développés par la communauté Z. Ainsi un modèle DEVS est soumis à une vérification formelle automatique avant son passage à la phase de simulation
The general framework of the thesis consists in improving the verification and the validation of simulation models through the integration of formal methods. We offered an approach of formal verification of DEVS models based on Z language. DEVS is a formalism that allows the description and analysis of the behavior of discrete event systems, ie systems whose state change depends on the occurrence of an event. A DEVS model is essentially validated by the simulation which permits to verify if it correctly describes the behavior of the system. However, the simulation does not detect the presence of a possible inconsistency in the model (conflict, ambiguity or incompleteness). For this reason, we have integrated a formal specification language, known as Z, in the DEVS formalism. This integration consists in: (1) transforming a DEVS model into an equivalent Z specification and (2) verifying the consistency of the resulting specification using the tools developed by the Z community. Thus, a DEVS model is subjected to an automatic formal verification before its simulation

Gli stili APA, Harvard, Vancouver, ISO e altri

35

Schmaltz, Julien. "Une formalisation fonctionnelle des communications sur la puce". Université Joseph Fourier (Grenoble), 2006. http://www.theses.fr/2006GRE10011.

Testo completo

Abstract (sommario):

Cette thèse présente un modèle formel représentant toute architecture de communication sur la puce. Ce modèle est mathématiquement décrit par une fonction nommée GeNoC. La correction de GeNoC est exprimée par un théorème montrant que tout message émis atteint sa destination sans modification de l'information qu'il transporte. Le modèle identifie les composantes communes à toute architecture et leurs propriétés essentielles, à partir desquelles est déduite la preuve du théorème sur GeNoC. Chaque composante est représentée par une fonction sans définition explicite, mais contrainte de satisfaire ses propriétés essentielles. Ainsi, la validation de toute architecture particulière consiste en la preuve que les définitions concrètes de ses composantes satisfont les propriétés essentielles. En pratique, ce formalisme a été réalisé dans la logique du démonstrateur de théorèmes ACL2. Une méthodologie associée au modèle fournit un support systématique pour la spécification et la validation des architectures de communication sur la puce à un haut niveau d'abstraction. Pour valider notre approche, nous avons exhibé différentes architectures constituant autant de concrétisations du modèle générique GeNoC. Ces concrétisations comprennent notamment des systèmes industriels, comme le bus AMBA AHB ou le réseau Octagon de ST Microelectronics
This thesis presents a formal model that represents any on-chip communication architecture. This model is described mathematically by a function, named GeNoC. The correctness of GeNoC is expressed as a theorem, which states that messages emitted on the architecture reach their expected destination without any modification of their content. The model identifies the key constituents common to all communication architectures and their essential properties, from which the proof of the GeNoC theorem is deduced. Each constituent is represented by a function, which has no explicit definition, but that is constrained to satisfy the essential properties. Thus, the validation of a particular architecture is reduced to the proof that its concrete definition satisfies the essential properties. In practice, the model has been defined in the logic of the ACL2 theorem proving system. We defined a methodology that yields a systematic approach to the validation of communication architectures at a high level of abstraction. To validate our approach, we exhibit several architectures that constitute concrete instances of the generic model GeNoC. Some of these applications come from industrial designs, such as the AMBA AHB bus or the Octagon network from ST Microelectronics

Gli stili APA, Harvard, Vancouver, ISO e altri

36

Ji, Kailiang. "Model checking and theorem proving". Sorbonne Paris Cité, 2015. http://www.theses.fr/2015USPCC250.

Testo completo

Abstract (sommario):

Le model checking est une technique de vérification automatique de propriétés de correction de systèmes finis. Normalement, les outils de model checking ont deux caractéristiques remarquables : ils sont automatisés et ils produisent un contre-exemple si le système ne satisfait pas la propriété. La Déduction Modulo est une reformulation de la logique des prédicats où certains axiomes---possiblement tous---sont remplacés par des règles de réécriture. Le but de cette dissertation est de donner un encodage de propriétés temporelles exprimées en CTL en des formules du premier ordre, en exprimant l'équivalence logique entre les opérateurs temporels avec des règles de réécriture. De cette manière, les algorithmes de recherche de preuve conçus pour la Déduction Modulo, tels que la Résolution Modulo ou les Tableaux Modulo, peuvent être utilisés pour vérifier des propriétés temporelles de systèmes de transition finis. Afin d'accomplir le but de résoudre des problèmes de model checking avec un prouveur automatique quelconque, trois travaux sont inclus dans cette dissertation. Premièrement, nous abordons le problème de parcours de graphes en model checking avec des prouveurs automatiques. Nous proposons une façon d'encoder un graphe en tant que formule de manière à ce que le parcours du graphe correspond aux étapes de résolution. Nous présentons ensuite comment formuler les problèmes de model checking comme des formules du premier ordre en Déduction Modulo. La correction et la complétude de notre méthode montre que résoudre des problèmes de model checking CTL avec des prouveurs automatiques est faisable. Enfin, en nous appuyant sur la base théorique du deuxième travail, nous proposons une méthode de model checking symbolique. Cette méthode est implantée dans iProver Modulo, qui est un prouveur automatique du premier ordre qui utilise la Résolution Modulo Polarisée
Model checking is a technique for automatically verifying correctness properties of finite systems. Normally, model checking tools enjoy two remarkable features: they are fully automatic and a counterexample will be produced if the system fails to satisfy the property. . Deduction Modulo is a reformulation of Predicate Logic where some axioms- - - possibly ail---are replaced by rewrite rules. The focus of this dissertation is to give an encoding of temporal properties expressed in CTL as first -order formulas, by translating the logical equivalence between temporal operators into rewrite rules. This way, proof -search algorithms designed for Deduction Modulo, such as Resolution Modulo or Tableaux Modulo, can be used to verify temporal properties of finite transition systems. To achieve the aim of solving model checking problems with an off-the-shelf automated theorem proyer, three works are included in this dissertation. First, we address the graph traversai problems in model checking with automated theorem provers. As a preparation work, we propose a way of encoding a graph as a formula such that the traversal of the graph corresponds to resolution steps. Then we present the way of translating model checking problems as proving first-order formulas in Deduction Modulo. The soundness and completeness of our method shows that solving CTL model checking problems with automated theorem provers is feasible. At last, based on the theoretical basis in the second work, we propose a symbolic model checking method. This method is implemented in iProver Modulo, which is a first-order theorem proyer uses Polarized Resolution Modulo

Gli stili APA, Harvard, Vancouver, ISO e altri

37

Scharff, Christelle. "Déduction avec contraintes et simplification dans les théories équationnelles". Nancy 1, 1999. http://docnum.univ-lorraine.fr/public/SCD_T_1999_0271_SCHARFF.pdf.

Testo completo

Gli stili APA, Harvard, Vancouver, ISO e altri

38

Vanzetto, Hernán. "Automatisation des preuves et synthèse des types pour la théorie des ensembles dans le contexte de TLA+". Electronic Thesis or Diss., Université de Lorraine, 2014. http://www.theses.fr/2014LORR0208.

Testo completo

Abstract (sommario):

Cette thèse présente des techniques efficaces pour déléguer des obligations de preuves TLA+ dans des démonstrateurs automatiques basées sur la logique du premier ordre non-sortée et multi-sortée. TLA+ est un langage formel pour la spécification et vérification des systèmes concurrents et distribués. Sa partie non-temporelle basée sur une variante de la théorie des ensembles Zermelo-Fraenkel permet de définir des structures de données. Le système de preuves TLAPS pour TLA+ est un environnement de preuve interactif dans lequel les utilisateurs peuvent vérifier de manière déductive des propriétés de sûreté sur des spécifications TLA+. TLAPS est un assistant de preuve qui repose sur les utilisateurs pour guider l’effort de preuve, il permet de générer des obligations de preuve puis les transmet aux vérificateurs d’arrière-plan pour atteindre un niveau satisfaisant d’automatisation. Nous avons développé un nouveau démonstrateur d’arrière-plan qui intègre correctement dans TLAPS des vérificateurs externes automatisés, en particulier, des systèmes ATP et solveurs SMT. Deux principales composantes constituent ainsi la base formelle pour la mise en oeuvre de ce nouveau vérificateur. Le premier est un cadre de traduction générique qui permet de raccorder à TLAPS tout démonstrateur automatisé supportant les formats standards TPTP/ FOF ou SMT-LIB/AUFLIA. Afin de coder les expressions d’ordre supérieur, tels que les ensembles par compréhension ou des fonctions totales avec des domaines, la traduction de la logique du premier ordre repose sur des techniques de réécriture couplées à une méthode par abstraction. Les théories sortées telles que l’arithmétique linéaire sont intégrés par injection dans la logique multi-sortée. La deuxième composante est un algorithme pour la synthèse des types dans les formules (non-typées) TLA+. L’algorithme, qui est basé sur la résolution des contraintes, met en oeuvre un système de type avec types élémentaires, similaires à ceux de la logique multi-sortée, et une extension avec des types dépendants et par raffinement. Les informations de type obtenues sont ensuite implicitement exploitées afin d’améliorer la traduction. Cette approche a pu être validé empiriquement permettant de démontrer que les vérificateurs ATP/SMT augmentent de manière significative le développement des preuves dans TLAPS
This thesis presents effective techniques for discharging TLA+ proof obligations to automated theorem provers based on unsorted and many-sorted first-order logic. TLA+ is a formal language for specifying and verifying concurrent and distributed systems. Its non-temporal fragment is based on a variant of Zermelo-Fraenkel set theory for specifying the data structures. The TLA+ Proof System TLAPS is an interactive proof environment in which users can deductively verify safety properties of TLA+ specifications. While TLAPS is a proof assistant that relies on users for guiding the proof effort, it generates proof obligations and passes them to backend verifiers to achieve a satisfactory level of automation. We developed a new back-end prover that soundly integrates into TLAPS external automated provers, specifically, ATP systems and SMT solvers. Two main components provide the formal basis for implementing this new backend. The first is a generic translation framework that allows to plug to TLAPS any automated prover supporting the standard input formats TPTP/FOF or SMT-LIB/AUFLIA. In order to encode higher-order expressions, such as sets by comprehension or total functions with domains, the translation to first-order logic relies on term-rewriting techniques coupled with an abstraction method. Sorted theories such as linear integer arithmetic are homomorphically embedded into many-sorted logic. The second component is a type synthesis algorithm for (untyped) TLA+ formulas. The algorithm, which is based on constraint solving, implements one type system for elementary types, similar to those of many-sorted logic, and an expansion with dependent and refinement types. The obtained type information is then implicitly exploited to improve the translation. Empirical evaluation validates our approach: the ATP/SMT backend significantly boosts the proof development in TLAPS

Gli stili APA, Harvard, Vancouver, ISO e altri

39

Salvat, Eric. "Raisonner avec des opérations de graphes : graphes conceptuels et règles d'inférence". Montpellier 2, 1997. http://www.theses.fr/1997MON20192.

Testo completo

Abstract (sommario):

Le modele des graphes conceptuels a ete propose par j. F. Sowa en 1984. Les graphes conceptuels simples sont des graphes etiquetes. L'operation de base, la projection, est un morphisme de graphes. Le modele des graphes conceptuels simples possede une semantique en logique du premier ordre qui est adequate et complete par rapport a la deduction. Un interet fondamental des graphes conceptuels reside donc dans la possibilite de pouvoir effectuer des raisonnements avec des operations de graphes. Dans ce travail, nous proposons une extension du modele par des regles d'inferences du type si g1 alors g2 ou g1 et g2 sont des graphes conceptuels. Nous presentons des operations de graphes permettant d'utiliser des regles de graphes conceptuels dans des mecanismes de chainage avant et de chainage arriere. Dans les deux cas les operations proposees sont adequates et completes par rapport a la deduction en logique du premier ordre. Les graphes conceptuels emboites constituent une autre extension du modele de base. L'emboitement permet d'ajouter de l'information a l'interieur meme d'un sommet concept. Cette information est donc interne a ce sommet, c'est-a-dire qu'elle est pertinente dans le contexte represente par ce sommet. Nous avons etendu les regles de graphes conceptuels aux graphes conceptuels emboites. Tout comme precedemment les mecanismes de chainage avant et de chainage arriere definis sont adequats et complets vis-a-vis de la deduction en logique du premier ordre.

Gli stili APA, Harvard, Vancouver, ISO e altri

40

Coquand, Thierry. "Une théorie des constructions". Paris 7, 1985. http://www.theses.fr/1985PA07F126.

Testo completo

Abstract (sommario):

On propose une synthèse de différents systèmes de types: la théorie des types de Martin-Loef, le calcul d'ordre supérieur de Girard, et le calcul automath de De Bruijn. Le résultat fondamental de ce travail est une preuve de cohérence du calcul ainsi obtenu (la théorie des constructions). D'après les résultats de Girard, ce système a la puissance d'expression de l'arithmétique d'ordre supérieure. Les exemples développes sont de deux ordres: en logique (on retrouve les différents systèmes logiques connus) et en informatique (le type étant alors la spécification du programme)

Gli stili APA, Harvard, Vancouver, ISO e altri

41

Lazrak, Noureddine. "Contribution à la vérification des spécifications algébriques : application à certaines propriétés de programmes parallèles". Nancy 1, 1990. http://www.theses.fr/1990NAN10035.

Testo completo

Abstract (sommario):

Notre objectif dans cette thèse est de vérifier la validité d'une formule équationnelle dans une spécification algébrique axiomatisée par un ensemble d'équations. Une formule équationnelle est une formule universellement quantifiée d'un langage du premier ordre dont les formules atomiques sont des équations simples. Nous proposons de généraliser et d'adapter les méthodes utilisées dans le cas des équations simples pour prouver la validité des formules équationnelles. Ainsi, dans le cas de la validité inductive nous avons utilisé l'induction structurelle basée sur la récurrence classique. Nous avons proposé une méthode pour la génération automatique des schémas d'induction dans certains cas particuliers. Dans le cas de la validité équationnelle nous avons proposé une méthode basée sur la transformation et la décomposition de la formule initiale pour déterminer un ensemble représentatif d'équations simples. La validité équationnelle de ces équations est équivalente à celle de la formule initiale. Un autre mécanisme de raisonnement appelé le chaînage transitif est proposé pour tester la validité des équations contenant des relations d'ordre. L'étude théorique des principes proposés dans cette thèse a abouti à la réalisation du système de preuve pause que nous avons utilisé pour vérifier certaines relations d'asynchronisme entre les composantes qui gèrent la communication dans un système parallèle

Gli stili APA, Harvard, Vancouver, ISO e altri

42

Hermann, Odile. "Mécanisation de la recherche de preuves et de programmes en arithmétique fonctionnelle du second ordre". Nancy 1, 1995. http://www.theses.fr/1995NAN10054.

Testo completo

Abstract (sommario):

Ce travail a pour propos la synthèse de programmes à partir de preuves constructives dans un cadre logique spécifique: l'arithmétique fonctionnelle du second ordre. Une première étape consiste à proposer une transcription du système de règles initial exprime en déduction naturelle, en un système de séquents plus adapte au traitement automatique du développement de preuves. Pour mécaniser la recherche de preuves, nous définissons un ensemble de tactiques que nous prouvons correctes vis-à-vis du cadre logique de référence de façon à garantir l'adéquation du système de preuves obtenu. Parmi ces tactiques, nous nous concentrons sur les plans de preuve, tactiques particulières capables de développer complètement une preuve ou une classe de preuves. La partie centrale de notre travail consiste en une étude des mécanismes d'induction dont la mise en œuvre est nécessaire pour l'obtention de programmes définis récursivement. Nous montrons des liens entre forme d'induction, spécification du programme, définition des types de données, et réussite de la construction de la preuve. Pour tirer profit de cette étude, nous proposons une procédure de choix d'induction et un plan de preuve générique qui permet d'obtenir des programmes aussi variés que la fonction d'Ackermann, la fonction Fibonacci ou le tri d'une liste par arbre binaire. Ces travaux ont fait l'objet de l'implantation d'un système baptise SKIL (Synthesizing Knowledge in Intuitionistic Logic)

Gli stili APA, Harvard, Vancouver, ISO e altri

43

Richer, Jean-Michel. "SACRE : Une approche de résolution en logique fondée sur des techniques de satisfaction de contraintes / Jean-Michel Richer ; sous la direction de Jean-Jacques Chabrier". Dijon, 1999. http://www.theses.fr/1999DIJOS001.

Testo completo

Abstract (sommario):

La démonstration automatique s'intéresse à la preuve de théorèmes dans le cadre de la logique. Un démonstrateur automatique de théorèmes est un programme qui utilise des procédés de déduction, appelés règles d'inférence, pour inférer des conclusions qui découlent logiquement d'un ensemble d'axiomes. La recherche de preuve en logique reste un problème combinatoire complexe car elle s'attaque à des problèmes NP-complets. La complétude des méthodes employées pour la recherche de preuve implique de parcourir l'espace de recherche dans sa totalité. On est donc parfois amené à s'intéresser à des branches de l'arbre de recherche stériles pour le but à résoudre. La nécessité de disposer de mécanismes de contrôle aptes à orienter la recherche reste à l'heure actuelle une préoccupation légitime des chercheurs. La programmation en logique représente une spécialisation de la démonstration automatique qui privilégie l'efficacité des traitements en se restreignant à des clauses de Horn qui capturent le caractère procédural de certaines clauses. Un programme logique représente l'expression logique d'un algorithme qui possède l'avantage de pouvoir orienter la recherche dans une direction précise limitant ainsi l'étendue de l'espace de recherche à étudier. Dans cette thèse, nous nous intéressons à la conception d'une nouvelle méthode de résolution des problèmes de la logique des prédicats du premier ordre exprimés sous forme normale conjonctive. L'originalité de notre approche repose sur la résolution des problèmes de la logique en tant que problèmes de satisfaction de contraintes (CSP) adaptés au calcul des prédicats. Ces CSP peuvent être résolus comme des programmes logiques et secondes par des techniques heuristique performantes qui visent à limiter l'espace de recherche à étudier. La méthode qui résulte de nos travaux allie la déclarativité de la démonstration automatique à l'efficacité de la programmation en logique et de la programmation par contraintes. Elle permet de réaliser du test de consistance et du calcul de modèle sur des problèmes exprimés dans un langage de description de connaissances déclaratif et statique. Nous avons valide notre approche en concevant un logiciel, baptisé SACRE, capable sous certaines conditions de rivaliser avec les démonstrateurs automatiques les plus performants a l'heure actuelle.

Gli stili APA, Harvard, Vancouver, ISO e altri

44

Vanzetto, Hernán. "Automatisation des preuves et synthèse des types pour la théorie des ensembles dans le contexte de TLA+". Thesis, Université de Lorraine, 2014. http://www.theses.fr/2014LORR0208/document.

Testo completo

Abstract (sommario):

Cette thèse présente des techniques efficaces pour déléguer des obligations de preuves TLA+ dans des démonstrateurs automatiques basées sur la logique du premier ordre non-sortée et multi-sortée. TLA+ est un langage formel pour la spécification et vérification des systèmes concurrents et distribués. Sa partie non-temporelle basée sur une variante de la théorie des ensembles Zermelo-Fraenkel permet de définir des structures de données. Le système de preuves TLAPS pour TLA+ est un environnement de preuve interactif dans lequel les utilisateurs peuvent vérifier de manière déductive des propriétés de sûreté sur des spécifications TLA+. TLAPS est un assistant de preuve qui repose sur les utilisateurs pour guider l’effort de preuve, il permet de générer des obligations de preuve puis les transmet aux vérificateurs d’arrière-plan pour atteindre un niveau satisfaisant d’automatisation. Nous avons développé un nouveau démonstrateur d’arrière-plan qui intègre correctement dans TLAPS des vérificateurs externes automatisés, en particulier, des systèmes ATP et solveurs SMT. Deux principales composantes constituent ainsi la base formelle pour la mise en oeuvre de ce nouveau vérificateur. Le premier est un cadre de traduction générique qui permet de raccorder à TLAPS tout démonstrateur automatisé supportant les formats standards TPTP/ FOF ou SMT-LIB/AUFLIA. Afin de coder les expressions d’ordre supérieur, tels que les ensembles par compréhension ou des fonctions totales avec des domaines, la traduction de la logique du premier ordre repose sur des techniques de réécriture couplées à une méthode par abstraction. Les théories sortées telles que l’arithmétique linéaire sont intégrés par injection dans la logique multi-sortée. La deuxième composante est un algorithme pour la synthèse des types dans les formules (non-typées) TLA+. L’algorithme, qui est basé sur la résolution des contraintes, met en oeuvre un système de type avec types élémentaires, similaires à ceux de la logique multi-sortée, et une extension avec des types dépendants et par raffinement. Les informations de type obtenues sont ensuite implicitement exploitées afin d’améliorer la traduction. Cette approche a pu être validé empiriquement permettant de démontrer que les vérificateurs ATP/SMT augmentent de manière significative le développement des preuves dans TLAPS
This thesis presents effective techniques for discharging TLA+ proof obligations to automated theorem provers based on unsorted and many-sorted first-order logic. TLA+ is a formal language for specifying and verifying concurrent and distributed systems. Its non-temporal fragment is based on a variant of Zermelo-Fraenkel set theory for specifying the data structures. The TLA+ Proof System TLAPS is an interactive proof environment in which users can deductively verify safety properties of TLA+ specifications. While TLAPS is a proof assistant that relies on users for guiding the proof effort, it generates proof obligations and passes them to backend verifiers to achieve a satisfactory level of automation. We developed a new back-end prover that soundly integrates into TLAPS external automated provers, specifically, ATP systems and SMT solvers. Two main components provide the formal basis for implementing this new backend. The first is a generic translation framework that allows to plug to TLAPS any automated prover supporting the standard input formats TPTP/FOF or SMT-LIB/AUFLIA. In order to encode higher-order expressions, such as sets by comprehension or total functions with domains, the translation to first-order logic relies on term-rewriting techniques coupled with an abstraction method. Sorted theories such as linear integer arithmetic are homomorphically embedded into many-sorted logic. The second component is a type synthesis algorithm for (untyped) TLA+ formulas. The algorithm, which is based on constraint solving, implements one type system for elementary types, similar to those of many-sorted logic, and an expansion with dependent and refinement types. The obtained type information is then implicitly exploited to improve the translation. Empirical evaluation validates our approach: the ATP/SMT backend significantly boosts the proof development in TLAPS

Gli stili APA, Harvard, Vancouver, ISO e altri

45

Touleimat, Mohamed Nizar. "Méthodologie d'extraction et d'analyse de réseaux de régulation de gènes : analyse de la réponse transcriptionnelle à l'irradiation chez S. cerevisiæ". Thesis, Evry-Val d'Essonne, 2008. http://www.theses.fr/2008EVRY0044/document.

Testo completo

Abstract (sommario):

La réponse cellulaire aux dommages de l'ADN provoqués par l'irradiation (IR) est relativement bien étudiée mais de nombreuses observations montrent l'implication de l'expression de nombreux gènes. Nous souhaitons identifier les différentes formes de la réponse transcriptionnelle à l'IR et reconstruire un réseau de régulation génique impliqué dans son contrôle. La problématique réside dans l'exploitation de dynamiques d'expression de gènes dans des conditions de perturbations génétiques et dans l'intégration d'informations biologiques systémiques. Nous définissons une approche constituée d'une étape automatisée de déduction de régulations à partir de perturbations et de deux étapes d'induction qui permettent d'analyser la dynamique d'expression des gènes et d'extraire des régulations des données additionnelles. Cela nous a permis d'identifier, chez la levure, une réponse complexe à l'IR et de proposer un modèle de régulation dont certaines relations ont été validées expérimentalement
The cellular response to the DNA damage provoked by irradiation (IR) is relatively well studied, however, many observations show the involvement of the expression of many genes. We propose to identify the different potential patterns of the transcriptional response to IR and to reconstruct a gene regulatory network involved in its control. The first point of this work lies in the exploitation of the gene expression dynamics in conditions of genetic perturbations. The second point lies in the integration of systemic biological informations. We define an approach composed of one step of automated logical deduction of regulations from a strategy of perturbations and two induction steps that allow the analysis of the gene expression dynamics and the extraction of potential regulation from additional data. This approach allowed to identify, for the yeast, a complex response to IR and allowed to propose a regulation model which some relations have been experimentally validated

Gli stili APA, Harvard, Vancouver, ISO e altri

46

Burel, Guillaume. "Bonnes démonstrations en déduction modulo". Phd thesis, Université Henri Poincaré - Nancy I, 2009. http://tel.archives-ouvertes.fr/tel-00372596.

Testo completo

Abstract (sommario):

Cette thèse étudie comment l'intégration du calcul dans les démonstrations peut les simplifier. Nous nous intéressons pour cela à la déduction modulo et à la surdéduction, deux formalismes proches dans lesquels le calcul est incorporé dans les démonstrations via un système de réécriture. Pour améliorer la recherche mécanisée de démonstration, nous considérons trois critères de simplicité.

L'admissibilité des coupures permet de restreindre l'espace de recherche des démonstrations, mais elle n'est pas toujours assurée en déduction modulo. Nous définissons une procédure qui complète le système de réécriture pour, au final, admettre les coupures. Au passage, nous montrons comment transformer toute théorie pour l'intégrer à la partie calculatoire des démonstrations.

Nous montrons ensuite comment la déduction modulo permet de réduire arbitrairement la taille des démonstrations, en transférant des étapes de déduction dans le calcul. En particulier, nous appliquons ceci à l'arithmétique d'ordre supérieur pour démontrer que les réductions de taille qui sont possibles en augmentant l'ordre dans lequel on se place disparaissent si on travaille en déduction modulo.

Suite à ce dernier résultat, nous avons recherchés quels sont les systèmes d'ordre supérieur pouvant être simulés au premier ordre, en déduction modulo. Nous nous sommes intéressés aux systèmes de type purs et nous montrons comment ils peuvent être encodés en surdéduction, ce qui offre de nouvelles perspectives concernant leur normalisation et la recherche de démonstration dans ceux-ci. Nous développons également une méthodologie qui permet d'utiliser la surdéduction pour spécifier des systèmes de déduction.

Gli stili APA, Harvard, Vancouver, ISO e altri

47

Urso, Pascal. "Généralisations et méthodes correctes pour l'induction mathématique". Phd thesis, Université de Nice Sophia-Antipolis, 2002. http://tel.archives-ouvertes.fr/tel-00505928.

Testo completo

Abstract (sommario):

Il existe de nombreux systèmes de preuves par induction visant à automatiser la preuve de théorèmes mathématiques. Cependant, un système de preuve ne peut pas être réellement automatique si plusieurs interactions humaines -- telles que l'apport de lemmes, de généralisations, ou de schémas d'induction -- sont nécessaires pour prouver des théorèmes qui semblent triviaux pour un être humain. Par exemple, la preuve de la commutativité de la multiplication (y * x = x * y) doit notamment recourir à des lemmes exprimant la distributivité de la multiplication ainsi que la distributivité et la commutativité de l'addition. Dans cette thèse, nous proposons des apports aux méthodes de preuve par induction dans le sens d'une plus grande automatisation. Ces apports sont constitués de deux heuristiques efficaces et surtout de deux algorithmes corrects. Le premier algorithme calcule des généralisations correctes pour des théories non-conditionnelles. Le second est une méthode d'induction originale -- la "partition de termes"-- permettant la preuve automatique de théorèmes inductifs.

Gli stili APA, Harvard, Vancouver, ISO e altri

48

Aravantinos, Vincent. "Schémas de formules et de preuves en logique propositionnelle". Phd thesis, Grenoble, 2010. http://www.theses.fr/2010GRENM044.

Testo completo

Abstract (sommario):

Le domaine de cette thèse est la déduction automatique, c. -à-d. Le développement d'algorithmes dont le but est de prouver automatiquement des conjectures mathématiques. Dans cette thèse, les conjectures que nous voulons prouver appartiennent à une extension de la logique propositionnelle, appelée "schémas de formules". Ces objets permettent de représenter de façon finie une infinité de formules propositionnelles (de même que, p. Ex. , les langages réguliers permettent de représenter de façon finie des ensembles infinis de mots). Démontrer un schéma de formules revient alors à démontrer (en une fois) l'infinité de formules qu'il représente. Nous montrons que le problème de démontrer des schémas de formules est indécidable en général. La suite de la thèse s'articule autour de la définition d'algorithmes essayant tout de même de prouver automatiquement des schémas (mais, bien sûr, qui ne terminent pas en général). Ces algorithmes nous permettent d'identifier des classes décidables de schémas, c. -à-d. Des classes pour lesquelles il existe un algorithme qui termine sur n'importe quelle entrée en répondant si le schéma est vrai ou pas. L'un de ces algorithmes a donné lieu à l'implémentation d'un prototype. Les méthodes de preuves présentées mélangent méthodes de preuve classiques en logique propositionnelle (DPLL ou tableaux sémantiques) et raisonnement par récurrence. Le raisonnement par récurrence est effectuée par l'utilisation de "preuves cycliques", c. -à-d. Des preuves infinies dans lesquelles nous détectons des cycles. Dans ce cas, nous pouvons ramener les preuves infinies à des objets finis, ce que nous pouvons appeler des "schémas de preuves"
This thesis lies in the field of automated deduction, i. E. The development of algorithms aiming at proving automatically some mathematical conjectures. In this thesis, the conjectures that we want to prove belong to an extension of propositional logic called ``formula schemas''. Those objects allow to represent infinitely many propositional formulae in a finite way (similarly to the way that regular languages finitely represent infinitely many words). Proving a formula schema amounts to prove (at once) all the formulae that it represents. We show that the problem of proving formula schemas is undecidable in general. The remaining part of the thesis presents algorithms that still try to prove schemas (event though, of course, they do not terminate in general). Those algorithms allow to identify decidable classes of schemas, i. E. Classes for which there exists an algorithm that always terminates for any entry by answering if the schema is valid or not. One of those algorithms have been implemented. Proof methods that are presented here mix classical procedures for propositional logic (DPLL or semantic tableaux) and inductive reasoning. Inductive reasoning is achieved by the use of ``cyclic proofs'', i. E. Infinite proofs in which cycles are automatically detected. In such a case, we can turn those infinite proofs into finite objects, which we can call ``proofs schemas''

Gli stili APA, Harvard, Vancouver, ISO e altri

49

Aravantinos, Vincent. "Schémas de formules et de preuves en logique propositionnelle". Phd thesis, Grenoble, 2010. http://tel.archives-ouvertes.fr/tel-00523658.

Testo completo

Abstract (sommario):

Le domaine de cette thèse est la déduction automatique, c.-à-d. le développement d'algorithmes dont le but est de prouver automatiquement des conjectures mathématiques. Dans cette thèse, les conjectures que nous voulons prouver appartiennent à une extension de la logique propositionnelle, appelée "schémas de formules". Ces objets permettent de représenter de façon finie une infinité de formules propositionnelles (de même que, p.ex., les langages réguliers permettent de représenter de façon finie des ensembles infinis de mots). Démontrer un schéma de formules revient alors à démontrer (en une fois) l'infinité de formules qu'il représente. Nous montrons que le problème de démontrer des schémas de formules est indécidable en général. La suite de la thèse s'articule autour de la définition d'algorithmes essayant tout de même de prouver automatiquement des schémas (mais, bien sûr, qui ne terminent pas en général). Ces algorithmes nous permettent d'identifier des classes décidables de schémas, c.-à-d. des classes pour lesquelles il existe un algorithme qui termine sur n'importe quelle entrée en répondant si le schéma est vrai ou pas. L'un de ces algorithmes a donné lieu à l'implémentation d'un prototype. Les méthodes de preuves présentées mélangent méthodes de preuve classiques en logique propositionnelle (DPLL ou tableaux sémantiques) et raisonnement par récurrence. Le raisonnement par récurrence est effectuée par l'utilisation de "preuves cycliques", c.-à-d. des preuves infinies dans lesquelles nous détectons des cycles. Dans ce cas, nous pouvons ramener les preuves infinies à des objets finis, ce que nous pouvons appeler des "schémas de preuves".

Gli stili APA, Harvard, Vancouver, ISO e altri

50

Tran, Duc-Khanh. "Conception de Procédures de Décision par Combinaison et Saturation". Phd thesis, Université Henri Poincaré - Nancy I, 2007. http://tel.archives-ouvertes.fr/tel-00580582.

Testo completo

Abstract (sommario):

Beaucoup d'applications des méthodes formelles reposent sur la génération de formules en logique du premier ordre et la preuve de leur satisfiabilité par rapport à une théorie en arrière-plan, qui est souvent obtenu par mélange de plusieurs théories. Dans la littérature, cette forme de satisfiabilité est appelée Satisfiabilité Modulo Théories (SMT). Dans cette thèse, on s'intéresse à la conception de procédures de décision pour les problèmes SMT, en intégrant des techniques de saturation basées sur la réécriture pour des théories finiment axiomatisées et des techniques de combinaison pour des unions de théories. La première contribution de cette thèse est une reconstruction raisonnée, dans un cadre uniforme, des méthodes de combinaison proposées par Nelson-Oppen, Shostak et d'autres. Ceci est le point de départ pour de nouvelles investigations. Nous introduisons ensuite le concept de canoniseur étendu et dérivons un résultat de modularité pour une nouvelle classe de théories, ce qui contraste avec l'absence de modularité pour la classe de théories considérée par Shostak. La deuxième contribution concerne le problème de la combinaison de procédures basées sur la réécriture en utilisant la méthode de Nelson-Oppen. Nous utilisons la méta-saturation pour développer des techniques de preuve automatique permettant de tester les conditions pour la combinabilité de telles procédures. Lorsque la méta-saturation termine pour une théorie, le résultat obtenu permet de raisonner sur la combinabilité pour cette théorie d'une procédure de satisfiabilité basée sur la réécriture. La troisième contribution de cette thèse est liée à l'intégration des procédures de décision dans les solveurs SMT. Nous considérons le problème de rajouter aux procédures de décision la capacité de construire des justifications en cas d'insatisfiabilité, sans dégradation des performances, en nous focalisant sur la construction modulaire de telles justifications pour une théorie combinée. Pour ce faire, nous étendons la méthode de combinaison de Nelson-Oppen de manière à construire de façon modulaire des justisfications d'insatisfiabilité pour des unions de théories. Nous étudions également comment les justifications obtenues peuvent être reliées à une forme appropriée de minimalité.

Gli stili APA, Harvard, Vancouver, ISO e altri

Tesi sul tema "Démonstration automatisée de théorèmes"

Cita una fonte nei formati APA, MLA, Chicago, Harvard e in molti altri stili