O estatuto lexical das preposições sob e sobre

This paper describes the prepositions sob and sobre in the Functional Discourse Grammar framework (HENGEVELD; MACKENZIE, 2008) aiming at checking their lexical or grammatical status on the basis of classification criteria postulated by Keizer (2007). The following aspects point to their lexical status : (i) they consist of an Ascription Subact; (ii) they contain a specific content on the vertical axis signaling inferiority and superiority position in relation to a limit; (iii) they are not required by any predicate, but they are predicates by themselves, which require complementation by an argument playing Reference semantic function; (iv) they may be combined with de, em, para and por; which are genuine grammatical prepositions; and, finally, (v) they are not subjected to any phonological process of reduction and fusion.

Desenvolvimento de um instrumento multidimensional para avaliação de práticas de ensino no processo de aprendizagem

Pós-graduação em Engenharia Mecânica - FEG

Trajetórias de mudança dos predicados acabar, acontecer e começar sob perspectiva discursivo-funcional

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)

As construções verbais paratáticas: gramaticalização em italiano

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)

The SB-index and the HSB-index: efficient indices for spatial data warehouses

Spatial data warehouses (SDWs) allow for spatial analysis together with analytical multidimensional queries over huge volumes of data. The challenge is to retrieve data related to ad hoc spatial query windows according to spatial predicates, avoiding the high cost of joining large tables. Therefore, mechanisms to provide efficient query processing over SDWs are essential. In this paper, we propose two efficient indices for SDW: the SB-index and the HSB-index. The proposed indices share the following characteristics. They enable multidimensional queries with spatial predicate for SDW and also support predefined spatial hierarchies. Furthermore, they compute the spatial predicate and transform it into a conventional one, which can be evaluated together with other conventional predicates by accessing a star-join Bitmap index. While the SB-index has a sequential data structure, the HSB-index uses a hierarchical data structure to enable spatial objects clustering and a specialized buffer-pool to decrease the number of disk accesses. The advantages of the SB-index and the HSB-index over the DBMS resources for SDW indexing (i.e. star-join computation and materialized views) were investigated through performance tests, which issued roll-up operations extended with containment and intersection range queries. The performance results showed that improvements ranged from 68% up to 99% over both the star-join computation and the materialized view. Furthermore, the proposed indices proved to be very compact, adding only less than 1% to the storage requirements. Therefore, both the SB-index and the HSB-index are excellent choices for SDW indexing. Choosing between the SB-index and the HSB-index mainly depends on the query selectivity of spatial predicates. While low query selectivity benefits the HSB-index, the SB-index provides better performance for higher query selectivity.

Theoretical and implementation aspects in the mechanization of the metatheory of programming languages

Interactive theorem provers are tools designed for the certification of formal proofs developed by means of man-machine collaboration. Formal proofs obtained in this way cover a large variety of logical theories, ranging from the branches of mainstream mathematics, to the field of software verification. The border between these two worlds is marked by results in theoretical computer science and proofs related to the metatheory of programming languages. This last field, which is an obvious application of interactive theorem proving, poses nonetheless a serious challenge to the users of such tools, due both to the particularly structured way in which these proofs are constructed, and to difficulties related to the management of notions typical of programming languages like variable binding. This thesis is composed of two parts, discussing our experience in the development of the Matita interactive theorem prover and its use in the mechanization of the metatheory of programming languages. More specifically, part I covers: - the results of our effort in providing a better framework for the development of tactics for Matita, in order to make their implementation and debugging easier, also resulting in a much clearer code; - a discussion of the implementation of two tactics, providing infrastructure for the unification of constructor forms and the inversion of inductive predicates; we point out interactions between induction and inversion and provide an advancement over the state of the art. In the second part of the thesis, we focus on aspects related to the formalization of programming languages. We describe two works of ours: - a discussion of basic issues we encountered in our formalizations of part 1A of the Poplmark challenge, where we apply the extended inversion principles we implemented for Matita; - a formalization of an algebraic logical framework, posing more complex challenges, including multiple binding and a form of hereditary substitution; this work adopts, for the encoding of binding, an extension of Masahiko Sato's canonical locally named representation we designed during our visit to the Laboratory for Foundations of Computer Science at the University of Edinburgh, under the supervision of Randy Pollack.

A FIREWALL MODEL OF FILE SYSTEM SECURITY

File system security is fundamental to the security of UNIX and Linux systems since in these systems almost everything is in the form of a file. To protect the system files and other sensitive user files from unauthorized accesses, certain security schemes are chosen and used by different organizations in their computer systems. A file system security model provides a formal description of a protection system. Each security model is associated with specified security policies which focus on one or more of the security principles: confidentiality, integrity and availability. The security policy is not only about “who” can access an object, but also about “how” a subject can access an object. To enforce the security policies, each access request is checked against the specified policies to decide whether it is allowed or rejected. The current protection schemes in UNIX/Linux systems focus on the access control. Besides the basic access control scheme of the system itself, which includes permission bits, setuid and seteuid mechanism and the root, there are other protection models, such as Capabilities, Domain Type Enforcement (DTE) and Role-Based Access Control (RBAC), supported and used in certain organizations. These models protect the confidentiality of the data directly. The integrity of the data is protected indirectly by only allowing trusted users to operate on the objects. The access control decisions of these models depend on either the identity of the user or the attributes of the process the user can execute, and the attributes of the objects. Adoption of these sophisticated models has been slow; this is likely due to the enormous complexity of specifying controls over a large file system and the need for system administrators to learn a new paradigm for file protection. We propose a new security model: file system firewall. It is an adoption of the familiar network firewall protection model, used to control the data that flows between networked computers, toward file system protection. This model can support decisions of access control based on any system generated attributes about the access requests, e.g., time of day. The access control decisions are not on one entity, such as the account in traditional discretionary access control or the domain name in DTE. In file system firewall, the access decisions are made upon situations on multiple entities. A situation is programmable with predicates on the attributes of subject, object and the system. File system firewall specifies the appropriate actions on these situations. We implemented the prototype of file system firewall on SUSE Linux. Preliminary results of performance tests on the prototype indicate that the runtime overhead is acceptable. We compared file system firewall with TE in SELinux to show that firewall model can accommodate many other access control models. Finally, we show the ease of use of firewall model. When firewall system is restricted to specified part of the system, all the other resources are not affected. This enables a relatively smooth adoption. This fact and that it is a familiar model to system administrators will facilitate adoption and correct use. The user study we conducted on traditional UNIX access control, SELinux and file system firewall confirmed that. The beginner users found it easier to use and faster to learn then traditional UNIX access control scheme and SELinux.

Unfolding Feasible Arithmetic and Weak Truth

In this paper we continue Feferman’s unfolding program initiated in (Feferman, vol. 6 of Lecture Notes in Logic, 1996) which uses the concept of the unfolding U(S) of a schematic system S in order to describe those operations, predicates and principles concerning them, which are implicit in the acceptance of S. The program has been carried through for a schematic system of non-finitist arithmetic NFA in Feferman and Strahm (Ann Pure Appl Log, 104(1–3):75–96, 2000) and for a system FA (with and without Bar rule) in Feferman and Strahm (Rev Symb Log, 3(4):665–689, 2010). The present contribution elucidates the concept of unfolding for a basic schematic system FEA of feasible arithmetic. Apart from the operational unfolding U0(FEA) of FEA, we study two full unfolding notions, namely the predicate unfolding U(FEA) and a more general truth unfolding UT(FEA) of FEA, the latter making use of a truth predicate added to the language of the operational unfolding. The main results obtained are that the provably convergent functions on binary words for all three unfolding systems are precisely those being computable in polynomial time. The upper bound computations make essential use of a specific theory of truth TPT over combinatory logic, which has recently been introduced in Eberhard and Strahm (Bull Symb Log, 18(3):474–475, 2012) and Eberhard (A feasible theory of truth over combinatory logic, 2014) and whose involved proof-theoretic analysis is due to Eberhard (A feasible theory of truth over combinatory logic, 2014). The results of this paper were first announced in (Eberhard and Strahm, Bull Symb Log 18(3):474–475, 2012).

Applicative theories for logarithmic complexity classes

We present applicative theories of words corresponding to weak, and especially logarithmic, complexity classes. The theories for the logarithmic hierarchy and alternating logarithmic time formalise function algebras with concatenation recursion as main principle. We present two theories for logarithmic space where the first formalises a new two-sorted algebra which is very similar to Cook and Bellantoni's famous two-sorted algebra B for polynomial time [4]. The second theory describes logarithmic space by formalising concatenation- and sharply bounded recursion. All theories contain the predicates WW representing words, and VV representing temporary inaccessible words. They are inspired by Cantini's theories [6] formalising B.

Inversion, Obviation, and Animacy in Native Languages of the Americas: Elements for a Cross-linguistic Survey

Native languages of the Americas whose predicate and clause structure reflect nominal hierarchies show an interesting range of structural diversity not only with respect to morphological makeup of their predicates and arguments but also with respect to the factors governing obviation status. The present article maps part of such diversity. The sample surveyed here includes languages with some sort of nonlocal (third person acting on third person) direction-marking system.

Simplicidad de Dios y pluralidad de nombres divinos : ¿una contradicción?

En el siglo XIII, ningún autor negaba la absoluta simplicidad de Dios. Sin embargo, se utilizaban múltiples nombres para hablar de lo divino. ¿Se pueden considerar verdaderos todos esos predicados, sin que ello implique concebir una multiplicidad real en la esencia divina? Este trabajo intenta mostrar, bajo la guía de Tomás de Aquino, que la pluralidad de atributos divinos no contradice la simplicidad divina y que, sin entenderlos como sinónimos, dichos nombres constituyen predicaciones verdaderas in divinis.

Predicados, propiedades y condiciones de aplicación

En el presente artículo examinamos la relación entre predicados y propiedades. Por un lado, procuramos mostrar que la concepción de acuerdo con la cual la función primaria de predicados es la de denotar propiedades es insatisfactoria. Por otro lado, distinguimos entre el criterio de uso de predicados y su condición de aplicación, i. e. la condición que un objeto debe satisfacer para que sea correcto aplicar el predicado a él. Defendemos que propiedades se relacionan con predicados en la medida en que la condición de aplicación de un predicado es la instanciación de una propiedad

Predicados, propiedades y condiciones de aplicación

En el presente artículo examinamos la relación entre predicados y propiedades. Por un lado, procuramos mostrar que la concepción de acuerdo con la cual la función primaria de predicados es la de denotar propiedades es insatisfactoria. Por otro lado, distinguimos entre el criterio de uso de predicados y su condición de aplicación, i. e. la condición que un objeto debe satisfacer para que sea correcto aplicar el predicado a él. Defendemos que propiedades se relacionan con predicados en la medida en que la condición de aplicación de un predicado es la instanciación de una propiedad

Predicados, propiedades y condiciones de aplicación

En el presente artículo examinamos la relación entre predicados y propiedades. Por un lado, procuramos mostrar que la concepción de acuerdo con la cual la función primaria de predicados es la de denotar propiedades es insatisfactoria. Por otro lado, distinguimos entre el criterio de uso de predicados y su condición de aplicación, i. e. la condición que un objeto debe satisfacer para que sea correcto aplicar el predicado a él. Defendemos que propiedades se relacionan con predicados en la medida en que la condición de aplicación de un predicado es la instanciación de una propiedad

Automatic Inference of Determinacy and Mutual Exclusion for Logic Programs Using Mode and Type Analyses

We propose an analysis for detecting procedures and goals that are deterministic (i.e., that produce at most one solution at most once),or predicates whose clause tests are mutually exclusive (which implies that at most one of their clauses will succeed) even if they are not deterministic. The analysis takes advantage of the pruning operator in order to improve the detection of mutual exclusion and determinacy. It also supports arithmetic equations and disequations, as well as equations and disequations on terms,for which we give a complete satisfiability testing algorithm, w.r.t. available type information. Information about determinacy can be used for program debugging and optimization, resource consumption and granularity control, abstraction carrying code, etc. We have implemented the analysis and integrated it in the CiaoPP system, which also infers automatically the mode and type information that our analysis takes as input. Experiments performed on this implementation show that the analysis is fairly accurate and efficient.