Relevant bibliographies by topics / Démonstration automatisée de théorèmes / Dissertations / Theses
To see the other types of publications on this topic, follow the link: Démonstration automatisée de théorèmes.

Dissertations / Theses on the topic 'Démonstration automatisée de théorèmes'

Author: Grafiati
Published: 31 August 2024

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles

Select a source type:

Consult the top 50 dissertations / theses for your research on the topic 'Démonstration automatisée de théorèmes.'

Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.

You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.

Browse dissertations / theses on a wide variety of disciplines and organise your bibliography correctly.

1

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

Full text
Abstract:
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 com
APA, Harvard, Vancouver, ISO, and other styles
2

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

Full text
Abstract:
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
APA, Harvard, Vancouver, ISO, and other styles
3

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

Full text
Abstract:
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
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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
APA, Harvard, Vancouver, ISO, and other styles
5

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

Full text
Abstract:
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 compl
APA, Harvard, Vancouver, ISO, and other styles
6

Cubadda, Christophe, and 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.

Full text
Abstract:
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
APA, Harvard, Vancouver, ISO, and other styles
7

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

Full text
Abstract:
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é
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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
APA, Harvard, Vancouver, ISO, and other styles
9

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

Full text
Abstract:
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 perm
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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 rec
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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
APA, Harvard, Vancouver, ISO, and other styles
13

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

Full text
Abstract:
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éren
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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 consistan
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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
APA, Harvard, Vancouver, ISO, and other styles
16

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

Full text
Abstract:
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é
APA, Harvard, Vancouver, ISO, and other styles
17

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

Full text
Abstract:
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é
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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éa
APA, Harvard, Vancouver, ISO, and other styles
19

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

Full text
Abstract:
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 ce
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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écurrenc
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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équent
APA, Harvard, Vancouver, ISO, and other styles
22

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

Full text
Abstract:
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 d
APA, Harvard, Vancouver, ISO, and other styles
23

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

Full text
Abstract:
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 plusieur
APA, Harvard, Vancouver, ISO, and other styles
24

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

Full text
Abstract:
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 specifi
APA, Harvard, Vancouver, ISO, and other styles
25

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

Full text
Abstract:
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 traduc
APA, Harvard, Vancouver, ISO, and other styles
26

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

Full text
Abstract:
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 fonc
APA, Harvard, Vancouver, ISO, and other styles
27

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

Full text
Abstract:
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
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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'ar
APA, Harvard, Vancouver, ISO, and other styles
32

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

Full text
Abstract:
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
APA, Harvard, Vancouver, ISO, and other styles
33

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

Full text
Abstract:
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. No
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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 b
APA, Harvard, Vancouver, ISO, and other styles
35

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

Full text
Abstract:
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
APA, Harvard, Vancouver, ISO, and other styles
36

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

Full text
Abstract:
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'
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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
APA, Harvard, Vancouver, ISO, and other styles
40

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

Full text
Abstract:
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)
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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 t
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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 bra
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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é.<br /><br />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
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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 commutat
APA, Harvard, Vancouver, ISO, and other styles
48

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

Full text
Abstract:
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 un
APA, Harvard, Vancouver, ISO, and other styles
49

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

Full text
Abstract:
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 f
APA, Harvard, Vancouver, ISO, and other styles
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.

Full text
Abstract:
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
APA, Harvard, Vancouver, ISO, and other styles
We offer discounts on all premium plans for authors whose works are included in thematic literature selections. Contact us to get a unique promo code!

To the bibliography