Tesis sobre el tema "Démonstration automatisée de théorèmes"
Crea una cita precisa en los estilos APA, MLA, Chicago, Harvard y otros
Consulte los 50 mejores tesis para su investigación sobre el tema "Démonstration automatisée de théorèmes".
Junto a cada fuente en la lista de referencias hay un botón "Agregar a la bibliografía". Pulsa este botón, y generaremos automáticamente la referencia bibliográfica para la obra elegida en el estilo de cita que necesites: APA, MLA, Harvard, Vancouver, Chicago, etc.
También puede descargar el texto completo de la publicación académica en formato pdf y leer en línea su resumen siempre que esté disponible en los metadatos.
Explore tesis sobre una amplia variedad de disciplinas y organice su bibliografía correctamente.
Amaniss, Ali. "Méthodes de schématisation pour la démonstration automatique". Nancy 1, 1996. http://www.theses.fr/1996NAN10092.
Texto completoMzali, Jalel. "Méthodes de filtrage équationnel et de preuve automatique de théorèmes". Nancy 1, 1986. http://www.theses.fr/1986NAN10387.
Texto completoHerzig, Andreas. "Raisonnement automatique en logique modale et algorithmes d'unification". Toulouse 3, 1989. http://www.theses.fr/1989TOU30115.
Texto completoNoyer, 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 completoLarchey-Wendling, Dominique. "Preuves, réfutations et contre-modèles dans des logiques intuitionnistes". Nancy 1, 2000. http://www.theses.fr/2000NAN10158.
Texto completoLogics 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
Cubadda, Christophe y 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 completoPichardie, David. "Interprétation abstraite en logique intuitionniste : extraction d'analyseurs Java certifiés". Rennes 1, 2005. http://www.theses.fr/2005REN1S183.
Texto completoPuitg, 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 completoCruanes, Simon. "Extending superposition with integer arithmetic structural induction and beyond". Palaiseau, Ecole polytechnique, 2015. https://tel.archives-ouvertes.fr/tel-01223502.
Texto completoThe 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
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 completoIn 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
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 completoShminke, 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 completoThis 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
Benhammadi, Farid. "La gestion des préférences en logique des défauts". Angers, 1999. http://www.theses.fr/1999ANGE0008.
Texto completoLazrek, 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 completoJuban, 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 completoIn 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
Curien, Régis. "Outils pour la preuve". Nancy 1, 1995. http://docnum.univ-lorraine.fr/public/SCD_T_1995_0007_CURIEN.pdf.
Texto completoRusinowitch, Michaël. "Démonstration automatique par des techniques de réécritures". Nancy 1, 1987. http://www.theses.fr/1987NAN10358.
Texto completoSmirnova, 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 completoThis 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
Notin, Jean-Marc. "Recherche et construction de preuves en logique non-commutative". Nancy 1, 2004. http://www.theses.fr/2004NAN10183.
Texto completoPartially 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
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 completoMethods 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
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 completoMéry, Daniel. "Preuves et sémantiques dans des logiques de ressources". Nancy 1, 2004. http://www.theses.fr/2004NAN10160.
Texto completoResource-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
Mengin, Jérôme. "Raisonnement par défaut : résolutions de conflits et priorités". Paris 11, 1994. http://www.theses.fr/1994PA112101.
Texto completoKhan, Muhammad Uzair. "A study of first class futures : specification, formalisation, and mechanised proofs". Nice, 2011. http://www.theses.fr/2011NICE4003.
Texto completoLes 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
Coscoy, Yann. "Explication textuelle de preuves pour le calcul des constructions inductives". Nice, 2000. http://www.theses.fr/2000NICE5428.
Texto completoDas, Barman Kuntal. "Type theoretic semantics for programming languages". Nice, 2004. http://www.theses.fr/2004NICE4029.
Texto completoSemantics 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
Laporte, Vincent. "Vérification d’analyses statiques pour langages de bas niveau". Thesis, Rennes 1, 2015. http://www.theses.fr/2015REN1S078/document.
Texto completoStatic 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
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 completoGarcia, 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 completoBensaid, 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 completoBoyer, Benoît. "Réécriture d'automates certifiée pour la vérification de modèle". Rennes 1, 2010. http://www.theses.fr/2010REN1S211.
Texto completoThis 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
Fallot, Laurent. "Une aide interactive à la construction de preuves en logique du premier ordre". Bordeaux 1, 1989. http://www.theses.fr/1989BOR10526.
Texto completoFissore, Olivier. "Terminaison de la réécriture sous stratégies". Nancy 1, 2003. http://www.theses.fr/2003NAN10176.
Texto completoThe 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
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 completoThe 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
Schmaltz, Julien. "Une formalisation fonctionnelle des communications sur la puce". Université Joseph Fourier (Grenoble), 2006. http://www.theses.fr/2006GRE10011.
Texto completoThis 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
Ji, Kailiang. "Model checking and theorem proving". Sorbonne Paris Cité, 2015. http://www.theses.fr/2015USPCC250.
Texto completoModel 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
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 completoVanzetto, 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 completoThis 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
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 completoCoquand, Thierry. "Une théorie des constructions". Paris 7, 1985. http://www.theses.fr/1985PA07F126.
Texto completoLazrak, 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 completoHermann, 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 completoRicher, 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 completoVanzetto, 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 completoThis 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
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 completoThe 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
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 completoL'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.
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 completoAravantinos, Vincent. "Schémas de formules et de preuves en logique propositionnelle". Phd thesis, Grenoble, 2010. http://www.theses.fr/2010GRENM044.
Texto completoThis 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''
Aravantinos, Vincent. "Schémas de formules et de preuves en logique propositionnelle". Phd thesis, Grenoble, 2010. http://tel.archives-ouvertes.fr/tel-00523658.
Texto completoTran, 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