of doctoral thesis Study of Arithmetical Structures and Theories with Regard to Representative and Descriptive Analysis Petr Glivický We are motivated by a problem of understanding relations between local and global properties of an operation o in a structure of the form B, o , with regard to an application for the study of models B, · of Peano arithmetic, where B is a model of Presburger arithmetic. We are particularly interested in a dependency problem, which we formulate as the problem of describing the dependency closure iclO (E) = {d ∈ Bn ; (∀o, o ∈ O)(o E = o E ⇒ o(d) = o (d))}, where B is a structure, O a set of n-ary operations on B, and E ⊆ Bn. We show, that this problem can be reduced to a definability question in certain expansion of B. In particular, if B is a saturated model of Presburger arithmetic, and O is the set of all (saturated) Peano products on B, we prove that, for a ∈ B, iclO ({a}×B) is the smallest possible, i.e. it contains just those pairs (d0, d1) ∈ B2 for which at least one of di equals p(a), for some polynomial p ∈ Q[x]. We show that the presented problematics is closely connected to the descriptive analysis of linear theories. That are theories, models of which are - up to a change of the language - certain discretely ordered modules over specific discretely ordered...

Submitted by Renata Lopes (renatasil82@gmail.com) on 2016-04-28T15:47:51Z No. of bitstreams: 1 igordeoliveiracosta.pdf: 2715764 bytes, checksum: c8160cddc86f647724c428607a8341c6 (MD5) / Approved for entry into archive by Adriana Oliveira (adriana.oliveira@ufjf.edu.br) on 2016-05-02T01:02:51Z (GMT) No. of bitstreams: 1 igordeoliveiracosta.pdf: 2715764 bytes, checksum: c8160cddc86f647724c428607a8341c6 (MD5) / Made available in DSpace on 2016-05-02T01:02:51Z (GMT). No. of bitstreams: 1 igordeoliveiracosta.pdf: 2715764 bytes, checksum: c8160cddc86f647724c428607a8341c6 (MD5) Previous issue date: 2015-11-30 / CAPES - Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / Este trabalho, de viés sociocognitivista e construcionista, tem como objeto analítico um nódulo da rede de Construções Quantificadoras Mórficas Sufixais, reconhecida como uma estratégia morfológica de evocação da noção de coletividade na Língua Portuguesa, como ilustram os exemplos seguir: (i) {XN-ADA} (“Com AXE vou pegar a mulherada.”); (ii) {XN-ARADA} (“No meio daquela brinquedarada toda tinha um brinquedo que, pelo menos o que eu acho hoje, era da família daqueles patinhos de borracha [...]”); (iii) {XN-AIADA} (“Após a cachaçaiada é sempre bom beber bastante liquido [...]”). Tal estudo de caso serve de estofo a um objeto teórico mais amplo, qual seja a proposição de um trato construcionista da morfologia derivacional (MIRANDA, 2013; RHODES, 1992). A Gramática das Construções Cognitiva (GOLDBERG, 1995, 2006; BOAS, 2013), entendida como um Modelo Baseado no Uso (BYBEE, 2010; CROFT E CRUSE, 2004), fornece o aparato teórico central a este estudo. Da premissa sociocognitivista que reivindica a centralidade da experiência na constituição da linguagem deriva outro fundamento crucial à sustentação das análises, qual seja a proposição de convergência entre o escopo teórico construcionista e a Semântica de Frames (FILLMORE, 1977, 2009[1982], 1985; PETRUCK, 1996; RUPENHOFER et al., 2010). Dado o relevo do uso no modelo teórico-analítico eleito, acolhe-se, em termos metodológicos, uma Linguística Cognitiva baseada em corpus (FILLMORE, 2008[1992]; MCENERY, XIAO E TONO, 2006), o que implica o uso de corpora eletrônicos e ferramentas computacionais na análise dos dados. As análises apontam, dentre outras coisas, para a consistência de um trato construcionista da morfologia derivacional, bem como para a riqueza linguística e cognitiva das construções estudadas. Os construtos, instituídos pelo esquema imagético COLEÇÃO (JOHNSON, 2005; CLAUSNER E CROFT, 1999), tem na evocação dos frames Quantidade e Desejabilidade a sua constituição semântica, apresentando-se como estratégias de quantificação e avaliação pertinentes a gêneros mais distensos da Língua Portuguesa. / This paper analyses, in a cognitive and constructionist perspective, a node of the vast network of Suffixal Morphic Quantifying Constructions, recognized as a morphological strategy evocation of the notion of collectivity in Portuguese, as illustrated with the following examples: (i) {XN-ADA} (“Com AXE vou pegar a mulherada.”); (ii) {XN-ARADA} (“No meio daquela brinquedarada toda tinha um brinquedo que, pelo menos o que eu acho hoje, era da família daqueles patinhos de borracha [...]”); (iii) {XN-AIADA} (“Após a cachaçaiada é sempre bom beber bastante liquido [...]”). This case study supports a broader theoretical object, the proposition for a constructionist approach to derivational morphology (MIRANDA, 2013; RHODES, 1992). Cognitive Construction Grammar (GOLDBERG, 1995, 2006; BOAS, 2013), a Used-based Model of Language (BYBEE, 2010; CROFT AND CRUSE, 2004), provides the central theoretical apparatus to this study. The Cognitive Linguistics premise of claiming the centrality of experience in the creation of language grants another crucial support to this analysis, which is the proposition of convergence between the constructionist approach and Frame Semantics (FILLMORE, 1977, 2009[1982], 1985; PETRUCK, 1996; RUPENHOFER et al., 2010). Given the amount of use in the theoretical and analytical model adopted, corpus-based Cognitive Linguistics (FILLMORE, 2008[1992]; MCENERY, XIAO AND TONO, 2006) was the methodology chosen. It implies the use of electronic corpora, computational tools and quantitative analysis of the data in terms of type frequency and token frequency (BYBEE, 2010; GOLDBERG, 1995). The analysis points out, among other things, to the consistency of a constructionist approach for derivational morphology, as well as the cognitive and linguistic richness of the constructional patterns under investigation. The constructs, established by the COLLECTION image schema (JOHNSON, 2005; CLAUSNER AND CROFT, 1999), evoke the Quantity and Desirability frames, presenting itself as quantifying and evaluation strategies relevant to distended genres of Portuguese.

No description available.

Text in English / This study explores the syntax of the substantive phrase, more especially substantive phrase composed of more than one qualificative, in Sesotho. Adopting interviews, questionnaires and documents, the study seeks to investigate the syntactic sequence of qualificatives, their relation to the modified head word and influence of such ordering pattern in the phrase. Structurally, qualificatives comprise two components, namely the qualificative concord and stem. The qualificative serves to give varied information about the implicit or explicit substantive resulting in seven types of qualificatives in Sesotho, be they the Adjective, Demonstrative, Enumerative, Interrogative, Possessive, Quantifier and Relative. From the Minimalist perspective, the qualificative is recursive. The study established a maximum of five qualificatives in a single phrase. The number is generally achieved by recurrence of the Adjective, the Possessive and the Relative up to a maximum of four of the same qualificative in a single phrase. It is observed that the recurrence of the Demonstrative, Interrogative, Enumerative and Quantifier is proscribed in Sesotho. Regarding the ordering of qualificatives, it is also observed that the Demonstrative, Interrogative, Quantifier and Possessive mostly occupy the position closer to the substantive while the Adjective, Enumerative, Possessive and Quantifier mostly occur in the medial position. The Possessive and Relative occur in the outer-border position of the phrase. Such a sequence is influenced by several factors including focus, emphasis, the nature of the relationship between the head word and the dependent element, the syntactic complexity of the qualificative and the knowledge shared by both the speaker and the hearer about the qualified substantive. It can, therefore, be concluded that there are no strict rules of occurrence of the qualificatives in Sesotho. / African Languages / D. Litt. et Phil. (African Languages)

Simple counting quantifiers that can be used to compare the number of role successors of an individual or the cardinality of a concept with a fixed natural number have been employed in Description Logics (DLs) for more than two decades under the respective names of number restrictions and cardinality restrictions on concepts. Recently, we have considerably extended the expressivity of such quantifiers by allowing to impose set and cardinality constraints formulated in the quantifier-free fragment of Boolean Algebra with Presburger Arithmetic (QFBAPA) on sets of role successors and concepts, respectively. We were able to prove that this extension does not increase the complexity of reasoning. In the present paper, we investigate the expressive power of the DLs obtained in this way, using appropriate bisimulation characterizations and 0–1 laws as tools to differentiate between the expressiveness of different logics. In particular, we show that, in contrast to most classical DLs, these logics are no longer expressible in first-order predicate logic (FOL), and we characterize their first-order fragments. In most of our previous work on DLs with QFBAPA-based set and cardinality constraints we have employed finiteness restrictions on interpretations to ensure that the obtained sets are finite, as required by the standard semantics for QFBAPA. Here we dispense with these restrictions to ease the comparison with classical DLs, where one usually considers arbitrary models rather than finite ones, easier. It turns out that doing so does not change the complexity of reasoning.

We introduce a new description logic that extends the well-known logic ALCQ by allowing the statement of constraints on role successors that are more general than the qualified number restrictions of ALCQ. To formulate these constraints, we use the quantifier-free fragment of Boolean Algebra with Presburger Arithmetic (QFBAPA), in which one can express Boolean combinations of set constraints and numerical constraints on the cardinalities of sets. Though our new logic is considerably more expressive than ALCQ, we are able to show that the complexity of reasoning in it is the same as in ALCQ, both without and with TBoxes. / The first version of this report was put online on April 6, 2017. The current version, containing more information on related work, was put online on July 13, 2017. This is an extended version of a paper published in the proceedings of FroCoS 2017.

Cette thèse présente un algorithme qui élimine les racines carrées et les divi- sions dans des programmes sans boucles, utilisés dans des systèmes embarqués, tout en préservant la sémantique. L'élimination de ces opérations permet d'éviter les erreurs d'arrondis à l'exécution, ces erreurs d'arrondis pouvant entraîner un comportement complètement inattendu de la part du programme. Cette trans- formation respecte les contraintes du code embarqué, en particulier la nécessité pour le programme produit de s'exécuter en mémoire fixe. Cette transformation utilise deux algorithmes fondamentaux développés dans cette thèse. Le premier permet d'éliminer les racines carrées et les divisions des expressions booléennes contenant des comparaisons d'expressions arithmétiques. Le second est un algo- rithme qui résout un problème d'anti-unification particulier, que nous appelons anti-unification contrainte. Cette transformation de programme est définie et prou- vée dans l'assistant de preuves PVS. Elle est aussi implantée comme une stratégie de ce système. L'anti-unification contrainte est aussi utilisée pour étendre la transformation à des programmes contenant des fonctions. Elle permet ainsi d'éliminer les racines carrées et les divisions de spécifications écrites en PVS. La robustesse de cette méthode est mise en valeur par un exemple conséquent: l'élimination des racines carrées et des divisions dans un programme de détection des conflits aériens.

Un problème de géométrie algébrique réelle s'exprime sous forme d’un système d’équations et d’inéquations polynomiales, dont l’ensemble des solutions est un ensemble semi-algébrique. L'objectif de cette thèse est de montrer comment les algorithmes de ce domaine peuvent être décrits formellement dans le langage du système de preuve Coq.Un premier résultat est la définition formelle et la certification de l’algorithme de transformation de Newton présentée dans la thèse d'A. Bostan. Ce travail fait intervenir non seulement des polynômes, mais également des séries formelles tronquées. Un deuxième résultat est la description d'un type de donnée représentant les ensembles semi-algébriques. Un ensemble semialgébrique est représenté par une formule logique du premier ordre basée sur des comparaisons entre expressions polynomiales multivariées. Pour ce type de données, nous montrons comment obtenir les différentes opérations ensemblistes et allons jusqu'à décrire les fonctions semi-algébriques. Pour toutes ces étapes, nous fournissons des preuves formelles vérifiées à l'aide de Coq. Enfin, nous montrons également comment la continuité des fonctions semi-algébrique peut être décrite, mais sans en fournir une preuve formelle complète. / A real algebraic geometry problem is expressed as a system of polynomial equations and inequalities, and the set of solutions are semi-algebraic sets. The objective of this thesis is to show how the algorithms of this domain can be formally described in the language of the Coq proof system. A first result is the formal definition and certification of the Newton transformation algorithm presented in A. Bostan's thesis. This work involves not only polynomials, but also truncated formal series. A second result is the description of a data type representing semi-algebraic sets. A semi-algebraic set is represented by a first-order logical formula based on comparisons between multivariate polynomial expressions. For this type of data, we show how to obtain the different set operations all the way to describing semialgebraic functions. For all these steps, we provide formal proofs verified with Coq. Finally, we also show how the continuity of semi-algebraic functions can be described, but without providing a fully formalized proof.