Bibliografias temáticas / Démonstration automatisée de théorèmes / Teses / dissertações
Siga este link para ver outros tipos de publicações sobre o tema: Démonstration automatisée de théorèmes.

Teses / dissertações sobre o tema "Démonstration automatisée de théorèmes"

Autor: Grafiati
Publicado: 31 de agosto de 2024

Crie uma referência precisa em APA, MLA, Chicago, Harvard, e outros estilos

Selecione um tipo de fonte:

Veja os 50 melhores trabalhos (teses / dissertações) para estudos sobre o assunto "Démonstration automatisée de théorèmes".

Ao lado de cada fonte na lista de referências, há um botão "Adicionar à bibliografia". Clique e geraremos automaticamente a citação bibliográfica do trabalho escolhido no estilo de citação de que você precisa: APA, MLA, Harvard, Chicago, Vancouver, etc.

Você também pode baixar o texto completo da publicação científica em formato .pdf e ler o resumo do trabalho online se estiver presente nos metadados.

Veja as teses / dissertações das mais diversas áreas científicas e compile uma bibliografia correta.

1

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

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
2

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

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
3

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

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
5

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

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
7

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

Texto completo da fonte
Resumo:
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é
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
9

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

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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.
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
13

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

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
16

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

Texto completo da fonte
Resumo:
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é
Estilos ABNT, Harvard, Vancouver, APA, etc.
17

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

Texto completo da fonte
Resumo:
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é
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
19

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

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
22

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

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
23

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

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
24

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

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
25

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

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
26

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

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
27

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

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
32

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

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
33

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

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
35

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

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
36

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

Texto completo da fonte
Resumo:
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'
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
40

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

Texto completo da fonte
Resumo:
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)
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
48

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

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
49

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

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
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.

Texto completo da fonte
Resumo:
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
Estilos ABNT, Harvard, Vancouver, APA, etc.
Oferecemos descontos em todos os planos premium para autores cujas obras estão incluídas em seleções literárias temáticas. Contate-nos para obter um código promocional único!

Vá para a bibliografia