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.

Concurrent tabling

In the past few years Tabling has emerged as a powerful logic programming model. The integration of concurrent features into the implementation of Tabling systems is demanded by need to use recently developed tabling applications within distributed systems, where a process has to respond concurrently to several requests. The support for sharing of tables among the concurrent threads of a Tabling process is a desirable feature, to allow one of Tabling’s virtues, the re-use of computations by other threads and to allow efficient usage of available memory. However, the incremental completion of tables which are evaluated concurrently is not a trivial problem. In this dissertation we describe the integration of concurrency mechanisms, by the way of multi-threading, in a state of the art Tabling and Prolog system, XSB. We begin by reviewing the main concepts for a formal description of tabled computations, called SLG resolution and for the implementation of Tabling under the SLG-WAM, the abstract machine supported by XSB. We describe the different scheduling strategies provided by XSB and introduce some new properties of local scheduling, a scheduling strategy for SLG resolution. We proceed to describe our implementation work by describing the process of integrating multi-threading in a Prolog system supporting Tabling, without addressing the problem of shared tables. We describe the trade-offs and implementation decisions involved. We then describe an optimistic algorithm for the concurrent sharing of completed tables, Shared Completed Tables, which allows the sharing of tables without incurring in deadlocks, under local scheduling. This method relies on the execution properties of local scheduling and includes full support for negation. We provide a theoretical framework and discuss the implementation’s correctness and complexity. After that, we describe amethod for the sharing of tables among threads that allows parallelism in the computation of inter-dependent subgoals, which we name Concurrent Completion. We informally argue for the correctness of Concurrent Completion. We give detailed performance measurements of the multi-threaded XSB systems over a variety of machines and operating systems, for both the Shared Completed Tables and the Concurrent Completion implementations. We focus our measurements inthe overhead over the sequential engine and the scalability of the system. We finish with a comparison of XSB with other multi-threaded Prolog systems and we compare our approach to concurrent tabling with parallel and distributed methods for the evaluation of tabling. Finally, we identify future research directions.

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

Description de restes squelettiques de Latidae: Lates (?) sp. (Poissons téléostéens, Percoidei) du Miocène inférieur et moyen du bassin du Bas Tage (environs de Lisbonne, Portugal)

Several Lower and Middle Miocene localities in the Lower Tagus basin near Lisbon yielded Latidae fragmentary remnants. No really decisive character has been recognized that would allow us to state these remnants could surely be ascribed to the genus Lates Cuv. & Val., although we regard this as nearly certain. There are some differences between the Miocene latidae under study and the type species Lates niloticus L. this suggests us to report the concerned remnants to a Lates (?) sp. that could belong to a new, hitherto undescribed species. The occurrence of Lates in fluviatile or lagoonal beds in the Lower Tagus basin Miocene series is not at all surprising under a paleoeciological view point. Even less if account is taken of the presence in the same levels of Siluriforms remnants belonging to Bagridae and Ariidae, two families that are well represented in Africa. Bagrid spines have been found at Quinta das Pedreiras in association with Lates (?) sp. remnants. The Lates (?) sp. discovery in the Lower and Middle Miocene from the Lower Tagus basin results in extending to the West this genus' biogeographic distribution. It is indeed the first discovery of this genus on Europe's Atlantic coasts. No matter which was the geographic origin of these fishes, they had to migrate several hundreds of kilometers through marine waters before entering the Tagus' estuary. The association of Lates (?) sp. remnants with Siluriform ones that have an extant, broad repartition in Africa south of the Sahara points out to an African origin. These thermophyll fishes imigration along the Atlantic coasts from lberian Peninsula probably has been possible owing to a warm climatic event that allowed them to migrate ca. 5 degrees (in latitude) northwards in Burdigalian times.

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

Combining open and closed world reasoning for the semantic web

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

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

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.

Evolution of Teeth and Quadrate in Non-avian Theropoda (Dinosauria: Saurischia), with the Description of Torvosaurus Remains from Portugal

Theropods form a highly successful and morphologically diversified group of dinosaurs that gave rise to birds. They include most, if not all, carnivorous dinosaurs, yet many theropod clades were secondarily adapted to piscivory, omnivory and herbivory, and theropods show a large array of skull and dentition morphologies. This work aims to investigate aspects of the evolution of theropod dinosaurs by analyzing in detail both the anatomy and ontogeny of teeth and quadrates in non-avian theropods, and by studying embryonic and adult material of a new species of theropod. A standardized list of terms and notations for each anatomical entity of the tooth, quadrate, and maxilla is here proposed with the goal of facilitating descriptions of these important cranial and dental elements. The distribution of thirty dental characters among 113 theropod taxa is investigated, and a list of diagnostic dental characters is proposed. As an example, four isolated theropod teeth from the Lourinhã Formation (Kimmeridgian‒Tithonian) of Portugal are described and identified based on a cladistic analysis performed on a data matrix of 141 dentition-based characters coded in 60 taxa. Two shed teeth are referred to an abelisaurid, providing the first record of Abelisauridae in the Jurassic of Laurasia and the one of the oldest records of this clade in the world, suggesting a possible radiation of Abelisauridae in Europe well before the Upper Cretaceous. The consensus tree resulting from this phylogenetic analysis, the most extensive on theropod teeth, indicates that theropod teeth provide reliable data for identification at approximately family level, and this method will help identifying theropod teeth with more confidence. A detailed description of the dentition of Megalosauridae is also provided, and a discriminant analysis performed on a dataset of numerical data collected on the teeth of 62 theropod taxa reveals that megalosaurid teeth are hardly distinguishable from other theropod clades with ziphodont dentition. This study highlights the importance of detailing anatomical descriptions and providing additional morphometric data on teeth with the purpose of helping to identify isolated theropod teeth. In order to evaluate the phylogenetic potential and investigate the evolutionary transformations of the quadrate, a phylogenetic morphometric analysis as well as a cladistic analysis using 98 discrete quadrate related characters were conducted. The quadrate morphology by its own provides a wealth of data with strong phylogenetic signal, and the phylogenetic morphometric analysis reveals two main morphotypes of the mandibular articulation of the quadrate linked to function. As an example, six isolated quadrates from the Kem Kem beds (Cenomanian) of Morocco are determined to be from juvenile and adult individuals of Spinosaurinae based on phylogenetic, morphometric, and phylogenetic morphometric analyses. Morphofunctional analysis of the spinosaurid mandibular articulation has shown that the posterior parts of the two mandibular rami displaced laterally when the jaw was depressed due to a mediolaterally oriented intercondylar sulcus of the quadrate. Such lateral movement of the mandibular ramus was possible due to a movable mandibular symphysis in spinosaurids, allowing the pharynx to be widened. A new species of theropod from the Lourinhã Formation of Portugal, Torvosaurus gurneyi, is erected based on a right maxilla and an incomplete caudal centrum. This taxon supports the mechanism of vicariance that occurred in the Iberian Meseta during the Late Jurassic when the proto-Atlantic was already well formed. A theropod clutch containing several crushed eggs and embryonic material is also assigned to this new species of Torvosaurus. Investigation on the maxilla ontogeny in basal tetanurans reveals that crown denticles, elongation of the anterior ramus, and fusion of interdental plates appear at a posthatchling stage. On the other hand, maxillary pneumaticity is already present at an embryonic stage in non-avian theropods.

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.

A description of the Australian early psychosis intervention model and a proposal to establish a Pilot Early Intervention Program in Santa Cruz de la Sierra, Bolívia

RESUMO: Em 2011, a Associação Psiquiátrica Mundial lançou um programa de bolsas de investigação para psiquiatras em início de carreira a partir de países de renda baixa ou média-baixa, no âmbito deste programa, o autor foi selecionado para uma bolsa de pesquisa no Centre for Youth Mental Health/Orygen Youth Health Research Centre da Universidade de Melbourne. Orygen, é a principal organização de pesquisa e tradução do conhecimento do mundo com foco em problemas de saúde mental em pessoas jovens. O estágio foi baseado em Prevenção e Intervenção Precoce Psychosis Centre (EPPIC), que faz parte do Orygen. EPPIC fornece programa de tratamento abrangente e integrada, baseada na comunidade para o primeiro episódio de psicose. Esta dissertação descreve o modelo EPPIC, e seus componentes essenciais e fatores que são necessários para uma implementação de serviço direito. Além disso, uma proposta de criação de um programa-piloto de intervenção psicose precoce é discutido. Este programa inclui um programa de extensão inovadora que combina princípios comerciais sólidos, com metas sociais, a fim de combater especificamente a maior barreira para o tratamento da psicose precoce na Bolívia: o estigma da doença mental. Ao utilizar uma equipe de tratamento móvel, multidisciplinar, que enfatiza os papéis dos gerentes do caso treinados focada em fornecer indivíduo intensiva e apoio familiar no lar, este programa irá prestar cuidados culturalmente apropriados que irá alavancar contribuições de um suprimento limitado de psiquiatras e mudar longe da dependência um sistema médico fragmentado. ---------------------------- ABSTRACT: In 2011, the World Psychiatric Association launched a programme of research fellowships for early-career psychiatrists from low- or lower-middle income countries, within this programme, the author was selected to a research fellowship at the Centre for Youth Mental Health/Orygen Youth Health Research Centre at University of Melbourne. Orygen, is the world’s leading research and knowledge translation organization focusing on mental ill-health in young people. The traineeship was based on Early Psychosis Prevention and Intervention Centre (EPPIC), which is part of Orygen. EPPIC provides comprehensive, integrated, community-based treatment program for first-episode psychosis. This dissertation describes the EPPIC model, and its core components and factors which are necessary to a right service implementation. Additionally, a proposal to establish a pilot early psychosis intervention programme is discussed. This programme includes an innovative outreach programme that combines sound business principals with social goals in order to specifically target the largest barrier to early psychosis treatment in Bolivia: the stigma of mental illness. By utilizing a mobile, multidisciplinary treatment team that emphasizes the roles of trained case managers focused on providing intensive individual and family support in the home, this programme will provide culturally appropriate care that will leverage contributions from a limited supply of psychiatrists and shift dependence away from a fragmented medical system.

Reconfigurable photonic logic architecture

The amorphous silicon photo-sensor studied in this thesis, is a double pin structure (p(a-SiC:H)-i’(a-SiC:H)-n(a-SiC:H)-p(a-SiC:H)-i(a-Si:H)-n(a-Si:H)) sandwiched between two transparent contacts deposited over transparent glass thus with the possibility of illumination on both sides, responding to wave-lengths from the ultra-violet, visible to the near infrared range. The frontal il-lumination surface, glass side, is used for light signal inputs. Both surfaces are used for optical bias, which changes the dynamic characteristics of the photo-sensor resulting in different outputs for the same input. Experimental studies were made with the photo-sensor to evaluate its applicability in multiplexing and demultiplexing several data communication channels. The digital light sig-nal was defined to implement simple logical operations like the NOT, AND, OR, and complex like the XOR, MAJ, full-adder and memory effect. A pro-grammable pattern emission system was built and also those for the validation and recovery of the obtained signals. This photo-sensor has applications in op-tical communications with several wavelengths, as a wavelength detector and to execute directly logical operations over digital light input signals.