Constraint solving over multi-valued logics - application to digital circuits

Due to usage conditions, hazardous environments or intentional causes, physical and virtual systems are subject to faults in their components, which may affect their overall behaviour. In a ‘black-box’ agent modelled by a set of propositional logic rules, in which just a subset of components is externally visible, such faults may only be recognised by examining some output function of the agent. A (fault-free) model of the agent’s system provides the expected output given some input. If the real output differs from that predicted output, then the system is faulty. However, some faults may only become apparent in the system output when appropriate inputs are given. A number of problems regarding both testing and diagnosis thus arise, such as testing a fault, testing the whole system, finding possible faults and differentiating them to locate the correct one. The corresponding optimisation problems of finding solutions that require minimum resources are also very relevant in industry, as is minimal diagnosis. In this dissertation we use a well established set of benchmark circuits to address such diagnostic related problems and propose and develop models with different logics that we formalise and generalise as much as possible. We also prove that all techniques generalise to agents and to multiple faults. The developed multi-valued logics extend the usual Boolean logic (suitable for faultfree models) by encoding values with some dependency (usually on faults). Such logics thus allow modelling an arbitrary number of diagnostic theories. Each problem is subsequently solved with CLP solvers that we implement and discuss, together with a new efficient search technique that we present. We compare our results with other approaches such as SAT (that require substantial duplication of circuits), showing the effectiveness of constraints over multi-valued logics, and also the adequacy of a general set constraint solver (with special inferences over set functions such as cardinality) on other problems. In addition, for an optimisation problem, we integrate local search with a constructive approach (branch-and-bound) using a variety of logics to improve an existing efficient tool based on SAT and ILP.

Solving colored nonograms

Trabalho apresentado no âmbito do Mestrado em Engenharia Informática, como requisito parcial para obtenção do grau de Mestre em Engenharia Informática

Modern techniques for constraint solving the CASPER experience

Dissertação apresentada para obtenção do Grau de Doutor em Engenharia Informática, pela Universidade Nova de Lisboa, Faculdade de Ciências e Tecnologia

Constraint reasoning for differential models

The basic motivation of this work was the integration of biophysical models within the interval constraints framework for decision support. Comparing the major features of biophysical models with the expressive power of the existing interval constraints framework, it was clear that the most important inadequacy was related with the representation of differential equations. System dynamics is often modelled through differential equations but there was no way of expressing a differential equation as a constraint and integrate it within the constraints framework. Consequently, the goal of this work is focussed on the integration of ordinary differential equations within the interval constraints framework, which for this purpose is extended with the new formalism of Constraint Satisfaction Differential Problems. Such framework allows the specification of ordinary differential equations, together with related information, by means of constraints, and provides efficient propagation techniques for pruning the domains of their variables. This enabled the integration of all such information in a single constraint whose variables may subsequently be used in other constraints of the model. The specific method used for pruning its variable domains can then be combined with the pruning methods associated with the other constraints in an overall propagation algorithm for reducing the bounds of all model variables. The application of the constraint propagation algorithm for pruning the variable domains, that is, the enforcement of local-consistency, turned out to be insufficient to support decision in practical problems that include differential equations. The domain pruning achieved is not, in general, sufficient to allow safe decisions and the main reason derives from the non-linearity of the differential equations. Consequently, a complementary goal of this work proposes a new strong consistency criterion, Global Hull-consistency, particularly suited to decision support with differential models, by presenting an adequate trade-of between domain pruning and computational effort. Several alternative algorithms are proposed for enforcing Global Hull-consistency and, due to their complexity, an effort was made to provide implementations able to supply any-time pruning results. Since the consistency criterion is dependent on the existence of canonical solutions, it is proposed a local search approach that can be integrated with constraint propagation in continuous domains and, in particular, with the enforcing algorithms for anticipating the finding of canonical solutions. The last goal of this work is the validation of the approach as an important contribution for the integration of biophysical models within decision support. Consequently, a prototype application that integrated all the proposed extensions to the interval constraints framework is developed and used for solving problems in different biophysical domains.

Human-robot teamwork: a knowledge-based solution

Dissertação apresentada na Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa para obtenção do grau de Mestre em Engenharia Electrotécnica e de Computadores

Playing Newtonian Games with Modellus

This article is a short introduction on how to use Modellus (a computer package that is freely available on the Internet and used in the IOP Advancing Physics course) to build physics games using Newton’s laws, expressed as differential equations. Solving systems of differential equations is beyond most secondary-school or first-year college students. However, with Modellus, the solution is simply the output of the usual physical reasoning: define the force law, compute its magnitude and components, use it to obtain the acceleration components, then the velocity components and, finally, use the velocity components to find the coordinates.

Integrated ecological-economic modelling and assessment aproach for coastal ecosystem management

Thesis submitted to the Faculty of Sciences and Technology, New University of Lisbon, for the degree of Doctor of Philosophy in Environmental Sciences

Validação da antropometria e ultrassonografia do braço, para medição dos respectivos compartimentos, em lactentes nascidos pré-termo : contributo para a avaliação corporal do recem-nascido e do lactente

RESUMO: Contexto: Indicadores fidedignos da composição corporal são importantes na orientação das estratégias nutricionais de recém-nascidos e pequenos lactentes submetidos a cuidados intensivos. O braço é uma região acessível para avaliar a composição corporal regional, pela medida dos seus compartimentos. A antropometria e a ultrassonografia (US) são métodos não invasivos, relativamente económicos, que podem ser usados à cabeceira do paciente na medição desses compartimentos, embora esses métodos não tenham ainda sido validados neste subgrupo etário. A ressonância magnética (RM) pode ser usada como método de referência na validação da medição dos compartimentos do braço. Objectivo: Validar em lactentes pré-termo, as medidas do braço por antropometria e por US. Métodos: Foi estudada uma coorte de recém-nascidos admitidos consecutivamente na unidade de cuidados intensivos neonatais, com  33 semanas de idade de gestação e peso adequado para a mesma, sem anomalias congénitas major e não submetidas a diuréticos ou oxigenoterapia no momento da avaliação. Nas vésperas da alta, foram efectuadas medições do braço, com ocultação, pelos métodos antropométrico, ultrassonográfico e RM. As medidas antropométricas directas foram: peso (P), comprimento (C), perímetro cefálico (PC), perímetro braquial (PB) e prega cutânea tricipital (PT). As área braquial total, área muscular (AM) e área adiposa foram calculadas pelos métodos de Jeliffee & Jeliffee e de Rolland-Cachera. Utilizando uma sonda PSH-7DLT de 7 Hz no ecógrafo Toshiba SSH 140A foram medidos os perímetros braquial e muscular e calculadas automaticamente as áreas braquial e muscular, sendo a área adiposa obtida por subtracção. Como método de referência foi utilizada a RM – Philips Gyroscan ACS-NT, Power-Track 1000 ®, 1.5 Tesla com uma antena de quadratura do joelho. Na análise estatística foram utilizados os métodos paramétricos e não paramétricos, conforme adequado. Resultados: Foram incluídas 30 crianças, nascidas com ( ±DP) 30.7 ±1.9 semanas de gestação, pesando 1380 ±325g, as quais foram avaliadas às 35.4 ±1.1 semanas de idade corrigida, quando pesavam 1786 ±93g. Nenhuma das medidas antropométricas, individualmente, constitui um indicador aceitável (r2 <0.5) das medições por RM. A melhor e mais simples equação alternativa encontrada é a que estima a AM (r2 = 0.56), derivada dos resultados da análise de regressão múltipla: AMRM = (P x 0.17) + (PB x 5.2) – (C x 6) – 150, sendo o P expresso em g, o C e o PB em cm. Nenhuma das medidas ultrassonográficas constitui um indicador aceitável (r2 <0.4) das medições por RM. Conclusões: A antropometria e as medidas ultrassonográficas do braço não são indicadores fidedignos da composição corporal regional em lactentes pré-termo, adequados para a idade de gestação.----------ABSTRACT: Background: Accurate predictors for body composition are valuable tools guiding nutritional strategies in infants needing intensive care. The upper-arm is a part of the body that is easily accessible and convenient for assessing the regional body composition, throughout the assessment of their compartments. Anthropometry and by ultrasonography (US) are noninvasive and relatively nonexpensive methods for bedside assessment of the upper-arm compartments. However, these methods have not yet been validated in infants. Magnetic resonance imaging (MRI) may be used as gold standard to validate the measurements of the upper-arm compartments. Objective: To validate the upper-arm measurements by anthropometry and by US in preterm infants. Methods: A cohort of neonates consecutively admitted at the neonatal intensive care unit, appropriate for gestational age, with  33 weeks, without major congenital abnormalities and not subjected to diuretics or oxygen therapy, was assessed. Before the discharge, the upper-arm was blindly measured by anthropometry, US and MRI. The direct anthropometric parameters measured were: weight (W), length (L), head circumference (HC), mid-arm circumference (MAC), and tricipital skinfold thickness. The arm area (AA), arm muscle area (AMA) and arm fat area were calculated applying the methods proposed by Jeliffee & Jeliffee and by Rolland-Cachera. Using the sonolayer Toshiba SSH 140A and the probe PSH-7DLT 7Hz, the arm and muscle perimeters were measured by US, the arm and muscle areas included were automatically calculated, and the fat area was calculated by subtraction. The MR images were acquired on a 1.5-T Philips Gyroscan ACS-NT, Power-Track 1000 scanner, and a knee coil was chosen for the upper-arm measurements. For statistical analysis parametric and nonparametric methods were used as appropriate. Results: Thirty infants born with ( ±SD) 30.7 ±1.9 weeks of gestational age and weighing 1380 ±325g were included in the study; they were assessed at 35.4 ±1.1 weeks of corrected age, weighing 1786 ±93g. None of the anthropometric measurements are individually acceptable (r2 <0.5) for prediction of the measurements obtained by MRI. The best and simple alternative equation found is the equation for prediction of the AMA (r2 = 0.56), derived from the results of multiple regression analysis: AMARM = (W x 0.17) + (MAC x 5.2) – (L x 6) – 150, being the W expressed in g, and L and MAC in cm. None of the ultrasonographic measurements are acceptable (r2 <0.5) predictors for the measurements obtained by MRI. Conclusions: The measurements of the upper-arm by anthropometry and by US are not accurate predictors for the regional body composition in preterm appropriate for gestational age infants.

Intelligent decision support systems for collaboration in industrial plants

Dissertação apresentada para obtenção do Grau de Doutor em Sistemas de Informação Industriais, Engenharia Electrotécnica, pela Universidade Nova de Lisboa, Faculdade de Ciências e Tecnologia

Constraint-based modeling of minimum set covering: application to species differentation

Work presented in the context of the European Master in Computational Logics, as partial requisit for the graduation as Master in Computational Logics

Negative non-ground queries in well founded semantics

Dissertação apresentada na Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa para obtenção do grau de Mestre em Computational Logic

Database repairs with answer set programming

Dissertação para obtenção do Grau de Mestre em Engenharia Informática

Monte Carlo simulations for dosimetric verification in photon and electron beam radiotherapy

Dissertação para obtenção do Grau de Doutor em Engenharia Biomédica

Constraint-based verification of imperative programs

work presented in the context of the European Master’s program in Computational Logic, as the partial requirement for obtaining Master of Science degree in Computational Logic

Modeling assembly program with constraints. A contribution to WCET problem

Dissertação para obtenção do Grau de Mestre em Lógica Computacional