Whilst results from Structural Proof Theory can be couched in many formalisms, it is the sequent calculus which is the most amenable of the formalisms to metamathematical treatment. Constructive syntactic proofs are filled with bureaucratic details; rarely are all cases of a proof completed in the literature. Two intermediate results can be used to drastically reduce the amount of effort needed in proofs of Cut admissibility: Weakening and Invertibility. Indeed, whereas there are proofs of Cut admissibility which do not use Invertibility, Weakening is almost always necessary. Use of these results simply shifts the bureaucracy, however; Weakening and Invertibility, whilst more easy to prove, are still not trivial. We give a framework under which sequent calculi can be codified and analysed, which then allows us to prove various results: for a calculus to admit Weakening and for a rule to be invertible in a calculus. For the latter, even though many calculi are investigated, the general condition is simple and easily verified. The results have been applied to G3ip, G3cp, G3s, G3-LC and G4ip. Invertibility is important in another respect; that of proof-search. Should all rules in a calculus be invertible, then terminating root-first proof search gives a decision procedure for formulae without the need for back-tracking. To this end, we present some results about the manipulation of rule sets. It is shown that the transformations do not affect the expressiveness of the calculus, yet may render more rules invertible. These results can guide the design of efficient calculi. When using interactive proof assistants, every case of a proof, however complex, must be addressed and proved before one can declare the result formalised. To do this in a human readable way adds a further layer of complexity; most proof assistants give output which is only legible to a skilled user of that proof assistant. We give human-readable formalisations of Cut admissibility for G3cp and G3ip, Contraction admissibility for G4ip and Craig's Interpolation Theorem for G3i using the Isar vernacular of Isabelle. We also formalise the new invertibility results, in part using the package for reasoning about first-order languages, Nominal Isabelle. Examples are given showing the effectiveness of the formalisation. The formal proof of invertibility using the new methods is drastically shorter than the traditional, direct method.

This research is an exploratory study of the relationship between two supply chain management (SCM) concepts, namely supply chain structure and supply chain integration. The objective is to enhance the understanding of the extent to which supply chain structure is relevant to the supply chain integration, and of how this relationship between these concepts contributes to the ideas of supply chain quality (SCQ) in the manufacturing industry. The literature review with reference to the structure and integration results in the following structural dimensions: centralisation, formalisation and communication which are likely to have an effect on the supply chain integration; ultimately, on supply chain quality. For the purposes of this research, the conceptual model was developed, and its validity was explored via case-studies. The two manufacturing supply chains including their focal firms and the first-tier suppliers based in Turkey were selected as the case-supply chains. A total of 41 face-to-face, semi-structured interviews were carried out. The findings of the present study suggest that while formalisation and communication are positively related to the supply chain integration, centralisation in which a focal firm designs and manages the whole network negatively affects the supply chain integration. Hence decentralised, formalised supply chains facilitated by the means of communication are proposed in today’s global economy in order for supply chains to achieve integration, hence considered to attain supply chain quality.

The master's thesis discusses a development concept inspired by the Peruvian economist Hernando de Soto. It describes this concept and analyzes its potential to work in praxis. It introduces several critical responses addressed from a wide range of stakeholders - from civil society advocates to scholars -- and contends with their critique. Furthermore, the thesis frames this concept within the development paradigm, with a short overview of its evolution from the 50's and an emphasis on the institutional aspect. The last part analyzes results of the property rights formalization reform in Peru. The outcomes of this reform may be of major importance for the development efforts in the future. Although the anticipated connection of formalization and a better access to loans has not been proved yet, there are some other interesting effects to look at.

Reproduction de : Thèse de doctorat : Intelligence artificielle : Toulouse, INPT : 2007. / Titre provenant de l'écran-titre. Bibliogr. 167 réf.

Texte abrégé de: Thèse 3# cycle--Linguistique--Lyon II, 1973. / Thèse soutenue sous le titre : "Pour un calcul du sens, essai de formalisation de théories sémantiques" Bibliogr. p. 181-194. Index.

After more than two decades of democracy, South Africa is still faced with challenges of unemployment, poverty and inequality. The informal sector is one that presents opportunities for making a positive contribution towards solving social problems that South Africa is faced with. While the informal sector is large and offers flexibility in employment, it is associated with low productivity and poor governance as traders in the informal sector are not obliged to register their businesses and therefore cannot make tax contributions. The lack of formalisation of the informal sector not only impacts the government for not being able to account for the sector, but it also creates barriers for those trading in the sector. The study adopted qualitative research methods to gain insights into describing and exploring the meaning research participants use to construct and interpret their world of reality, such as formalising the informal sector to stimulate economic growth in South African Townships. A total of 15 semi-structured interviews were conducted with business owners in the retail informal sector, managers of big corporates in retail in the formal sector and government employees from various departments who were represented by those in relevant positions such as directors, heads of departments, regional and board members. Interviews were analysed by means of thematic analysis. The key findings from literature indicated that the informal sector is broad and there is no one definition of the informal sector. It was also established that there is a direct relationship that exists between the state and the informal sector, however there is an indirect relationship that exists between the formal and informal sector as further explained in institutional and stakeholder theory. The lack of development in the informal sector can be attributed to the non-existence of policies to guide and regulate the existence of the informal sector. The insights shared from the interviews pointed to the applicability of the proposed model in terms of formalising the informal sector. / Mini Dissertation (MBA)--University of Pretoria, 2021. / Gordon Institute of Business Science (GIBS) / MBA / Unrestricted

Dans cette thèse, nous examinons comment un assistant de preuve peut être utilise pour étudier les fondements de la géométrie. Nous débutons en nous concentrant sur les façons d’axiomatiser la géométrie euclidienne et leurs relations. Ensuite, nous exposons une nouvelle preuve de l’indépendance de l’axiome des parallèles des autres axiomes de la géométrie euclidienne du premier ordre. Cela nous amène à affiner la classification des plans de Hilbert de Pejas en considérant les propriétés de décidabilité. Mais, notre intuition nous amène souvent à négliger leur utilisation. Un assistant de preuve nous permet d’utiliser un outil parfait qui ne possède aucune intuition : un ordinateur. De plus, les assistants de preuve nous laissent exploiter les capacités de calcul des ordinateurs. Nous démontrons comment utiliser de méthodes algébriques de déduction automatique en géométrie synthétique. Enfin, nous présentons une procédure spécifique destinée à automatiser des preuves d’incidence. / In this thesis, we investigate how a proof assistant can be used to study the foundations of geometry. We start by focusing on ways to axiomatize Euclidean geometry and their relationship to each other. Then, we expose a new proof that Euclid’s parallel postulate is not derivable from the other axioms of first-order Euclidean geometry. This leads us to refine Pejas’ classification of parallel postulates. We do so by considering decidability properties when classifying the postulates. However, our intuition often guides us to overlook uses of such properties. A proof assistant allows us to use a perfect tool which possesses no intuition: a computer. Moreover, proof assistants let us leverage the computational capabilities of computers. We demonstrate how we enable the use of algebraic automated deduction methods thanks to the arithmetization of geometry. Finally, we present a specific procedure designed to automate proofs of incidence properties.

No description available.

Ce travail s’engage dans la reconstitution d’une intelligibilité globale nouvelle pour la logique qui est née avec Frege afin de restituer l’une des conditions décisives pour la philosophie contemporaine, à savoir celle qui concerne son rapport aux pratiques et aux savoirs formels. Son hypothèse initiale affirme que le projet premier et constant de Frege a été celui d’une logique du contenu. Pourtant, il ne s’agit pas de réinvestir l’œuvre de Frege d’une cohérence nouvelle dans le but de rétablir une unité stable. Car l’intelligibilité procurée par cette reconstitution permet de localiser dans les formulations de Frege de véritables lacunes qui ne semblent pas avoir été identifiées comme telles jusqu’ici. Que la logique de Frege soit efficace malgré ces lacunes, voilà ce qu’il faut expliquer. La réponse que nous donnons à ces questions est que l’efficacité de la logique de Frege en tant que logique du contenu provient d’un certain rapport à l’Arithmétique, à savoir celui par lequel c’est la logique qui est construite d’après les principes de l’Arithmétique, avant qu’elle ne soit capable de la construire à son tour. La question se pose alors de caractériser avec précision à ce niveau constitutif, non « fondationnel », la nature du rapport entre une logique du contenu comme forme spécifique de la logique dans le cadre de sa mathématisation, et l’Arithmétique comme domaine mathématique particulier. De l’analyse minutieuse de la constitution du système logique frégéen, une idée se dégage qui constitue la thèse centrale de notre travail : les différents systèmes de la logique mathématisée ou formelle ne reposent sur les mathématiques que par l’intermédiaire d’une dimension d’exercice, de réflexion et d’élaboration de signes, où les circulations et les emprunts entre ces deux savoirs formels contemporains que sont les mathématiques et la logique se construisent et se justifient. C’est donc cette thèse qu’il s’agit de démontrer, par une étude détaillée des processus d’émergence des deux plus grands projets de formalisation de la logique du XIXe siècle : celui de Frege et celui de Boole et des Booléens. Dans cet espace qui mène des pratiques mathématiques aux systématisations logiques à travers les fonctionnements des signes, deux régimes généraux se dessinent : celui d’ « Abstraction symbolique » qui mène de l’Algèbre abstraite à la Logique propositionnelle booléenne ; et celui de l’ « Expressionnisme », qui mène de l’Arithmétique au Calcul logique des prédicats, associée aux travaux de Frege. Mais plus profondément, par l’effet d’une lecture symptomale au plus près des dynamiques internes à ces processus, le présent travail décèle un lien transversal entre le contenu logique d’une part et l’Arithmétique comme ensemble des déterminations du nombre de l’autre. En suivant ce lien, qui s’avère le responsable de l’introduction de la catégorie de sens dans le cadre de la logique mathématisée, une théorie de l’expression formelle se dessine, définissant les conditions pour le développement d’une logique du sens. / This work aims at providing a new general interpretation of the logic that was born with the work of Gottlob Frege, in order to make explicit one of the most decisive conditions of contemporary philosophy: the one that concerns the relation of philosophy to formal practices and knowledge. Its initial hypothesis states that Frege’s primary and most constant project was that of building a logic of content. However, the intelligibility thus gained does not intend to unearth a new underlying unity of Frege’s thought; it rather aims at localising the real gaps within Frege’s formulations that have not been identified as such until now. Still, those gaps do not require to be filled, for Frege’s logic is indeed effective despite this indeterminacy. Rather than the gaps, it is this ungrounded effectiveness that needs to be explained. Our answer to this question is that the effectiveness of Frege’s logic as a logic of content comes from a certain relationship with Arithmetic; in fact, Frege’s logic is constructed on the template of Arithmetic, before it becomes capable of constructing Arithmetic in turn. The task then arises to characterise precisely, at this constitutive and non-foundational level, the nature of the relation between a logic of content as a specific form of logic in the framework of its mathematization, and Arithmetic as a particular mathematical domain. From the meticulous study of the constitution of the Fregean system, an idea can be drawn that constitutes the central argument of this thesis: the various mathematical or formalised logical systems rest upon mathematics only through an intermediary dimension consisting in the practice, the reflection and the elaboration of signs, where the circulations between these two contemporary domains of formal knowledge (mathematics and logic) are constructed and justified. From this point of view, we then lay out a detailed study of the rise of the two most significant projects for formalizing logic in the nineteenth century: Frege’s and Boole’s (and the Booleans’). In the space leading from mathematical practices to logical systematisations through semiotic functioning, two general schemes or semiotic formal regimes can be drawn: “Symbolic Abstraction”, leading from abstract Algebra to Boolean propositional logic; and “Expressionism”, leading from Arithmetic to Predicate Calculus, associated to Frege’s work. More deeply, our research reveals a deep connexion between logical content and Arithmetic (understood as the theory of integers), which horizontally crosses the different semiotic regimes. Following the multiple dimensions of this nexus – which is responsible for the introduction of the category of sense in the framework of mathematized logic – a formal theory of expression can be drawn, which defines the conditions for the actual development of a logic of sense.

Face aux nouveaux cadres législatifs ou environnementaux dans lesquels ils doivent évoluer, les systèmes industriels actuels sont, en plus d'être contraints par des exigences classiques de productivité et de cout, sujets au respect de nouvelles exigences relatives à la sûreté, la sécurité ou au développement durable notamment. Pour répondre à ces exigences et améliorer la maitrise des performances de ses systèmes, EDF souhaite faire évoluer sa démarche d'Optimisation de la Maintenance Basée sur la Fiabilité vers une nouvelle méthode. Cette méthode nécessite en autre la proposition d'une approche outillée permettant de quantifier a priori les programmes de maintenance (CMPQ) sur ses systèmes par rapport aux indicateurs de performance attendus (KPIs). Cet outillage fait l'objet de cette thèse financée dans le cadre du GIS 3SGS - projet DEPRADEM 2. Après avoir généralisé les besoins d'EDF en regard de la CMPQ, nous proposons une identification de la connaissance générique nécessaire pour évaluer les KPI. Afin d'aboutir à un outil permettant l'automatisation de ces études de CMPQ, cette connaissance générique est ensuite modélisée sur la base de deux langages : le langage semi-formel SysML capitalisant, par l'intermédiaire de différents diagrammes, la connaissance statique, interactionnelle et comportementale ; et le langage AltaRicaDF, supportant un modèle dynamique permettant d'évaluer les KPIs par simulation stochastique. La création de ce modèle dynamique à partir des différents diagrammes est basée sur un mapping entre les concepts d'intérêt des deux langages. La démarche dans sa globalité est validée à la CMPQ d'un cas d'étude fourni par EDF : le système ARE / To face with new legislatives and environmental contexts in which they have to operate, it is needed now that the industrials systems have to satisfy to many different requirements and constraints. Thus, these requirements are not only conventional ones such as availability and costs, but also emergent ones such as safety and sustainability. This report implies for the specific French company EDF (energy power supplier) to evolve from its usual approach of reliability centered maintenance (RCM) to a new approach. It is consisting mainly in developing a tool able to support the Complex Maintenance Programs Quantification (CMPQ). This Ph.D. is dealing with this the engineering and deployment of this tool in the frame of the GIS 3SGS - DEPRADEM 2 project. The first step of the work is to generalize EDF needs, then to propose a framework enabling to identify required generic knowledge needed to assess the Key Performances Indicators (KPIs) for supporting quantification. The next step is to model the generic knowledge in two complementary ways: a formalization of the static, interactional and behavioral knowledge based on different SysML diagrams; and a formalization of the dynamic and executable knowledge formalized by AltaRicaDF (ADF) language, allowing to perform stochastic simulation and to assess required KPIs. The path to elaborate dynamic executable vision from SysML diagrams is released by means of rules between each element of interest of both languages. All this approach/tool is applied to a specific EDF case study: the ARE system