Curry-Howard for sequent calculus at last!

This paper tries to remove what seems to be the remaining stumbling blocks in the way to a full understanding of the Curry-Howard isomorphism for sequent calculus, namely the questions: What do variables in proof terms stand for? What is co-control and a co-continuation? How to define the dual of Parigot's mu-operator so that it is a co-control operator? Answering these questions leads to the interpretation that sequent calculus is a formal vector notation with first-class co-control. But this is just the "internal" interpretation, which has to be developed simultaneously with, and is justified by, an "external" one, offered by natural deduction: the sequent calculus corresponds to a bi-directional, agnostic (w.r.t. the call strategy), computational lambda-calculus. Next, the duality between control and co-control is studied and proved in the context of classical logic, where one discovers that the classical sequent calculus has a distortion towards control, and that sequent calculus is the de Morgan dual of natural deduction.

Field oriented control of an axial flux permanent magnet synchronous motor for traction solutions

Electric Vehicles (EVs) are increasingly used nowadays, and different powertrain solutions can be adopted. This paper describes the control system of an axial flux Permanent Magnet Synchronous Motor (PMSM) for EVs powertrain. It is described the implemented Field Oriented Control (FOC) algorithm and the Space Vector Modulation (SVM) technique. Also, the mathematical model of the PMSM is presented. Both, simulation and experimental, results with different types of mechanical load are presented. The experimental results were obtained using a laboratory test bench. The obtained results are discussed.

Companies' OHS internal structures: Types and theoretical foundations

An organization manages to regulate, standardize and optimize its operations in a way that places health and safety first by considering Health, Safety, Environment and Ergonomics (HSEE). In order to provide a theoretical foundation for Companies’ Occupational Health and Safety Internal Structures (COHSIS) allowing the focus on safety, COHSIS and its fundamentals were reviewed and described based on a brief literature review, which have included both papers published in journals, as well as works made available by selected organizations with mature safety culture. Three COHSIS were defined for description of its fundamentals, enabling improve the usability of its terminologies and provide the mentioned theoretical foundation.

Fractional pennes' bioheat equation: theoretical and numerical studies

In this work we provide a new mathematical model for the Pennes’ bioheat equation, assuming a fractional time derivative of single order. Alternative versions of the bioheat equation are studied and discussed, to take into account the temperature-dependent variability in the tissue perfusion, and both finite and infinite speed of heat propagation. The proposed bioheat model is solved numerically using an implicit finite difference scheme that we prove to be convergent and stable. The numerical method proposed can be applied to general reaction diffusion equations, with a variable diffusion coefficient. The results obtained with the single order fractional model, are compared with the original models that use classical derivatives.

Using a new developed die and different types of thermosetting resins to produce U200 profiles by pultrusion

In this work, a new steel heated pultrusion die was designed, developed and manufactured to produce U200 glass fibre reinforced thermosetting matrix (GRP) profiles. The finite element analysis (FEA) was used to predict and optimise the developed die heating by using cylindrical electrical powered cartridges. To assess the new die performance it was mounted in the 120 kN pultrusion line of the Portuguese company Vidropol SA and used to produce continuously U200 profiles able to meet all requirements specified for the E23 grade accordingly to the European Standard EN 13706: 2002. After setting up the type, orientation and sequence of layers in the U 200 laminate, different types of thermosetting resins were used in its production. Orthophthalic, isophthalic and bisphenolic unsaturated polyester as well as vinylester resins were used to produce glass fibre reinforced U 200 composite profiles. All applied resins were submitted to SPI gel tests in order to select the more appropriated catalyst system and optimise the processing variables to be used in each case, namely, pultrusion pull-speed and die temperature. The best pultrusion operational conditions were selected by varying and monitoring the pull-speed and die temperature and, at the same time, measuring the temperature on the manufactured U 200 profile during processing. Finally, the produced U200 profiles were submitted to visual inspection, calcination and mechanical tests, namely, flexural, tensional and interlaminar shear strength (ILSS) tests, to assess their accomplishment with the EN 13706 requirements.

Da modelação matemática à simulação computacional: a experimentação matemática no ensino

Tese de Doutoramento em Ciências (área de especialização em Matemática).

Da modelação matemática à simulação computacional: a experimentação matemática no ensino

Tese de Doutoramento em Ciências (área de especialização em Matemática).

Logic programming and artificial neural networks in breast cancer detection

About 90% of breast cancers do not cause or are capable of producing death if detected at an early stage and treated properly. Indeed, it is still not known a specific cause for the illness. It may be not only a beginning, but also a set of associations that will determine the onset of the disease. Undeniably, there are some factors that seem to be associated with the boosted risk of the malady. Pondering the present study, different breast cancer risk assessment models where considered. It is our intention to develop a hybrid decision support system under a formal framework based on Logic Programming for knowledge representation and reasoning, complemented with an approach to computing centered on Artificial Neural Networks, to evaluate the risk of developing breast cancer and the respective Degree-of-Confidence that one has on such a happening.

Desenvolvimento de rede neuronal artificial para o diagnóstico de doenças neurodegenerativas

Dissertação de mestrado integrado em Engenharia Eletrónica Industrial e Computadores

Logificação da Psicologia o itinerário intelectual de Edmundo Curvelo sobre a Mente, a Lógica e a Filosofia

Tese de Doutoramento em Filosofia - Especialidade de Filosofia da Mente

Fundamental concepts in multibody dynamics

In this chapter, the fundamental ingredients related to formulation of the equations of motion for multibody systems are described. In particular, aspects such as degrees of freedom, types of coordinates, basic kinematics joints and types of analysis in multibody systems are briefly characterized. Illustrative examples of application are also presented to better clarify the fundamental issues for spatial rigid multibody systems, which are of crucial importance in the formulation development of mathematical models of mechanical systems, as well as its computational implementation.

Evaluation of inflammatory response induced by different types of daily contact lenses

Dissertação de mestrado em Genética Molecular