On Compositional Modelling

Many solutions to AI problems require the task to be represented in one of a multitude of rigorous mathematical formalisms. The construction of such mathematical models forms a difficult problem which is often left to the user of the problem solver. This void between problem solvers and the problems is studied by the eclectic field of automated modelling. Within this field, compositional modelling, a knowledge-based methodology for system modelling, has established itself as a leading approach. In general, a compositional modeller organises knowledge in a structure of composable fragments that relate to particular system components or processes. Its embedded inference mechanism chooses the appropriate fragments with respect to a given problem, instantiates and assembles them into a consistent system model. Many different types of compositional modeller exist, however, with significant differences in their knowledge representation and approach to inference. This paper examines compositional modelling. It presents a general framework for building and analysing compositional modellers. Based on this framework, a number of influential compositional modellers are examined and compared. The paper also identifies the strengths and weaknesses of compositional modelling and discusses some typical applications.

An approach to search and exploration through mixed-initiative

Generative design environments need support for human intervention as well as sound computational formalisms. A systematic approach to integrating the two, formal generation and the exploratory, is lacking. In this paper, we posit the possibility of a design support system that combines formal search with user driven exploration. Our approach is to cast the interaction between the user and the generative formalism as agent collaboration in a mixed-initiative environment. We describe the role of interaction and agency in an experimental mixed-initiative design support system, FOLDS and demonstrate its application.

Symbolic computation and perfect fluids in general relativity

Focuses on two areas within the field of general relativity. Firstly, the history and implications of the long-standing conjecture that general relativistic, shear-free perfect fluids which obey a barotropic equation of state p = p(w) such that w + p = 0, are either non-expanding or non-rotating. Secondly the application of the computer algebra system Maple to the area of tetrad formalisms in general relativity.

A formal model of mixed-initiative interaction in design exploration

Computer-based environments for supporting design are complex software artifacts. These tools need to use sound computational formalisms as well as address issues of human usability. The development of interactive and usable generative systems is a significant research area in design computation. Though classical search techniques play a central role in the generative kernels of these "closed-world" systems, the open-ended exploration of design spaces is the desirable goal. In this paper, we present a formal model of exploration that combines search with user driven exploration. We describe the role of interaction and agency in an experimental mixed-initiative design support system.

Mind change optimal learning of Bayes net structure

This paper analyzes the problem of learning the structure of a Bayes net (BN) in the theoretical framework of Gold’s learning paradigm. Bayes nets are one of the most prominent formalisms for knowledge representation and probabilistic and causal reasoning. We follow constraint-based approaches to learning Bayes net structure, where learning is based on observed conditional dependencies between variables of interest (e.g., “X is dependent on Y given any assignment to variable Z”). Applying learning criteria in this model leads to the following results. (1) The mind change complexity of identifying a Bayes net graph over variables V from dependency data is |V| 2 , the maximum number of edges. (2) There is a unique fastest mind-change optimal Bayes net learner; convergence speed is evaluated using Gold’s dominance notion of “uniformly faster convergence”. This learner conjectures a graph if it is the unique Bayes net pattern that satisfies the observed dependencies with a minimum number of edges, and outputs “no guess” otherwise. Therefore we are using standard learning criteria to define a natural and novel Bayes net learning algorithm. We investigate the complexity of computing the output of the fastest mind-change optimal learner, and show that this problem is NP-hard (assuming P = RP). To our knowledge this is the first NP-hardness result concerning the existence of a uniquely optimal Bayes net structure.

On some properties of weighted averaging with variable weights

Density-based means have been recently proposed as a method for dealing with outliers in the stream processing of data. Derived from a weighted arithmetic mean with variable weights that depend on the location of all data samples, these functions are not monotonic and hence cannot be classified as aggregation functions. In this article we establish the weak monotonicity of this class of averaging functions and use this to establish robust generalisations of these means. Specifically, we find that as proposed, the density based means are only robust to isolated outliers. However, by using penalty based formalisms of averaging functions and applying more sophisticated and robust density estimators, we are able to define a broader family of density based means that are more effective at filtering both isolated and clustered outliers. © 2014 Elsevier Inc. All rights reserved.

A Harmonized Vocabulary For Water Quality

Interoperability of water quality data depends on the use of common models, schemas and vocabularies. However, terms are usually collected during different activities and projects in isolation of one another, resulting in vocabularies that have the same scope being represented with different terms, using different formats and formalisms, and published in various access methods. Significantly, most water quality vocabularies conflate multiple concepts in a single term, e.g. quantity kind, units of measure, substance or taxon, medium and procedure. This bundles information associated with separate elements from the OGC Observations and Measurements (O&M) model into a single slot. We have developed a water quality vocabulary, formalized using RDF, and published as Linked Data. The terms were extracted from existing water quality vocabularies. The observable property model is inspired by O&M but aligned with existing ontologies. The core is an OWL ontology that extends the QUDT ontology for Unit and QuantityKind definitions. We add classes to generalize the QuantityKind model, and properties for explicit description of the conflated concepts. The key elements are defined to be sub-classes or sub-properties of SKOS elements, which enables a SKOS view to be published through standard vocabulary APIs, alongside the full view. QUDT terms are re-used where possible, supplemented with additional Unit and QuantityKind entries required for water quality. Along with items from separate vocabularies developed for objects, media, and procedures, these are linked into definitions in the actual observable property vocabulary. Definitions of objects related to chemical substances are linked to items from the Chemical Entities of Biological Interest (ChEBI) ontology. Mappings to other vocabularies, such as DBPedia, are in separately maintained files. By formalizing the model for observable properties, and clearly labelling the separate concerns, water quality observations from different sources may be more easily merged and also transformed to O&M for cross-domain applications.

JML- Based formal development of a Java card application for managing medical appointments

Although formal methods can dramatically increase the quality of software systems, they have not widely been adopted in software industry. Many software companies have the perception that formal methods are not cost-effective cause they are plenty of mathematical symbols that are difficult for non-experts to assimilate. The Java Modelling Language (short for JML) Section 3.3 is an academic initiative towards the development of a common formal specification language for Java programs, and the implementation of tools to check program correctness. This master thesis work shows how JML based formal methods can be used to formally develop a privacy sensitive Java application. This is a smart card application for managing medical appointments. The application is named HealthCard. We follow the software development strategy introduced by João Pestana, presented in Section 3.4. Our work influenced the development of this strategy by providing hands-on insight on challenges related to development of a privacy sensitive application in Java. Pestana’s strategy is based on a three-step evolution strategy of software specifications, from informal ones, through semiformal ones, to JML formal specifications. We further prove that this strategy can be automated by implementing a tool that generates JML formal specifications from a welldefined subset of informal software specifications. Hence, our work proves that JML-based formal methods techniques are cost-effective, and that they can be made popular in software industry. Although formal methods are not popular in many software development companies, we endeavour to integrate formal methods to general software practices. We hope our work can contribute to a better acceptance of mathematical based formalisms and tools used by software engineers. The structure of this document is as follows. In Section 2, we describe the preliminaries of this thesis work. We make an introduction to the application for managing medical applications we have implemented. We also describe the technologies used in the development of the application. This section further illustrates the Java Card Remote Method Invocation communication model used in the medical application for the client and server applications. Section 3 introduces software correctness, including the design by contract and the concept of contract in JML. Section 4 presents the design structure of the application. Section 5 shows the implementation of the HealthCard. Section 6 describes how the HealthCard is verified and validated using JML formal methods tools. Section 7 includes some metrics of the HealthCard implementation and specification. Section 8 presents a short example of how a client-side of a smart card application can be implemented while respecting formal specifications. Section 9 describes a prototype tools to generate JML formal specifications from informal specifications automatically. Section 10 describes some challenges and main ideas came acrorss during the development of the HealthCard. The full formal specification and implementation of the HealthCard smart card application presented in this document can be reached at https://sourceforge.net/projects/healthcard/.

Teorias f(R) de gravidade na formulação de Palatini

In this dissertation, after a brief review on the Einstein s General Relativity Theory and its application to the Friedmann-Lemaitre-Robertson-Walker (FLRW) cosmological models, we present and discuss the alternative theories of gravity dubbed f(R) gravity. These theories come about when one substitute in the Einstein-Hilbert action the Ricci curvature R by some well behaved nonlinear function f(R). They provide an alternative way to explain the current cosmic acceleration with no need of invoking neither a dark energy component, nor the existence of extra spatial dimensions. In dealing with f(R) gravity, two different variational approaches may be followed, namely the metric and the Palatini formalisms, which lead to very different equations of motion. We briefly describe the metric formalism and then concentrate on the Palatini variational approach to the gravity action. We make a systematic and detailed derivation of the field equations for Palatini f(R) gravity, which generalize the Einsteins equations of General Relativity, and obtain also the generalized Friedmann equations, which can be used for cosmological tests. As an example, using recent compilations of type Ia Supernovae observations, we show how the f(R) = R − fi/Rn class of gravity theories explain the recent observed acceleration of the universe by placing reasonable constraints on the free parameters fi and n. We also examine the question as to whether Palatini f(R) gravity theories permit space-times in which causality, a fundamental issue in any physical theory [22], is violated. As is well known, in General Relativity there are solutions to the viii field equations that have causal anomalies in the form of closed time-like curves, the renowned Gödel model being the best known example of such a solution. Here we show that every perfect-fluid Gödel-type solution of Palatini f(R) gravity with density and pressure p that satisfy the weak energy condition + p 0 is necessarily isometric to the Gödel geometry, demonstrating, therefore, that these theories present causal anomalies in the form of closed time-like curves. This result extends a theorem on Gödel-type models to the framework of Palatini f(R) gravity theory. We derive an expression for a critical radius rc (beyond which causality is violated) for an arbitrary Palatini f(R) theory. The expression makes apparent that the violation of causality depends on the form of f(R) and on the matter content components. We concretely examine the Gödel-type perfect-fluid solutions in the f(R) = R−fi/Rn class of Palatini gravity theories, and show that for positive matter density and for fi and n in the range permitted by the observations, these theories do not admit the Gödel geometry as a perfect-fluid solution of its field equations. In this sense, f(R) gravity theory remedies the causal pathology in the form of closed timelike curves which is allowed in General Relativity. We also examine the violation of causality of Gödel-type by considering a single scalar field as the matter content. For this source, we show that Palatini f(R) gravity gives rise to a unique Gödeltype solution with no violation of causality. Finally, we show that by combining a perfect fluid plus a scalar field as sources of Gödel-type geometries, we obtain both solutions in the form of closed time-like curves, as well as solutions with no violation of causality

Sete motivações teóricas para o uso da modelagem baseada no indivíduo em ecologia

A modelagem baseada no indivíduo tem sido crescentemente empregada para analisar processos ecológicos, desenvolver e avaliar teorias, bem como para fins de manejo da vida silvestre e conservação. Os modelos baseados no indivíduo (MBI) são bastante flexíveis, permitem o uso detalhado de parâmetros com maior significado biológico, sendo portanto mais realistas do que modelos populacionais clássicos, mais presos dentro de um rígido formalismo matemático. O presente artigo apresenta e discute sete razões para a adoção dos MBI em estudos de simulação na Ecologia: (1) a inerente complexidade de sistemas ecológicos, impassíveis de uma análise matemática formal; (2) processos populacionais são fenômenos emergentes, resultando das interações entre seus elementos constituintes (indivíduos) e destes com o meio; (3) poder de predição; (4) a adoção definitiva, por parte da Ecologia, de uma visão evolutiva; (5) indivíduos são entidades discretas; (6) interações são localizadas no espaço e (7) indivíduos diferem entre si.

Closed string thermal torus from thermo field dynamics

In this Letter a topological interpretation for the string thermal vacuum in the thermo field dynamics (TFD) approach is given. As a consequence, the relationship between the imaginary time and TFD formalisms is achieved when both are used to study closed strings at finite temperature. The TFD approach starts by duplicating the system's degrees of freedom, defining an auxiliary (tilde) string. In order to lead the system to finite temperature a Bogoliubov transformation is implemented. We show that the effect of this transformation is to glue together the string and the tilde string to obtain a torus. The thermal vacuum appears as the boundary state for this identification. Also, from the thermal state condition, a Kubo-Martin-Schwinger condition for the torus topology is derived. © 2005 Elsevier B.V. All rights reserved.

Quantization of the superstring in Ramond-Ramond backgrounds

Sigma model actions are constructed for the type II superstring compactified to four-and six-dimensional curved backgrounds which can contain non-vanishing Ramond-Ramond fields. These actions are N = 2 worldsheet superconformally invariant and can be covariantly quantized preserving manifest spacetime supersymmetry. They are constructed using a hybrid Version of superstring variables which combines features of the Ramond-Neveu-Schwarz and Green-Schwarz formalisms. For the AdS(2) x S-2 and AdS(3) x S-3 backgrounds, these actions differ from the classical Green-Schwarz actions by a crucial kinetic term for the fermions. Parts of this work have been done in collaborations with M Bershadsky, T Hauer, W Siegel, C Vafa, E Witten, S Zhukov and B Zwiebach.

Chiral corrections to baryon properties with composite pions

A calculational scheme is developed to evaluate chiral corrections to properties of composite baryons with composite pions. The composite baryons and pions are bound states derived from a microscopic chiral quark model. The model is amenable to standard many-body techniques such as the BCS and random phase approximation formalisms. An effective chiral model involving only hadronic degrees of freedom is derived from the macroscopic quark model by projection onto hadron states. Chiral loops are calculated using the effective hadronic Hamiltonian. A simple microscopic confining interaction is used to illustrate the derivation of the pion-nucleon form factor and the calculation of picnic self-energy corrections to the nucleon and Delta (1232) masses.

Hamilton-Jacobi approach to Berezinian singular systems

In this work we present a formal generalization of the Hamilton-Jacobi formalism, recently developed For singular systems, to include the case of Lagrangians containing variables which are elements of Berezin algebra. We derive the Hamilton-Jacobi equation for such systems, analyzing the singular case in order to obtain the equations of motion as total differential equations and study the integrability conditions for such equations. An example is solved using both Hamilton-Jacobi and Dirac's Hamiltonian formalisms and the results are compared. (C) 1998 Academic Press.

Search for large extra spatial dimensions in dimuon production with the D0 detector

We present the results of a search for the effects of large extra spatial dimensions in p (p) over bar collisions at root s = 1: 96 TeV in events containing a pair of energetic muons. The data correspond to 246 pb(-1) of integrated luminosity collected by the D0 experiment at the Fermilab Tevatron Collider. Good agreement with the expected background was found, yielding no evidence for large extra dimensions. We set 95% C. L. lower limits on the fundamental Planck scale between 0.85 and 1.27 TeV within several formalisms. These are the most stringent limits achieved in the dimuon channel to date.