Approximate knowledge of rationality and correlated equilibria

We extend Aumann's [3] theorem deriving correlated equilibria as a consequence of common priors and common knowledge of rationality by explicitly allowing for non-rational behavior. We replace the assumption of common knowledge of rationality with a substantially weaker notion, joint p-belief of rationality, where agents believe the other agents are rational with probabilities p = (pi)i2I or more. We show that behavior in this case constitutes a constrained correlated equilibrium of a doubled game satisfying certain p-belief constraints and characterize the topological structure of the resulting set of p-rational outcomes. We establish continuity in the parameters p and show that, for p su ciently close to one, the p-rational outcomes are close to the correlated equilibria and, with high probability, supported on strategies that survive the iterated elimination of strictly dominated strategies. Finally, we extend Aumann and Dreze's [4] theorem on rational expectations of interim types to the broader p-rational belief systems, and also discuss the case of non-common priors.

Invariant-free deduction systems for temporal logic

In this thesis we propose a new approach to deduction methods for temporal logic. Our proposal is based on an inductive definition of eventualities that is different from the usual one. On the basis of this non-customary inductive definition for eventualities, we first provide dual systems of tableaux and sequents for Propositional Linear-time Temporal Logic (PLTL). Then, we adapt the deductive approach introduced by means of these dual tableau and sequent systems to the resolution framework and we present a clausal temporal resolution method for PLTL. Finally, we make use of this new clausal temporal resolution method for establishing logical foundations for declarative temporal logic programming languages. The key element in the deduction systems for temporal logic is to deal with eventualities and hidden invariants that may prevent the fulfillment of eventualities. Different ways of addressing this issue can be found in the works on deduction systems for temporal logic. Traditional tableau systems for temporal logic generate an auxiliary graph in a first pass.Then, in a second pass, unsatisfiable nodes are pruned. In particular, the second pass must check whether the eventualities are fulfilled. The one-pass tableau calculus introduced by S. Schwendimann requires an additional handling of information in order to detect cyclic branches that contain unfulfilled eventualities. Regarding traditional sequent calculi for temporal logic, the issue of eventualities and hidden invariants is tackled by making use of a kind of inference rules (mainly, invariant-based rules or infinitary rules) that complicates their automation. A remarkable consequence of using either a two-pass approach based on auxiliary graphs or aone-pass approach that requires an additional handling of information in the tableau framework, and either invariant-based rules or infinitary rules in the sequent framework, is that temporal logic fails to carry out the classical correspondence between tableaux and sequents. In this thesis, we first provide a one-pass tableau method TTM that instead of a graph obtains a cyclic tree to decide whether a set of PLTL-formulas is satisfiable. In TTM tableaux are classical-like. For unsatisfiable sets of formulas, TTM produces tableaux whose leaves contain a formula and its negation. In the case of satisfiable sets of formulas, TTM builds tableaux where each fully expanded open branch characterizes a collection of models for the set of formulas in the root. The tableau method TTM is complete and yields a decision procedure for PLTL. This tableau method is directly associated to a one-sided sequent calculus called TTC. Since TTM is free from all the structural rules that hinder the mechanization of deduction, e.g. weakening and contraction, then the resulting sequent calculus TTC is also free from this kind of structural rules. In particular, TTC is free of any kind of cut, including invariant-based cut. From the deduction system TTC, we obtain a two-sided sequent calculus GTC that preserves all these good freeness properties and is finitary, sound and complete for PLTL. Therefore, we show that the classical correspondence between tableaux and sequent calculi can be extended to temporal logic. The most fruitful approach in the literature on resolution methods for temporal logic, which was started with the seminal paper of M. Fisher, deals with PLTL and requires to generate invariants for performing resolution on eventualities. In this thesis, we present a new approach to resolution for PLTL. The main novelty of our approach is that we do not generate invariants for performing resolution on eventualities. Our method is based on the dual methods of tableaux and sequents for PLTL mentioned above. Our resolution method involves translation into a clausal normal form that is a direct extension of classical CNF. We first show that any PLTL-formula can be transformed into this clausal normal form. Then, we present our temporal resolution method, called TRS-resolution, that extends classical propositional resolution. Finally, we prove that TRS-resolution is sound and complete. In fact, it finishes for any input formula deciding its satisfiability, hence it gives rise to a new decision procedure for PLTL. In the field of temporal logic programming, the declarative proposals that provide a completeness result do not allow eventualities, whereas the proposals that follow the imperative future approach either restrict the use of eventualities or deal with them by calculating an upper bound based on the small model property for PLTL. In the latter, when the length of a derivation reaches the upper bound, the derivation is given up and backtracking is used to try another possible derivation. In this thesis we present a declarative propositional temporal logic programming language, called TeDiLog, that is a combination of the temporal and disjunctive paradigms in Logic Programming. We establish the logical foundations of our proposal by formally defining operational and logical semantics for TeDiLog and by proving their equivalence. Since TeDiLog is, syntactically, a sublanguage of PLTL, the logical semantics of TeDiLog is supported by PLTL logical consequence. The operational semantics of TeDiLog is based on TRS-resolution. TeDiLog allows both eventualities and always-formulas to occur in clause heads and also in clause bodies. To the best of our knowledge, TeDiLog is the first declarative temporal logic programming language that achieves this high degree of expressiveness. Since the tableau method presented in this thesis is able to detect that the fulfillment of an eventuality is prevented by a hidden invariant without checking for it by means of an extra process, since our finitary sequent calculi do not include invariant-based rules and since our resolution method dispenses with invariant generation, we say that our deduction methods are invariant-free.

Semi-automatic generation of learning domain modules for technology supported learning systems

In a time when Technology Supported Learning Systems are being widely used, there is a lack of tools that allows their development in an automatic or semi-automatic way. Technology Supported Learning Systems require an appropriate Domain Module, ie. the pedagogical representation of the domain to be mastered, in order to be effective. However, content authoring is a time and effort consuming task, therefore, efforts in automatising the Domain Module acquisition are necessary.Traditionally, textbooks have been used as the main mechanism to maintain and transmit the knowledge of a certain subject or domain. Textbooks have been authored by domain experts who have organised the contents in a means that facilitate understanding and learning, considering pedagogical issues.Given that textbooks are appropriate sources of information, they can be used to facilitate the development of the Domain Module allowing the identification of the topics to be mastered and the pedagogical relationships among them, as well as the extraction of Learning Objects, ie. meaningful fragments of the textbook with educational purpose.Consequently, in this work DOM-Sortze, a framework for the semi-automatic construction of Domain Modules from electronic textbooks, has been developed. DOM-Sortze uses NLP techniques, heuristic reasoning and ontologies to fulfill its work. DOM-Sortze has been designed and developed with the aim of automatising the development of the Domain Module, regardless of the subject, promoting the knowledge reuse and facilitating the collaboration of the users during the process.

An observer-based vaccination control law for an SEIR epidemic model based on feedback linearization techniques for nonlinear systems

This paper presents a vaccination strategy for fighting against the propagation of epidemic diseases. The disease propagation is described by an SEIR (susceptible plus infected plus infectious plus removed populations) epidemic model. The model takes into account the total population amounts as a refrain for the illness transmission since its increase makes the contacts among susceptible and infected more difficult. The vaccination strategy is based on a continuous-time nonlinear control law synthesised via an exact feedback input-output linearization approach. An observer is incorporated into the control scheme to provide online estimates for the susceptible and infected populations in the case when their values are not available from online measurement but they are necessary to implement the control law. The vaccination control is generated based on the information provided by the observer. The control objective is to asymptotically eradicate the infection from the population so that the removed-by-immunity population asymptotically tracks the whole one without precise knowledge of the partial populations. The model positivity, the eradication of the infection under feedback vaccination laws and the stability properties as well as the asymptotic convergence of the estimation errors to zero as time tends to infinity are investigated.

Global Self-Organization of the Cellular Metabolic Structure

Background: Over many years, it has been assumed that enzymes work either in an isolated way, or organized in small catalytic groups. Several studies performed using "metabolic networks models'' are helping to understand the degree of functional complexity that characterizes enzymatic dynamic systems. In a previous work, we used "dissipative metabolic networks'' (DMNs) to show that enzymes can present a self-organized global functional structure, in which several sets of enzymes are always in an active state, whereas the rest of molecular catalytic sets exhibit dynamics of on-off changing states. We suggested that this kind of global metabolic dynamics might be a genuine and universal functional configuration of the cellular metabolic structure, common to all living cells. Later, a different group has shown experimentally that this kind of functional structure does, indeed, exist in several microorganisms. Methodology/Principal Findings: Here we have analyzed around 2.500.000 different DMNs in order to investigate the underlying mechanism of this dynamic global configuration. The numerical analyses that we have performed show that this global configuration is an emergent property inherent to the cellular metabolic dynamics. Concretely, we have found that the existence of a high number of enzymatic subsystems belonging to the DMNs is the fundamental element for the spontaneous emergence of a functional reactive structure characterized by a metabolic core formed by several sets of enzymes always in an active state. Conclusions/Significance: This self-organized dynamic structure seems to be an intrinsic characteristic of metabolism, common to all living cellular organisms. To better understand cellular functionality, it will be crucial to structurally characterize these enzymatic self-organized global structures.

An enactive and dynamical systems theory account of dyadic relationships

Many social relationships are a locus of struggle and suffering, either at the individual or interactional level. In this paper we explore why this is the case and suggest a modeling approach for dyadic interactions and the well-being of the participants. To this end we bring together an enactive approach to self with dynamical systems theory. Our basic assumption is that the quality of any social interaction or relationship fundamentally depends on the nature and constitution of the individuals engaged in these interactions. From an enactive perspective the self is conceived as an embodied and socially enacted autonomous system striving to maintain an identity. This striving involves a basic two-fold goal: the ability to exist as an individual in one's own right, while also being open to and affected by others. In terms of dynamical systems theory one can thus consider the individual self as a self-other organized system represented by a phase space spanned by the dimensions of distinction and participation, where attractors can be defined. Based on two everyday examples of dyadic relationship we propose a simple model of relationship dynamics, in which struggle or well-being in the dyad is analyzed in terms of movements of dyadic states that are in tension or in harmony with individually developed attractors. Our model predicts that relationships can be sustained when the dyad develops a new joint attractor toward which dyadic states tend to move, and well-being when this attractor is in balance with the individuals' attractors. We outline how this can inspire research on psychotherapy. The psychotherapy process itself provides a setting that supports clients to become aware how they fare with regards to the two-fold norm of distinction and participation and develop, through active engagement between client (or couple) and therapist, strategies to co-negotiate their self-organization.