Добірка наукової літератури з теми "Démonstration automatisée de théorèmes"
Оформте джерело за APA, MLA, Chicago, Harvard та іншими стилями
Ознайомтеся зі списками актуальних статей, книг, дисертацій, тез та інших наукових джерел на тему "Démonstration automatisée de théorèmes".
Біля кожної праці в переліку літератури доступна кнопка «Додати до бібліографії». Скористайтеся нею – і ми автоматично оформимо бібліографічне посилання на обрану працю в потрібному вам стилі цитування: APA, MLA, «Гарвард», «Чикаго», «Ванкувер» тощо.
Також ви можете завантажити повний текст наукової публікації у форматі «.pdf» та прочитати онлайн анотацію до роботи, якщо відповідні параметри наявні в метаданих.
Статті в журналах з теми "Démonstration automatisée de théorèmes"
Rivenc, François. "Remarques à propos d'une récente Introduction à la logique." Dialogue 38, no. 2 (1999): 369–78. http://dx.doi.org/10.1017/s0012217300007265.
Повний текст джерелаДисертації з теми "Démonstration automatisée de théorèmes"
Amaniss, Ali. "Méthodes de schématisation pour la démonstration automatique." Nancy 1, 1996. http://www.theses.fr/1996NAN10092.
Повний текст джерелаMzali, Jalel. "Méthodes de filtrage équationnel et de preuve automatique de théorèmes." Nancy 1, 1986. http://www.theses.fr/1986NAN10387.
Повний текст джерелаHerzig, Andreas. "Raisonnement automatique en logique modale et algorithmes d'unification." Toulouse 3, 1989. http://www.theses.fr/1989TOU30115.
Повний текст джерела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.
Повний текст джерелаLarchey-Wendling, Dominique. "Preuves, réfutations et contre-modèles dans des logiques intuitionnistes." Nancy 1, 2000. http://www.theses.fr/2000NAN10158.
Повний текст джерелаLogics can be used as powerful tools for specifying computer systems and proving the soundness of their implementations with respect to these specifications. In the field of substructural logics, we develop tools and methods for automated deduction and counter-model generation. These logics involve the notion of resource : at the level of proof-search, the management of resources enables more efficient procedures : at the semantic level, resource models provide sound and complete interpretations. We develop a link between the syntactic notion of refutation and the semantic notion of counter-model. We deduce methods for proving the finite model property and algorithms for implementation of a proof-search procedure, based on a fine management of resources. In intuitionistic linear logic, resource based models constitute the core of an elegant proof of the finite model property. Furthermore, we establish a link between resource models and Petri net based models, from which we improve the proeceding partial completness results
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.
Повний текст джерелаPichardie, David. "Interprétation abstraite en logique intuitionniste : extraction d'analyseurs Java certifiés." Rennes 1, 2005. http://www.theses.fr/2005REN1S183.
Повний текст джерела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.
Повний текст джерелаCruanes, Simon. "Extending superposition with integer arithmetic structural induction and beyond." Palaiseau, Ecole polytechnique, 2015. https://tel.archives-ouvertes.fr/tel-01223502.
Повний текст джерелаThe central concept of theorem designates a claim backed by an irrefutable argument that follows formal rules, called a proof. Proving theorems is very useful in both Computer Science and Mathematics. However, many theorems are too boring and tedious for human experts (for instance, theorems generated to ensure that software abides by some specification); hence the decades-long effort in automated theorem proving, the field dedicated to writing programs that find proofs. Superposition is a very competitive technique for proving theorems in the language of first-order logic with equality over uninterpreted functions (in a nutshell, being able to replace equals by equals in any expression). Even then, Superposition falls short for many problems that require theory-specific reasoning or inductive proofs. In this thesis, we aim at developing new extensions to Superposition. Our claim is that Superposition lends itself very well to being grafted additional inference rules and reasoning mechanisms. First, we develop a Superposition-based calculus for integer linear arithmetic. Linear Integer Arithmetic is a widely studied and used theory in other areas of automated deduction, in particular SMT (Satisfiability Modulo Theory). This theory might also prove useful for problems that have a discrete, totally ordered structure, such as temporal logic, and that might be encoded efficiently into first-order logic with arithmetic. Then, we define an extension of Superposition that is able to reason by structural induction (natural numbers, lists, binary trees, etc. ) Inductive reasoning is pervasive in Mathematics and Computer Science but its integration into general purpose first-order provers has not been studied much. Last, we present a theory detection system that, given a signature-agnostic description of algebraic theories, detects their presence in sets of formulas. This system is akin to the way a mathematician who studies a new object discovers that this object belong to some known structure, such as groups, allowing her to leverage the large body of knowledge on this specific theory. A large implementation effort was also carried out in this thesis; all the contributions presented above have been implemented in a library and a theorem prover, Zipperposition, both written in OCaml and released under a free software license
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.
Повний текст джерелаIn this thesis, we present several new techniques for model building in Automated Deduction. In the first part, we propose a general method for building finite models that favourably compares with the most powerful existing finite model builders. In the second part, we investigate methods for simultaneous search for refutations and (infinite, Herbrand) models. We improve the methods RAMC (Refutation And Model Construction) and RAMCET (Refutation And Model Construction with Equational Tableaux) defined by R. Caferra and N. Zabel by defining new rules and strategies. These extensions strictly increase the capabilities of the methods both for model building and unsatisfiability detection. We show that some of the proposed methods are uniform decision procedures for a wide range of decidable classes. We show the limits of the formalism of equational constraints, previously used for representing Herbrand models, and we propose to extend it by including terms with integer exponents (I-terms) and tree automata. As a new result, we prove the decidability of the first-order theory of I-terms. Fourthly, we study some applications of our work: we present a new approach for discovering and using analogy in simultaneous search for refutations and models, and we show how to use the method RAMC in Logic Programming (for extending logic program interpreters, detecting and correcting errors in logic programs etc. ). Finally we describe the system RAMC-ATINF implementing our approach and we report some experiments showing the practical capabilities of our method
Книги з теми "Démonstration automatisée de théorèmes"
1956-, Kerber Manfred, and Kohlhase Michael 1964-, eds. Symbolic computation and automated reasoning: The CALCULEMUS-2000 Symposium. Natick, Mass: A K Peters, 2001.
Знайти повний текст джерелаMcAllester, David A. Ontic: A knowledge representation system for mathematics. Cambridge, Mass: MIT Press, 1989.
Знайти повний текст джерелаSnyers, Dominique. From logic design to logic programming: Theorem proving techniques and P-functions. Berlin: Springer-Verlag, 1987.
Знайти повний текст джерелаSchumann, Johann M., and D. Loveland. Automated Theorem Proving in Software Engineering. Springer London, Limited, 2013.
Знайти повний текст джерелаSchumann, Johann M., and D. Loveland. Automated Theorem Proving in Software Engineering. Springer Berlin / Heidelberg, 2010.
Знайти повний текст джерелаBibel, W. Automated theorem proving. 1987.
Знайти повний текст джерелаThe resolution calculus. Berlin: Springer, 1997.
Знайти повний текст джерелаAutomated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX'99, Saratoga Springs, NY, USA, June 7-11, 1999, Proceedings (Lecture Notes in Computer Science). Springer, 1999.
Знайти повний текст джерелаMurray, Neil V. Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX'99, Saratoga Springs, NY, USA, June 7-11, 1999, Proceedings. Springer, 2003.
Знайти повний текст джерелаBüning, Hans Kleine, and Theodor Lettmann. Propositional Logic: Deduction and Algorithms (Cambridge Tracts in Theoretical Computer Science). Cambridge University Press, 1999.
Знайти повний текст джерелаЧастини книг з теми "Démonstration automatisée de théorèmes"
Vecten, MM, MM Querret, MM Vernier, and Ch Sturm. "Démonstration des deux théorèmes de géométrie énoncés à la page 63 du présent volume." In Collected Works of Charles François Sturm, 160–65. Basel: Birkhäuser Basel, 2009. http://dx.doi.org/10.1007/978-3-7643-7990-2_12.
Повний текст джерелаSturm, M. M. Ch, Vecten, and Querret. "Démonstration des quatre théorèmes sur l’hyperbole énoncés à la page 268 du précédent volume." In Collected Works of Charles François Sturm, 192–96. Basel: Birkhäuser Basel, 2009. http://dx.doi.org/10.1007/978-3-7643-7990-2_17.
Повний текст джерелаSturm, M. Ch. "Démonstration de deux théorèmes de géométrie, énoncés à la page 248 du XIII: volume des Annales." In Collected Works of Charles François Sturm, 141–47. Basel: Birkhäuser Basel, 2009. http://dx.doi.org/10.1007/978-3-7643-7990-2_10.
Повний текст джерела