Assessing the eco-efficiency of a composite processing industry: evaluation and quantification of potential improvements’

In this study, an attempt was made in order to measure and evaluate the eco-efficiency performance of a pultruded composite processing company. For this purpose the recommendations of World Business Council for Sustainable Development (WCSD) and the directives of ISO 14301 standard were followed and applied. The main general indicators of eco-efficiency, as well as the specific indicators, were defined and determined. With basis on indicators’ figures, the value profile, the environmental profile, and the pertinent ecoefficiency’s ratios were established and analyzed. In order to evaluate potential improvements on company eco-performance, new indicators values and eco-efficiency ratios were estimated taking into account the implementation of new proceedings and procedures, both in upstream and downstream of the production process, namely: a) Adoption of new heating system for pultrusion die in the manufacturing process, more effective and with minor heat losses; c) Recycling approach, with partial waste reuse of scrap material derived from manufacturing, cutting and assembly processes of GFRP profiles. These features lead to significant improvements on the sequent assessed eco-efficiency ratios of the present case study, yielding to a more sustainable product and manufacturing process of pultruded GFRP profiles.

Eco-efficiency approaches towards a sustainable composite materials manufacturing industry’

In this study the potential eco-efficiency performance of a pultrusion manufacturing company was assessed. Indicators values and eco-efficiency ratios were estimated taking into account the implementation of new proceedings and procedures in the production process of glass fibre reinforced polymers (GFRP) pultrusion profiles. Two different approaches were foreseen: 1)Adoption of a new heating system for pultrusion die in the manufacturing process, more effective and with minor heat losses; and 2) Recycling approach, with partial waste reuse of scrap material derived from manufacturing, cutting and assembly processes of GFRP profiles. These features lead to significant improvements on the sequent assessed eco-efficiency ratios of the present case study, yielding to a more sustainable product and manufacturing process of pultruded GFRP profiles.

A case study on the improvement of eco-efficiency ratios: application to a composite processing industry

The World Business Council for Sustainable Development (WBCSD) defines Eco-Efficiency as follows: ‘Eco- Efficiency is achieved by the delivery of competitively priced-goods and services that satisfy human needs and bring quality of life, while progressively reducing ecological impacts and resource intensity throughout the life-cycle to a level at least in line with the earth’s estimated carrying capacity’. Eco-Efficiency is under this point of view a key concept for sustainable development, bringing together economic and ecological progress. Measuring the Eco-Efficiency of a company, factory or business, is a complex process that involves the measurement and control of several and relevant parameters or indicators, globally applied to all companies in general, or specific according to the nature and specificities of the business itself. In this study, an attempt was made in order to measure and evaluate the eco-efficiency of a pultruded composite processing company. For this purpose the recommendations of WBCSD [1] and the directives of ISO 14301 standard [2] were followed and applied. The analysis was restricted to the main business branch of the company: the production and sale of standard GFRP pultrusion profiles. The main general indicators of eco-efficiency, as well as the specific indicators, were defined and determined according to ISO 14031 recommendations. With basis on indicators’ figures, the value profile, the environmental profile, and the pertinent eco-efficiency’s ratios were established and analyzed. In order to evaluate potential improvements on company eco-performance, new indicators values and ecoefficiency ratios were estimated taking into account the implementation of new proceedings and procedures, both in upstream and downstream of the production process, namely: a) Adoption of new heating system for pultrusion die in the manufacturing process, more effective and with minor heat losses; b) Implementation of new software for stock management (raw materials and final products) that minimize production failures and delivery delays to final consumer; c) Recycling approach, with partial waste reuse of scrap material derived from manufacturing, cutting and assembly processes of GFRP profiles. In particular, the last approach seems to significantly improve the eco-efficient performance of the company. Currently, by-products and wastes generated in the manufacturing process of GFRP profiles are landfilled, with supplementary added costs to this company traduced by transport of scrap, landfill taxes and required test analysis to waste materials. However, mechanical recycling of GFRP waste materials, with reduction to powdered and fibrous particulates, constitutes a recycling process that can be easily attained on heavy-duty cutting mills. The posterior reuse of obtained recyclates, either into a close-looping process, as filler replacement of resin matrix of GFRP profiles, or as reinforcement of other composite materials produced by the company, will drive to both costs reduction in raw materials and landfill process, and minimization of waste landfill. These features lead to significant improvements on the sequent assessed eco-efficiency ratios of the present case study, yielding to a more sustainable product and manufacturing process of pultruded GFRP profiles.

Sustainability Improvement of a composite materials’ industry through recycling and re-engineering process approaches

Recent Advances in Mechanics and Materials in Design

Extending relAPS to first order logic

RelAPS is an interactive system assisting in proving relation-algebraic theorems. The aim of the system is to provide an environment where a user can perform a relation-algebraic proof similar to doing it using pencil and paper. The previous version of RelAPS accepts only Horn-formulas. To extend the system to first order logic, we have defined and implemented a new language based on theory of allegories as well as a new calculus. The language has two different kinds of terms; object terms and relational terms, where object terms are built from object constant symbols and object variables, and relational terms from typed relational constant symbols, typed relational variables, typed operation symbols and the regular operations available in any allegory. The calculus is a mixture of natural deduction and the sequent calculus. It is formulated in a sequent style but with exactly one formula on the right-hand side. We have shown soundness and completeness of this new logic which verifies that the underlying proof system of RelAPS is working correctly.

On the EA-style integrated processing of self-contained mathematical texts

A sound and complete first-order goal-oriented sequent-type calculus is developed with ``large-block'' inference rules. In particular, the calculus contains formal analogues of such natural proof-search techniques as handling definitions and applying auxiliary propositions.

Evidence Algorithm and Processing Formalized Mathematical Texts

The goal of a research programme Evidence Algorithm is a development of an open system of automated proving that is able to accumulate mathematical knowledge and to prove theorems in a context of a self-contained mathematical text. By now, the first version of such a system called a System for Automated Deduction, SAD, is implemented in software. The system SAD possesses the following main features: mathematical texts are formalized using a specific formal language that is close to a natural language of mathematical publications; a proof search is based on special sequent-type calculi formalizing natural reasoning style, such as application of definitions and auxiliary propositions. These calculi also admit a separation of equality handling from deduction that gives an opportunity to integrate logical reasoning with symbolic calculation.

Evolução da paisagem do baixo curso do rio de Piranhas-Assu (1988-2024): uso de autômatos celulares em modelo dinâmico espacial para simulação de cenários futuros

The lower course of Piranhas-Assu river, located in the north coast of Rio Grande do Norte, Brazil, arouses a keen interest as a study field, once it concentrates, besides petroleum and gas exploration, activities related to shrimp culture, salt and horticulture, factors that also deserve special attention. Thus, the awareness of the study field environmental stage demands studies from researchers and discernment from society, as a way of understanding the inter-relation between environment and men. Therefore, this work attempts at understanding and studying the dynamics of land use in the lower course of Piranhas-Assu river, through a multitemporal analysis of present and past, accomplishing future projections through simulation models. The work is divided in stages that include the research, analysis, interpretation of results, and the generation of simulation models, to analyze the landscape tendencies, making possible to identify indicators which cause such changes in the lower course of the river. From Geographical Database, the necessary exploratory analyses were accomplished to the following items: land use evolution, natural and environmental vulnerability, multiple geodiversity indexes, and preparation of the data to be used in the simulation model. Later, the construction of the landscape simulation model was conducted. Sequentially, simulations of future sceneries were accomplished through the execution of the model in a specific software environment. Last, the analyses of landscape tendencies in the study field were carried out. The lower course of Piranhas-Assu River didn't show any intense dynamics in landscape changing, once in the period taken into account (from 1988 to 2004) class stability proved to be superior to its transformations. Activities related to agriculture and livestock are the ones that influence, mostly, the landscape dynamics. The production of sea shrimp and petroleum also infers in the landscape, although in smaller proportion. INCRA s public policies excessively determined the dynamics of the landscape in the lower course of Piranhas-Assu River, RN. In respect to its natural vulnerability, the lower course of Piranhas-Assu River, RN, features more vulnerable than stable areas. The landscape simulation, in the first taken period (2004-2009), indicated considerable increases and decreases of antropic activities, if compared to its sequent periods (2009-2014, 2014-2019 and 2019-2024). The simulation, in a wider analysis, showed that the determining factors for the space mobility of antropic activities, in the focused area, are related to the pre-existence of communities with agricultural capability and to the existence of access routes and drainage. Considering the area that features fixed and mobile dunes, located in Porto do Mangue district, we recommend its conversion into a conservation area

Características morfológicas da região epididimária do pombo doméstico (Columba livia, L.)

A região epididimária do pombo doméstico compreende a parte principal da rede testicular, os dúctulos eferentes do testículo e o ducto epididimário. Os canais epiteliais da rede testicular são contínuos com o segmento extratesticular da rede, o qual, por sua vez, é seqüente com os dúctulos eferentes proximais e distais e, finalmente, o ducto epididimário se forma em continuidade aos eferentes distais. O epitélio de revestimento deste sistema tubular extratesticular é cúbico simples na rede testicular e pseudo-estratificado colunar nos outros ductos da região epididimária, com células ciliadas e não-ciliadas presentes principalmente nos dúctulos eferentes. As características ultra-estruturais das células epiteliais dos túbulos da região epididimária do pombo, com base comparativa, permitiram inferir que a reabsorção de fluido seminífero parece ser a função principal dessas células, embora outros papéis citofisiológicos foram também propostos, tais como: endocitose adsorptiva, ciliogênese, e possivelmente secreção apócrina nas células não-ciliadas escuras.

Sobre quantificadores: uma formalização do quantificador 'quase sempre'

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

Evaluation of indexed language used in collective catalogues of university libraries: a socio-cognitive study using verbal protocol

The use of indexing language in university libraries collective catalogs and the socio-cognitive context of indexing and users were evaluated. The methodology consisted of a diagnostic study elaboration of the functioning and treatment procedures of the indexing information from nine libraries of the UNESP Network, representing the Civil Engineering, Pedagogy and Dentistry areas from a data collection using the Verbal Protocol introspective technique in the Individual and Group forms. The study conducted a reflection upon the statements issued by the seventy-two participating individuals whose the results revealed unsatisfactory results about the use of the Subject Headings List of the BIBLIODATA Network, indexing language utilizing by the UNESP Libraries Network, Brazil, in the representation and in the information retrieval process in the ATHENA catalog, about the sequent aspects of the language: lack of specialized vocabulary as well as updated; lack of remissives and of specific headings, and others. We have concluded that the adequate use of indexing languages of specialized scientific areas becomes by means of evaluation as to updating, specificity and compatibility in order to meet the needs of indexing and information retrieval.

Certificates for Incremental Type Checking

The central topic of this thesis is the study of algorithms for type checking, both from the programming language and from the proof-theoretic point of view. A type checking algorithm takes a program or a proof, represented as a syntactical object, and checks its validity with respect to a specification or a statement. It is a central piece of compilers and proof assistants. We postulate that since type checkers are at the interface between proof theory and program theory, their study can let these two fields mutually enrich each other. We argue by two main instances: first, starting from the problem of proof reuse, we develop an incremental type checker; secondly, starting from a type checking program, we evidence a novel correspondence between natural deduction and the sequent calculus.

Proof theory of quantified modal logics

We introduce labelled sequent calculi for indexed modal logics. We prove that the structural rules of weakening and contraction are height-preserving admissible, that all rules are invertible, and that cut is admissible. Then we prove that each calculus introduced is sound and complete with respect to the appropriate class of transition frames.

A syntactic realization theorem for justification logics

Justification logics are refinements of modal logics where modalities are replaced by justification terms. They are connected to modal logics via so-called realization theorems. We present a syntactic proof of a single realization theorem that uniformly connects all the normal modal logics formed from the axioms \$mathsfd\$, \$mathsft\$, \$mathsfb\$, \$mathsf4\$, and \$mathsf5\$ with their justification counterparts. The proof employs cut-free nested sequent systems together with Fitting's realization merging technique. We further strengthen the realization theorem for \$mathsfKB5\$ and \$mathsfS5\$ by showing that the positive introspection operator is superfluous.

Canonical proof nets for classical logic

Proof nets provide abstract counterparts to sequent proofs modulo rule permutations; the idea being that if two proofs have the same underlying proof-net, they are in essence the same proof. Providing a convincing proof-net counterpart to proofs in the classical sequent calculus is thus an important step in understanding classical sequent calculus proofs. By convincing, we mean that (a) there should be a canonical function from sequent proofs to proof nets, (b) it should be possible to check the correctness of a net in polynomial time, (c) every correct net should be obtainable from a sequent calculus proof, and (d) there should be a cut-elimination procedure which preserves correctness. Previous attempts to give proof-net-like objects for propositional classical logic have failed at least one of the above conditions. In Richard McKinley (2010) [22], the author presented a calculus of proof nets (expansion nets) satisfying (a) and (b); the paper defined a sequent calculus corresponding to expansion nets but gave no explicit demonstration of (c). That sequent calculus, called LK∗ in this paper, is a novel one-sided sequent calculus with both additively and multiplicatively formulated disjunction rules. In this paper (a self-contained extended version of Richard McKinley (2010) [22]), we give a full proof of (c) for expansion nets with respect to LK∗, and in addition give a cut-elimination procedure internal to expansion nets – this makes expansion nets the first notion of proof-net for classical logic satisfying all four criteria.