No description available.

La planification des opérations dans un contexte industriel est une tâche complexe. Une bonne solution est difficile à obtenir, puisqu’elle doit respecter bon nombre de contraintes. Trouver la solution optimale est encore plus ardu. Pour ce faire, les entreprises ont recours à toutes sortes de méthodes, dont l’utilisation de modèles mathématiques d’optimisation. Bien que ces modèles fournissent une solution optimale, ils ne sont généralement qu’une approximation de la réalité. Pour pallier cette situation, nous proposons un système de tableaux de bord personnalisables permettant l’ajout facile et dynamique de préférences de la part du décideur. Comme l’ajout successif de préférences peut mener à la situation où chaque nouvelle préférence efface les précédentes, le décideur peut ne jamais obtenir la solution désirée même si elle existe. Pour contrer cette limitation, nous proposons une méthode permettant d’imposer des préférences pour les modifications futures. Ceci permet donc au décideur de converger rapidement vers la solution désirée. Une série d’expérimentations montre que l’utilisation d’un solveur offrira une plus grande diversité de solutions que l’utilisation de notre méthode si plusieurs préférences sont imposées. Cependant, le temps requis pour trouver des solutions par notre méthode est largement inférieur au temps nécessaire par un solveur. Le système de tableau de bord que nous avons développé permet uniquement l’utilisation de modèles linéaires, cependant les modèles à nombre entiers sont largement utilisés par les entreprises. Pour étendre l’utilisation de notre système, nous proposons une extension à l’approche originale qui permet l’utilisation de modèles à nombre entiers avec notre système de tableau de bord.

Submitted by Helen Gomes da Silva (helen-277@hotmail.com) on 2018-04-19T16:16:53Z No. of bitstreams: 1 Dissert_Helen.pdf: 519297 bytes, checksum: 5cb7a2e4a99a88a45d87901f4e7476cd (MD5) / Approved for entry into archive by Satie Tagara (satie@marilia.unesp.br) on 2018-04-19T17:33:50Z (GMT) No. of bitstreams: 1 silva_hg_me_mar.pdf: 519297 bytes, checksum: 5cb7a2e4a99a88a45d87901f4e7476cd (MD5) / Made available in DSpace on 2018-04-19T17:33:50Z (GMT). No. of bitstreams: 1 silva_hg_me_mar.pdf: 519297 bytes, checksum: 5cb7a2e4a99a88a45d87901f4e7476cd (MD5) Previous issue date: 2018-02-23 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES) / O professor Newton C. A. da Costa, notável lógico brasileiro, e colaboradores introduziram a noção de quase-verdade no contexto das ciências empíricas, onde há incompletude do conhecimento. Tal abordagem é considerada uma generalização para contextos parciais da proposta de formalização da verdade introduzida por Alfred Tarski. Inspirado nessa noção de quase-verdade, Silvestrini (2011) introduziu uma de nição de quase-verdade através da satisfação pragmática e, no mesmo trabalho apresentou, num sistema axiomático, uma lógica paraconsistente e trivalente, subjacente a essa noção, a qual denominou por Lógica da Verdade Pragmática (LPT- Logic of Pragmatic Truth ). Posteriormente, Feitosa e Silvestrini (2016) apresentaram algumas alterações no conjunto de axiomas de LPT e deram uma demonstração de adequação segundo a semântica matricial da lógica da verdade pragmática. Hoje, sistemas dedutivos alternativos ao axiomático têm sido de grande interesse para a área da teoria da prova e computabilidade, pois esses, em sua maioria, são métodos mais intuitivos. Alguns são caracterizados como algorítmicos, o que possibilita uma fácil implementação do método em computadores. Dentre esses sistemas de provas, destacamos o método dedutivo dos tableaux analíticos, que foi introduzido de uma forma bastante elegante por Smullyan (1968). Neste trabalho, introduzimos um sistema de tableaux analíticos para a Lógica da Verdade Pragmática e veri camos que todos os resultados dedutivos do sistema axiomático da LPT coincidem com os resultados de consequência analítica do sistema de tableaux que aqui introduzimos. / Professor Newton C. A. da Costa, notable Brazilian logician, and collaborators introduced the notion of quasi-truth in the context of the empirical sciences, where there is incompleteness of knowledge. Such an approach is considered a generalization of Tarski's proposal for partial contexts. Inspired by this notion of quasi-truth, Silvestrini (2011) introduced a de nition of quasi-truth through pragmatic satisfaction and, in the same work, presented, in an axiomatic system, a paraconsistent and trivalent logic, underlying this notion, which he called 'Logic of Pragmatic Truth (LPT)'. Later, Feitosa and Silvestrini (2016) presented some changes in the set of axioms of LPT and gave a proof of adequacy according to the trivalent matrix semantics of LPT. Nowadays, alternative axiomatic deductive systems have been of great interest to proof theory and computability, because these are in general intuitive methods. Some of them are characterized as algorithmic, which allows an easy implementation in computers. Among these systems of proof, we highlight the deductive method of analytic tableaux, which was introduced in an elegant way by Smullyan (1968). In this work, we introduce an analytic tableau system for the Logic of Pragmatic Truth and we verify that the results we can develop in the axiomatic system of the LPT coincide with the deductions in this analytic system of tableaux.

Le cône diamant a été introduit par N. J. Wildberger pour l'algèbre de Lie sl(n;R). C'est une présentation combinatoire d'une base de l'espace C[N] des fonctions polynomiales sur le facteur nilpotent N de la décompositon d'Iwasawa de SL(n;R), qui respecte la stratification naturelle de ce N-module indécomposable. Cette approche combinatoire peut se réaliser à l'aide de tableaux de Young, qui indexent une telle base. On réalise l'algèbre C[N] comme un quotient, appelé algèbre de forme réduite, de l'algèbre de forme S_ de SL(n;R), on en déduit une base indexée par des tableaux de Young semi standards particuliers, dits tableaux quasi standards. Dans cette thèse cette construction est étendue aux cas des algèbres semi simples de rang 2, puis des algèbres sp(2n), enfin aux super algèbres de Lie sl(m; 1). Dans chaque cas, on définit les tableaux quasi standards, et on montre qu'ils forment une bonne base de l'algèbre de forme réduite, soit directement, soit en utilisant une variante du jeu de taquin de Schützenberger. / The diamond cone was introduced by N. J. Wildberger for the Lie algebra sl(n;R). It is a combinatoric presentation for the space C[N] of polynomials functions on the nilpotent factor N in the Iwasawa decomposition of SL(n;R). This presentation describes the natural layering of this indecomposable N-module. This basis can be indexeded by using some semi standard Young tableaux. We realize the algebra C[N] as a quotient of the shape algebra S_ for SL(n;R). Let us call reduced shape algebra this quotient. It is possible to select a family of semi standard Young tableaux, the quasi standard tableaux, in such a manner to get a basis for the reduced shape algebra. In the present thesis, this construction is extended to the case of rank 2 semi simple Lie algebras, then to the cas of the Lie algebras sp(2n), finally, to the case of the super simple Lie algebra sl(m; 1). In each case, we define the quasi standard Young tableaux, and show they define a good basis for the reduced shape algebra, either directly, or using an adapted version of the jeu de taquin defined by Schützenberger.

Le raisonnement assisté par ordinateur joue un rôle crucial en informatique et en logique mathématique, de la programmation logique à la déduction automatique, en passant par les assistants à la démonstration. Le but de cette thèse est la conception d'un cadre général où différentes techniques de raisonnement assisté par ordinateur peuvent être implémentées, pour que ces dernières puissent collaborer, être généralisées, et être implémentées de manière plus sûre. Le cadre que je propose est un calcul des séquents appelé LKp(T), qui généralise un système de la littérature à la présence d'une théorie pour laquelle nous avons une procédure de décision, comme l'arithmétique linéaire. Cette thèse développe la méta-théorie de LKp(T), avec par exemple la propriété de complétude logique. Nous montrons ensuite comment le système spécifie une procédure de recherche de preuve qui émule une technique connue du domaine de la Satisfiabilité-modulo-théories appelée DPLL(T). Enfin, les tableaux de clauses et les tableaux de connexions sont d'autres techniques populaires en déduction automatique, d'une nature relativement différente de DPLL. Cette thèse décrit donc également comment ces techniques de tableaux peuvent être décrites en termes de recherche de preuve dans LKp(T). La simulation est donnée à la fois pour la logique propositionnelle et la logique du premier ordre, ce qui ouvre de nouvelles perspectives de généralisation et de collaboration entre les techniques de tableaux et DPLL, même en présence d'une théorie.

Le cône diamant a été introduit par N. J. Wildberger pour l'algèbre de Lie sl(n;R). C'est une présentation combinatoire d'une base de l'espace C[N] des fonctions polynomiales sur le facteur nilpotent N de la décompositon d'Iwasawa de SL(n;R), qui respecte la stratification naturelle de ce N-module indécomposable. Cette approche combinatoire peut se réaliser à l'aide de tableaux de Young, qui indexent une telle base. On réalise l'algèbre C[N] comme un quotient, appelé algèbre de forme réduite, de l'algèbre de forme S_ de SL(n;R), on en déduit une base indexée par des tableaux de Young semi standards particuliers, dits tableaux quasi standards. Dans cette thèse cette construction est étendue aux cas des algèbres semi simples de rang 2, puis des algèbres sp(2n), enfin aux super algèbres de Lie sl(m; 1). Dans chaque cas, on définit les tableaux quasi standards, et on montre qu'ils forment une bonne base de l'algèbre de forme réduite, soit directement, soit en utilisant une variante du jeu de taquin de Schützenberger.

Automated deduction procedures for modal logics, and related decidable fragments of first-order logic, are used in many real-world applications. A popular way of obtaining decision procedures for these logics is to base them on semantic tableau calculi. We focus on calculi that use unification, instead of the more widely employed approach of generating ground instantiations over the course of a derivation. The most common type of tableaux with unification are so-called free-variable tableaux, where variables are treated as global to the entire tableau. A long-standing open problem for procedures based on free-variable tableaux is how to ensure fairness, in the sense that "equivalent" applications of the closure rule are prevented from being done over and over again. Some solutions such as using depth-first iterative deepening are known, but those are unnecessary in theory, and not very efficient in practice. This is a main reason why there are hardly any decision procedures for modal logics based on free-variable tableaux. In this thesis, we review existing work on incorporating unification into first-order and modal tableau procedures, show how the closure fairness problem arises, and discuss existing solutions to it. For the first-order case, we outline a calculus which addresses the closure fairness problem. As opposed to free-variable tableaux, closure fairness is much easier to achieve in disconnection tableaux and similar clausal calculi. We therefore focus on using clausal first-order tableau calculi for decidable classes, in particular the two-variable fragment. Using the so-called unrestricted blocking mechanism for enforcing termination, we present the first ground tableau decision procedure for this fragment. Even for such a ground calculus, guaranteeing that depth-first terminations terminate is highly non-trivial. We parametrise our procedure by a so-called lookahead amount, and prove that this parameter is crucial for determining whether depth-first derivations terminate or not. Extending these ideas to tableaux with unification, we specify a preliminary disconnection tableau procedure which uses a non-grounding version of the unrestricted blocking rule.

La Méthode B est une méthode formelle de spécification et de développement de logiciels critiques largement utilisée dans l'industrie ferroviaire. Elle permet le développement de programmes dit corrects par construction, grâce à une procédure de raffinements successifs d'une spécification abstraite jusqu'à une implantation déterministe du programme. La correction des étapes de raffinement est garantie par la vérification de la correction de formules mathématiques appelées obligations de preuve et exprimées dans la théorie des ensembles de la Méthode B. Les projets industriels utilisant la Méthode B génèrent généralement des milliers d'obligation de preuve. La faisabilité et la rapidité du développement dépendent donc fortement d'outils automatiques pour prouver ces formules mathématiques. Un outil logiciel, appelé Atelier B, spécialement développé pour aider au développement de projet avec la Méthode B, aide les utilisateurs a se décharger des obligations de preuve, automatiquement ou interactivement. Améliorer la vérification automatique des obligations de preuve est donc une tache importante. La solution que nous proposons est d'utiliser Zenon, un outils de déduction automatique pour la logique du premier ordre et qui implémente la méthode des tableaux. La particularité de Zenon est de générer des certificats de preuve, des preuves écrites dans un certain format et qui permettent leur vérification automatique par un outil tiers. La théorie des ensembles de la Méthode B est une théorie des ensembles en logique du premier ordre qui fait appel à des schémas d'axiomes polymorphes. Pour améliorer la preuve automatique avec celle-ci, nous avons étendu l'algorithme de recherche de preuve de Zenon au polymorphisme et à la déduction modulo théorie. Ce nouvel outil, qui constitue le cœur de notre contribution, est appelé Zenon Modulo. L'extension de Zenon au polymorphisme nous a permis de traiter, efficacement et sans encodage, les problèmes utilisant en même temps plusieurs types, par exemple les booléens et les entiers, et des axiomes génériques, tels ceux de la théorie des ensembles de B. La déduction modulo théorie est une extension de la logique du premier ordre à la réécriture des termes et des propositions. Cette méthode est parfaitement adaptée à la recherche de preuve dans les théories axiomatiques puisqu'elle permet de transformer des axiomes en règles de réécriture. Par ce moyen, nous passons d'une recherche de preuve dans des axiomes à du calcul, réduisant ainsi l'explosion combinatoire de la recherche de preuve en présence d'axiomes et compressant la taille des preuves en ne gardant que les étapes intéressantes. La certification des preuves de Zenon Modulo, une autre originalité de nos travaux, est faite à l'aide de Dedukti, un vérificateur universel de preuve qui permet de certifier les preuves provenant de nombreux outils différents, et basé sur la déduction modulo théorie. Ce travail fait parti d'un projet plus large appelé BWare, qui réunit des organismes de recherche académique et des industriels autour de la démonstration automatique d'obligations de preuve dans l'Atelier B. Les partenaires industriels ont fournit à BWare un ensemble d'obligation de preuve venant de vrais projets industriels utilisant la Méthode B, nous permettant ainsi de tester notre outil Zenon Modulo.Les résultats expérimentaux obtenus sur cet ensemble de référence sont particulièrement convaincant puisque Zenon Modulo prouve plus d'obligation de preuve que les outils de déduction automatique de référence au premier ordre. De plus, tous les certificats de preuve produits par Zenon Modulo ont été validés par Dedukti, nous permettant ainsi d'être très confiant dans la correction de notre travail. / The B Method is a formal method heavily used in the railway industry to specify and develop safety-critical software. It allows the development of correct-by-construction programs, thanks to a refinement process from an abstract specification to a deterministic implementation of the program. The soundness of the refinement steps depends on the validity of logical formulas called proof obligations, expressed in a specific typed set theory. Typical industrial projects using the B Method generate thousands of proof obligations, thereby relying on automated tools to discharge as many as possible proof obligations. A specific tool, called Atelier B, designed to implement the B Method and provided with a theorem prover, helps users verify the validity of proof obligations, automatically or interactively. Improving the automated verification of proof obligations is a crucial task for the speed and ease of development. The solution developed in our work is to use Zenon, a first-orderlogic automated theorem prover based on the tableaux method. The particular feature of Zenon is to generate proof certificates, i.e. proof objects that can be verified by external tools. The B Method is based on first-order logic and a specific typed set theory. To improve automated theorem proving in this theory, we extend the proof-search algorithm of Zenon to polymorphism and deduction modulo theory, leading to a new tool called Zenon Modulo which is the main contribution of our work. The extension to polymorphism allows us to deal with problems combining several sorts, like booleans and integers, and generic axioms, like B set theory axioms, without relying on encodings. Deduction modulo theory is an extension of first-order logic with rewriting both on terms and propositions. It is well suited for proof search in axiomatic theories, as it turns axioms into rewrite rules. This way, we turn proof search among axioms into computations, avoiding unnecessary combinatorial explosion, and reducing the size of proofs by recording only their meaningful steps. To certify Zenon Modulo proofs, we choose to rely on Dedukti, a proof-checker used as a universal backend to verify proofs coming from different theorem provers,and based on deduction modulo theory. This work is part of a larger project called BWare, which gathers academic entities and industrial companies around automated theorem proving for the B Method. These industrial partners provide to BWare a large benchmark of proof obligations coming from real industrial projects using the B Method and allowing us to test our tool Zenon Modulo. The experimental results obtained on this benchmark are particularly conclusive since Zenon Modulo proves more proof obligations than state-of-the-art first-order provers. In addition, all the proof certificates produced by Zenon Modulo on this benchmark are well checked by Dedukti, increasing our confidence in the soundness of our work.

Comment reconnaît –on que l'apprentissage est efficace ? C’est une de nos questions à laquelle nous cherchons à répondre dans notre fonction de conseillère pédagogique. Bon nombre d'enseignants se plaignent que les élèves ne font pas l'unité des connaissances qu'ils acquièrent. Nous soulignons en particulier les mathématiques et les sciences physiques qui restent des vases étanches. Ce sont des îlots qu'il faut découvrir un à un sans se soucier de leur complémentarité. Certaines questions nous retiennent, est-ce que la présentation du programme et des contenus favorise l'articulation transdisciplinaire des connaissances ? Est-ce que la méthode de l'enseignant guide l'élève à articuler les connaissances acquises ? Est-ce que l'élève lui-même est capable de faire le transfert des connaissances acquises ? A l'exemple de la notion de proportionnalité, dans quelle mesure la présentation des contenus relatifs à la proportionnalité dans les disciplines des mathématiques et sciences physiques, favorise-t-elle l'articulation par les élèves des connaissances et des compétences ? Notre étude va essayer d'expliciter et de comprendre comment les élèves conceptualisent les connaissances, car la première difficulté tient au fait que la capacité de transfert des connaissances de l'élève dépend de sa méthode d'intégration. Une des conditions de transfert est la construction de sens. Le transfert de compétences n'est pas l'affaire de l'élève seul bien que la plus grande partie s'impose au dernier. Chacun a son propre rapport au savoir, ce qui nous invite à tenir compte de la place de la culture malgache dans l'apprentissage. L’élève est partagé entre différents cadres. De ce fait, le cadre de rationalité est important dans l'analyse des ruptures et les filiations des connaissances et des compétences dans les disciplines. / How can we assess the way we teach is efficient? This is one of the many questions. I’ll try to answer as a teacher trainer. Many teachers complain that students are unable to unify their knowledge. We wish to emphasize the fact this particularly true of mathematics and physics which still remain as subjects taught in class as “insulated vessels”. They’re like isolated islands one has to explore one after the other, indifferent to their complementary. Various questions arise at this stage. Does the layout of curriculum and its contents help link up the knowledge, the skills developed in various subjects? Does the teacher’s approach offer the students the necessary guidance to link up the knowledge acquired in various disciplines? Are the students capable of transferring the knowledge they have acquired we’ll take the example of proportionality. To what extent the layout of the content concerning proportionality help students to link up knowledge and skill? The present work aims at explicating and analyzing how students conceptualize knowledge: the main difficulty lies in the student’s ability to transfer to transfer knowledge this depends on how the students integrate this. One of the conditions for transferring efficiently is making sense. Transferring skill doesn’t only depend on the student’s abilities although the greater part lies on the latter. Each student develops his own perception of knowledge, we have take Madagascar culture into account the process of learning students remain divided between different frameworks. Consequently the framework of rationality remains essential in the analysis of breaks and links in the knowledge and skill developed in the discipline.

Les logiques modales sont des logiques permettant la représentation et l'inférence de connaissances. La logique hybride est une extension de la logique modale de base contenant des nominaux, permettant de faire référence à un unique individu ou monde du modèle. Dans cette thèse nous présentons plusieurs algorithmes de tableaux pour logiques hybrides expressives. Nous présentons aussi une implémentation de ces calculs, et nous décrivons les tests de correction et de performance que nous avons effectués, ainsi que les outils les permettant. De plus, nous étudions en détail une famille particulière de logiques liée aux logiques hybrides : les logiques avec opérateurs de comptage. Nous étudions la complexité et la décidabilité de certains de ces langages / Modal logics are logics enabling representing and inferring knowledge. Hybrid logic is an extension of the basic modal logic that contains nominals which enable to refer to a single individual or world of the model. In this thesis, we present several tableaux-based algorithms for expressive hybrid logics. We also present an implementation of these calculi and we describe correctness and performance tests we carried out, and the tools that enable these. Moreover, we study a particular family of logics related to hybrid logics: logics with counting operators.We investigate previous results, and study the complexity and decidability of certain of these languages