Every normal logic program has a 2-valued semantics: theory, extensions, applications, implementations

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

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.

Efficient paraconsistent reasoning with rules and ontologies for the semantic web

Ontologies formalized by means of Description Logics (DLs) and rules in the form of Logic Programs (LPs) are two prominent formalisms in the field of Knowledge Representation and Reasoning. While DLs adhere to the OpenWorld Assumption and are suited for taxonomic reasoning, LPs implement reasoning under the Closed World Assumption, so that default knowledge can be expressed. However, for many applications it is useful to have a means that allows reasoning over an open domain and expressing rules with exceptions at the same time. Hybrid MKNF knowledge bases make such a means available by formalizing DLs and LPs in a common logic, the Logic of Minimal Knowledge and Negation as Failure (MKNF). Since rules and ontologies are used in open environments such as the Semantic Web, inconsistencies cannot always be avoided. This poses a problem due to the Principle of Explosion, which holds in classical logics. Paraconsistent Logics offer a solution to this issue by assigning meaningful models even to contradictory sets of formulas. Consequently, paraconsistent semantics for DLs and LPs have been investigated intensively. Our goal is to apply the paraconsistent approach to the combination of DLs and LPs in hybrid MKNF knowledge bases. In this thesis, a new six-valued semantics for hybrid MKNF knowledge bases is introduced, extending the three-valued approach by Knorr et al., which is based on the wellfounded semantics for logic programs. Additionally, a procedural way of computing paraconsistent well-founded models for hybrid MKNF knowledge bases by means of an alternating fixpoint construction is presented and it is proven that the algorithm is sound and complete w.r.t. the model-theoretic characterization of the semantics. Moreover, it is shown that the new semantics is faithful w.r.t. well-studied paraconsistent semantics for DLs and LPs, respectively, and maintains the efficiency of the approach it extends.

Semantics of logic programs with explicit negation

After a historical introduction, the bulk of the thesis concerns the study of a declarative semantics for logic programs. The main original contributions are: ² WFSX (Well–Founded Semantics with eXplicit negation), a new semantics for logic programs with explicit negation (i.e. extended logic programs), which compares favourably in its properties with other extant semantics. ² A generic characterization schema that facilitates comparisons among a diversity of semantics of extended logic programs, including WFSX. ² An autoepistemic and a default logic corresponding to WFSX, which solve existing problems of the classical approaches to autoepistemic and default logics, and clarify the meaning of explicit negation in logic programs. ² A framework for defining a spectrum of semantics of extended logic programs based on the abduction of negative hypotheses. This framework allows for the characterization of different levels of scepticism/credulity, consensuality, and argumentation. One of the semantics of abduction coincides with WFSX. ² O–semantics, a semantics that uniquely adds more CWA hypotheses to WFSX. The techniques used for doing so are applicable as well to the well–founded semantics of normal logic programs. ² By introducing explicit negation into logic programs contradiction may appear. I present two approaches for dealing with contradiction, and show their equivalence. One of the approaches consists in avoiding contradiction, and is based on restrictions in the adoption of abductive hypotheses. The other approach consists in removing contradiction, and is based in a transformation of contradictory programs into noncontradictory ones, guided by the reasons for contradiction.

A Logic and tool for local reasoning about security protocols

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

Derivation methods for hybrid knowledge bases with rules and ontologies

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

A behavioral analysis tool for models of software systems

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

Core language for web applications

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

Combining open and closed world reasoning for the semantic web

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

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

Aconselhamento médico na prevenção da doença e promoção da saúde : análise a propósito do consumo de tabaco

RESUMO - O consumo de tabaco foi responsável por 100 milhões de mortes no século XX. Apesar dos grandes avanços alcançados no controlo deste problema a nível mundial, sob os auspícios da OMS, no contexto da Convenção-Quadro para o Controlo do Tabaco da OMS, se não forem adoptadas medidas consistentes e efectivas de saúde pública, a morbi-mortalidade que lhe está associada continuará a aumentar durante o presente século. A promoção da cessação tabágica constitui a estratégia populacional que permitirá obter ganhos em saúde a mais curto prazo. Embora a larga maioria dos fumadores faça, ao longo da vida, várias tentativas para parar de fumar sem apoio, apenas uma pequena minoria consegue manter-se abstinente a longo prazo. Os médicos de Medicina Geral e Familiar são, de entre todos os profissionais de saúde, os que podem intervir de modo mais consistente e efectivo neste âmbito e que melhores resultados obtêm na cessação tabágica dos pacientes fumadores, dado o vínculo terapêutico e a interacção frequente e continuada que com eles estabelecem ao longo do seu ciclo de vida. O aconselhamento breve, tendo por base a adopção de um estilo de comunicação motivacional centrado no paciente, adaptado aos estádios de mudança comportamental, tem-se revelado efectivo no apoio à mudança de comportamentos relacionados com a saúde e à resolução da ambivalência que caracteriza este processo. A revisão de literatura evidenciou o facto de os médicos nem sempre intervirem nas áreas preventivas e de promoção da saúde, em particular na área da cessação tabágica, com o investimento e a continuidade desejáveis. Por outro lado, muitos pacientes fumadores referem nunca ter sido aconselhados pelo seu médico a deixar de fumar.. Não são conhecidos estudos de âmbito nacional que permitam conhecer esta realidade, bem como os factores associados às melhores práticas de intervenção ou as barreiras sentidas pelos médicos de MGF à actuação nesta área. O presente trabalho teve como objectivos: (i) avaliar a hipótese de que os médicos que disseram adoptar o método clínico centrado no paciente teriam atitudes mais favoráveis relativamente à cessação tabágica e uma maior probabilidade de aconselhar os seus pacientes a parar de fumar; (ii) estudar a relação entre as atitudes, a percepção de auto-eficácia, a expectativa de efectividade e as práticas de aconselhamento sobre cessação tabágica, auto-referidas pelos médicos; (iii) Identificar as variáveis preditivas da adopção de intervenções breves de aconselhamento adaptadas ao estádio de mudança comportamental dos pacientes fumadores; (iv) identificar as barreiras e os incentivos à adopção de boas práticas de aconselhamento nesta área. A população de estudo foi constituída pelo total de médicos de medicina geral e familiar inscritos na Associação Portuguesa de Médicos de Clínica Geral, residentes em Portugal. Para recolha de informação, foi utilizado um questionário de resposta anónima, de autopreenchimento, aplicado por via postal a 2942 médicos, em duas séries de envio. O questionário integrou perguntas fechadas, semifechadas, escalas de tipo Likert e escalas de tipo visual analógico. Para avaliação da adopção do método clínico centrado no paciente, foi usada a Patient Practitioner Orientation Scale (PPOS). O tratamento estatístico dos dados foi efectuado com o Programa PASW Statistics (ex-SPSS), versão 18. Foram utilizados: o índice de α de Cronbach, diversos testes não paramétricos e a análise de regressão logística binária. Foi obtida uma taxa de resposta de 22,4%. Foram analisadas 639 respostas (67,4% de mulheres e 32,6% de homens). Referiram ser fumadores 23% dos homens e 14% das mulheres. Foi identificada uma grande carência formativa em cessação tabágica, tendo apenas 4% dos médicos afirmado não necessitar de formação nesta área. Responderam necessitar de formação em entrevista motivacional 66%, em prevenção da recaída 59%, de treino numa consulta de apoio intensivo 55%, em intervenção breve 54% e em terapêutica farmacológica 55%. Cerca de 92% dos respondentes consideraram que o aconselhamento para a cessação tabágica é uma tarefa que faz parte das suas atribuições, mas apenas 76% concordaram totalmente com a realização de uma abordagem oportunística deste assunto em todos os contactos com os seus pacientes. Como prática mais frequente, perante um paciente em preparação para parar, 85% dos médicos disseram tomar a iniciativa de aconselhar, 79% avaliar a motivação, 67% avaliar o grau de dependência, 60% marcar o “dia D” e 50% propor terapêutica farmacológica. Apenas 21% assumiram realizar com frequência uma intervenção breve com pacientes em preparação (5 Ás); 13% uma intervenção motivacional com pacientes não motivados para mudar (5 Rs) e 20% uma intervenção segundo os princípios da entrevista motivacional, relativamente a pacientes ambivalentes em relação à mudança. A análise multivariada de regressão logística permitiu concluir que as variáveis com maior influência na decisão de aconselhar os pacientes sobre cessação tabágica foram a percepção de auto-eficácia, o nível de atitudes negativas, a adopção habitual do Programa-tipo de cessação tabágica da DGS, a posse de formação específica nesta área e a não identificação de barreiras ao aconselhamento, em particular organizacionais ou ligadas ao processo de comunicação na consulta. Embora se tenha confirmado a existência de associação entre a adopção do método clínico centrado no paciente e as atitudes face à cessação tabágica, não foi possível confirmar plenamente a associação entre a adopção deste método e as práticas autoreferidas de aconselhamento. Os médicos que manifestaram um nível baixo ou moderado de atitudes negativas, uma percepção elevada de auto-eficácia, que nunca fumaram, que referiram adoptar o Programa-tipo de cessação tabágica e que não identificaram barreiras organizacionais apresentaram uma maior probabilidade de realizar uma intervenção breve (“5 Ás”) de aconselhamento de pacientes fumadores em preparação para parar de fumar. Nunca ter fumado apresentou-se associado a uma probabilidade de realizar uma intervenção breve (“5 Ás”) com frequência, superior à verificada entre os médicos que referiram ser fumadores (Odds-ratio ajustado = 2,6; IC a 95%: 1,1; 5,7). Os médicos com o nível de auto-eficácia no aconselhamento mais elevado apresentaram uma probabilidade superior à encontrada entre os médicos com o menor nível de auto-eficácia de realizar com frequência uma intervenção breve de aconselhamento, integrando as cinco vertentes dos “5 Ás” (Odds ratio ajustado = 2,6; IC a 95%: 1,3; 5,3); de realizar uma intervenção motivacional breve com fumadores renitentes a parar de fumar (Odds ratio ajustado = 3,1; IC a 95%: 1,4; 6,5) ou de realizar com frequência uma intervenção motivacional com pacientes em estádio de ambivalência (Odds ratio = 8,8; IC a 95%: 3,8; 19,9). A falta de tempo, a falta de formação específica e a falta de equipa de apoio foram as barreiras ao aconselhamento mais citadas. Como factores facilitadores de um maior investimento nesta área, cerca de 60% dos médicos referiram a realização de um estágio prático de formação; 57% a possibilidade de dispor do apoio de outros profissionais; cerca de metade a melhoria da sua formação teórica. Cerca de 25% dos médicos investiria mais em cessação tabágica se dispusesse de um incentivo financeiro e 20% se os pacientes demonstrassem maior interesse em discutir o assunto ou existisse uma maior valorização desta área por parte dos colegas e dos órgãos de gestão. As limitações de representatividade da amostra, decorrentes da taxa de resposta obtida, impõem reservas à possibilidade de extrapolação destes resultados para a população de estudo, sendo de admitir que os respondentes possam corresponder aos médicos mais interessados por este tema e que optam por não fumar. Outra importante limitação advém do facto de não ter sido estudada a vertente relativa aos pacientes, no que se refere às suas atitudes, percepções e expectativas quanto à actuação do médico neste campo. Pesem embora estas limitações, os resultados obtidos revelaram uma grande perda de oportunidades de prevenção da doença e de promoção da saúde. Parece ter ficado demonstrada a importante influência que as atitudes, em especial as negativas, e as percepções, em particular a percepção de auto-eficácia, podem exercer sobre as práticas de aconselhamento auto-referidas. Todavia, será necessário aprofundar os resultados agora encontrados com estudos de natureza qualitativa, que permitam compreender melhor, por um lado, as percepções, expectativas e necessidades dos pacientes, por outro, as estratégias de comunicação que deverão ser adoptadas pelo médico, atendendo à complexidade do problema e ao tempo disponível na consulta, tendo em vista aumentar a literacia dos pacientes para uma melhor autogestão da sua saúde. Parece ter ficado igualmente patente a grande carência formativa neste domínio. A adopção do modelo biomédico como paradigma da formação médica pré e pós-graduada, proposto, há precisamente cem anos, por Flexner, tem contribuído para a desvalorização das componentes psicoemocionais e sociais dos fenómenos de saúde e de doença, assim como para criar clivagens entre cuidados curativos e preventivos e entre medicina geral e familiar e saúde pública. Porém, o actual padrão de saúde/doença próprio das sociedades desenvolvidas, caracterizado por “pandemias” de doenças crónicas e incapacitantes, determinadas por factores de natureza sociocultural e comportamental, irá obrigar certamente à revisão daquele paradigma e à necessidade de se (re)adoptarem os grandes princípios Hipocráticos de compreensão dos processos de saúde/doença e do papel da medicina.

Revision based total semantics for extended normal logic programs

Dissertação para obtenção do Grau de Doutor em Matemática - Lógica e Fundamentos da Matemática

A logical foundation for session-based concurrent computation

Linear logic has long been heralded for its potential of providing a logical basis for concurrency. While over the years many research attempts were made in this regard, a Curry-Howard correspondence between linear logic and concurrent computation was only found recently, bridging the proof theory of linear logic and session-typed process calculus. Building upon this work, we have developed a theory of intuitionistic linear logic as a logical foundation for session-based concurrent computation, exploring several concurrency related phenomena such as value-dependent session types and polymorphic sessions within our logical framework in an arguably clean and elegant way, establishing with relative ease strong typing guarantees due to the logical basis, which ensure the fundamental properties of type preservation and global progress, entailing the absence of deadlocks in communication. We develop a general purpose concurrent programming language based on the logical interpretation, combining functional programming with a concurrent, session-based process layer through the form of a contextual monad, preserving our strong typing guarantees of type preservation and deadlock-freedom in the presence of general recursion and higher-order process communication. We introduce a notion of linear logical relations for session typed concurrent processes, developing an arguably uniform technique for reasoning about sophisticated properties of session-based concurrent computation such as termination or equivalence based on our logical approach, further supporting our goal of establishing intuitionistic linear logic as a logical foundation for sessionbased concurrency.

Machine ethics via logic programming

Machine ethics is an interdisciplinary field of inquiry that emerges from the need of imbuing autonomous agents with the capacity of moral decision-making. While some approaches provide implementations in Logic Programming (LP) systems, they have not exploited LP-based reasoning features that appear essential for moral reasoning. This PhD thesis aims at investigating further the appropriateness of LP, notably a combination of LP-based reasoning features, including techniques available in LP systems, to machine ethics. Moral facets, as studied in moral philosophy and psychology, that are amenable to computational modeling are identified, and mapped to appropriate LP concepts for representing and reasoning about them. The main contributions of the thesis are twofold. First, novel approaches are proposed for employing tabling in contextual abduction and updating – individually and combined – plus a LP approach of counterfactual reasoning; the latter being implemented on top of the aforementioned combined abduction and updating technique with tabling. They are all important to model various issues of the aforementioned moral facets. Second, a variety of LP-based reasoning features are applied to model the identified moral facets, through moral examples taken off-the-shelf from the morality literature. These applications include: (1) Modeling moral permissibility according to the Doctrines of Double Effect (DDE) and Triple Effect (DTE), demonstrating deontological and utilitarian judgments via integrity constraints (in abduction) and preferences over abductive scenarios; (2) Modeling moral reasoning under uncertainty of actions, via abduction and probabilistic LP; (3) Modeling moral updating (that allows other – possibly overriding – moral rules to be adopted by an agent, on top of those it currently follows) via the integration of tabling in contextual abduction and updating; and (4) Modeling moral permissibility and its justification via counterfactuals, where counterfactuals are used for formulating DDE.

UK Mental health professionals volunteering in LMIC-benefits to UK and host countries

RESUMO: O Royal College of Psychiatrists tem um programa de voluntariado internacional desde 2005. O interesse no Reino Unido tem crescido nos últimos 15 anos com muitos projetos novos. Os benefícios para vários países têm sido reconhecidos. O que está menos claro são os benefícios da experiência para o Reino Unido e do programa de voluntariado do Royal College of Psychiatrists. O objectivo desta dissertação é explorar os benefícios do voluntariado para o Sistema Nacional de Saúde focando principalmente, mas não exclusivamente, o programa de voluntariado do Royal College of Psychiatrists. Nesta dissertação abordamos primeiro o contexto antes de discutirmos dois grandes estudos de psiquiatras e hospitais do Sistema Nacional de Saúde no Reino Unido. Incluimos no estudo todos os psiquiatras registados como Voluntários no Royal College of Psychiatrists e o Grupo de Interesse Especial associado. Foi ainda possível incluir os Diretores Médicos de todos os hospitais do Reino Unido. Os estudos foram desenhados para analisar as opiniões dos Voluntários do Reino Unido sobre os benefícios para os países recetores de baixo e médio rendimento e para o Reino Unido. Todos os 60 hospitais do Sistema Nacional de Saúde foram incluí dos para analisar a opinião sobre Voluntariado. As limitações dos estudos foram a baixa taxa de resposta, mas esta foi comparável a outros estudos do College. É provável haver um enviezamento de resposta e favorecimento dos que estão envolvidos no Voluntariado. Os resultados mostraram um interesse forte no voluntariado e benefícios no Sistema Nacional de Saúde, nas. áreas de liderança, transculturalismo, gestão e recursos e capacidades pessoais. Os hospitais do Sistema Nacional de Saúde valorizaram o voluntariado e, em contrapartida, o valor acrescido para competências profissionais. Os obstáculos contra o Voluntariado a nível individual e dos hospitais foram maioritariamente de natureza prática, tais como obter dispensa do trabalho, substituição no trabalho e custos. As implicações destes estudos são que o programa de voluntariado do College precisa de ser fortalecido. Para assegurar que este trabalho continua é necessário existir uma sensibilização nacional e maior responsabilização sobre os benefícios para o Reino Unido e a nível global. -------------------------- ABSTRACT: The Royal College of Psychiatrists has had an international volunteering programme since 2005. The interest in UK has grown over the past 15 years with many new projects. The benefits in various countries has been acknowledged. What has been less clear are the benefits of the experience back in the UK and of the Royal College of Psychiatrists Volunteer Scheme. The aim of this dissertation is to explore the benefit of volunteering to the NHS focusing mainly, but not exclusively on the Royal College of Psychiatrists Volunteering scheme. In this dissertation we first look at background information before discussing two large surveys of Psychiatrists and NHS Trusts in UK. We surveyed all those registered as Volunteers at the Royal College of Psychiatrists and the associated Special Interest Group. We also were able to survey the Medical Directors of all UK Trusts. The Surveys were designed to assess views of UK Volunteers of benefits to hosts in LMIC and back in UK. All 60 NHS Trusts were surveyed to assess the view of Volunteering. Limitation of the surveys were the low response rate but this was comparable to other College surveys. There is likely to be a bias in response and favour those who are engaged in the Volunteering agenda. Results showed a strong interest in volunteering and perceived benefits in NHS. These areas included leadership, transcultural, resource management and personal skills. NHS trusts valued volunteering and added value to professional competencies on return. Obstacles to Volunteering at individual and Trust level were mainly practical issues such as getting time off, cover and costs. Implications of these surveys are that the College volunteering scheme needs strengthening. There needs to be a National advocacy to ensure that this work continues and greater accountability as to benefits in UK and globally.