1 |
First-order lax logic : a framework for abstraction, constraints and refinementWalton, Matthew January 1998 (has links)
No description available.
|
2 |
Statistics of the Self: Shaping the Self Through Quantified Self-TrackingRowse, Lauren M 01 January 2015 (has links)
Self-tracking practices are growing in popularity worldwide. From heart-rate monitoring to mood tracking, many believe that wearable technologies are making their users more mindful in exclusively positive ways. However, I will argue that consistent and deliberate self-tracking (with or without portable devices) necessitates a particular understanding of the self with consequences that have yet to be fully explored. Through an analysis of forum posts on a popular self-tracking discussion and informational site, QuantifiedSelf.com, I will claim that self-trackers approach the creation of self-knowledge in a manner that is particular to today’s society. I will discuss how the ubiquitous conflation of numerical identities with objective reasoning feeds into a mindset that supports quantification of the self, and how the views of self exhibited by these self-trackers can be considered a version of creating a “scientific self.” The notion of the scientific self supports both an individual and societal shift in the practice of “being”—a shift that carries with it many possible repercussions that have yet to be widely analyzed. This analysis, I will argue, is key to limiting the destructive potential of understanding people in terms of data, while simultaneously enabling new conceptualizations of self to be practiced in modern society.
|
3 |
Självkvantifiering och påverkan av omdöme vid sociala respektive vetenskapligt grundade jämförelser / The quantified self and influence on assessments by social and scientifically based comparisonsBerggrén, Rasmus, Sätterkvist, Arvid January 2015 (has links)
Tjänster för "självkvantifiering" är populära och innefattar ofta funktioner för jämförelser av prestationer användare emellan. När en kultur av jämförelse uppstår finns det risk för att användare bedömer sina prestationer utifrån de normer som bildas i en viss krets ("normerna"). Detta i kontrast till att bedöma prestationer utifrån vetenskapligt motiverade rekommendationer ("rekommendationerna"). Vi ville ta reda på hur användares omdömen påverkas av de två olika grunderna för jämförelse. Vi fokuserade på den enkla självkvantifieringstypen stegräkning. Vi lät 20 personer använda en stegräknare under en veckas tid. Därefter fick de svara på en enkät där de fick se hur de hade presterat (steg/dag i genomsnitt) och där de fick avlägga omdömen om sina prestationer enligt en niogradig skala. Enkäten hade 3 steg: I det första steget fanns ingen grund för jämförelse; i det andra fanns ett diagram för jämförelse med normen (konstruerade data); i det tredje fanns ett diagram för jämförelse med rekommendationen (konstruerade data). Deltagarna var uppdelade i fyra grupper: A (+/+), B (+/-), C (-/+), D (-/-)*. Resultatet blev att både normen och rekommendationen påverkade användarnas omdömen och att normen hade störst betydelse. 69 % (11/16) ändrade sina omdömen efter att ha fått se normen och skillnaden i omdöme var i genomsnitt 1,1 på den niogradiga skalan. Deltagare hade här lättare för att höja omdömet än att sänka det. I grupperna B (+/-) och C (-/+), som fick se en rekommendation som motsade normen, ändrade 63 % (5/8) sina omdömen efter att ha fått se rekommendationen och skillnaden var i genomsnitt 1,0. Rekommendationen påverkade till stor del omdömet i motsatt riktning jämfört med normen. Utifrån våra resultat skulle vi rekommendera att inte bara inkludera jämförelsefunktioner, utan även vetenskapliga rekommendationer, i tjänster för självkvantifiering. Dock är tillförlitligheten hos våra resultat låg, eftersom deltagarna var få och ur en väldigt specifik grupp. Vårt arbete bidrar huvudsakligen med en välgenomtänkt metodik som går att utveckla. * Tecknet innan snedstrecket anger hur gruppen i de konstruerade diagrammen placerades jämfört med normen och tecknet efter hur gruppen placerades jämfört med rekommendationen. Till exempel betyder (+/-) "över normen, under rekommendationen". / "Quantified self" services are popular and often contains features for comparing performances between users. When a comparison culture arises, there is a risk that users assess their performances based on the norms that form in a certain circle ("the norms"). This can be contrasted with assessing performances based on scientifically motivated recommendations ("the recommendations"). We wanted to find out how users’ assessments are affected by the two grounds for comparison. We focused on step-counting, which is a simple form of self-quantification. We let 20 people use a pedometer for a week’s time. They then answered a survey, where they got to see how they had performed (average steps/day) and got to assess their performances on a nine-step scale. The survey had 3 steps: In the first step there were no ground for comparison; in the second one there was a diagram for comparing against the norm (forged data); in the third one there was a diagram for comparing against the recommendation (forged data). The participants were split up into four groups: A (+/+), B (+/-), C (-/+), D (-/-)*. The results were that both the norm and the recommendation affected the users’ assessments and that the norm had the biggest impact. 69 % (11/16) changed their assessments after having seen the norm and the difference in assessment was on average 1.1. Here, participants were more inclined to higher their assessment than to lower it. In groups B (+/-) and C (-/+), that got to see a recommendation that contradicted the norm, 63 % (5/8) changed their assessments after having seen the recommendation and the difference was on average 1.0. The recommendation largely affected the assessment in the opposite direction of the norm. Based on our results, we would recommend including not only comparison features, but also scientific recommendations, in quantified self services. However, the reliability of our results is low, since the participants were few and came from a very specific group. Our work mainly contributes a well-thought-out methodology that can be developed further. * The symbol before the slash indicates how the group was placed in the forged diagrams compared to the norm and the symbol after how the group was placed compared to the recommendation. Example given, (+/-) means "above the norm, below the recommendation".
|
4 |
Quantified self-data och mobilanvändning : Hur kontinuerlig feedback om mobilanvändande inverkar på användarupplevelsen / Quantified self data and smartphone use : How continuous feedback about smartphone usage influence the user experienceFredriksson, Linnéa, Åkesson, Emma January 2018 (has links)
Mobiltelefoner, sociala medier och smarta teknologier är idag en självklar del av tillvaron för många. Samtidigt har överanvändning av mobiltelefoner förknippats med psykisk ohälsa. Som del av utvecklingen av smarta telefoner, appar och tillgången till stora datamängder har även fenomenet att bevaka sina egna vanor med hjälp av tekniken blivit vanligt förekommande. Denna typ av informationsinsamling kallas för quantified self-data och intresset för tekniken är stort. Tidigare forskning om quantified self-data antyder att det skulle kunna vara ett kraftfullt hjälpmedel för en användare som vill förbättra sin livskvalitet. Ett däremot outforskat område är vad som händer med effekterna av quantified self när det ställs mot teknologier som redan vunnit mark i att styra en användares beteende, exempelvis våra smartphones. Denna studie syftade till att utforska detta område och frågan som ställs är hur kontinuerlig feedback i form av quantified self-data, via en mobilapplikation, har för inverkan på en mobilanvändares upplevelse av mobilen och sin användning av den. I studien fick åtta deltagare under två veckor använda sig av mobilapplikationen Moment, som presenterar data om en användares mobilanvändning. Deltagarna ombads även skriva ner dagliga reflektioner i en loggbok. Resultatet visar på att appen tillsammans med loggboken fick deltagarna att aktivt reflektera över sin användning. Deltagarna ansåg att deras användning förblev oförändrad, men att appen och dess data mestadels motiverade till ett minskat användande. Samtliga deltagare trodde att appen var ett bra hjälpmedel för den som vill minska sin mobilanvändning. / Smartphones and social media have become common parts of our everyday life. At the same time, smartphone attachment and overuse have been associated with negative implications on mental health. As a part of the development of smartphones, apps and the access to great amounts of data, the phenomenon of tracking one’s own habits is frequently occurring. This type of data gathering is called quantified self and there is a big interest in the technology. Previous research suggests that quantified self could be a powerful tool for a user wishing to improve his or her life quality. However, the effect of quantified self when put up against technology that is already effective in steering users’ behaviors, such as our smartphones, remains an unexplored subject. This study aimed to explore that subject and the questioned asked is how continuous feedback through quantified self, when presented in a mobile application, influences a smartphone user’s experience of the phone and the usage of it. In the study conducted, eight participants used the application Moment during two weeks, an application which presents the user with data about phone usage. Participants where prompted to write down daily reflections in a journal. The result shows that the app together with the journal made the participants actively reflect on their phone usage. Participants felt that their usage remained unchanged, but that the app mostly motivated them to reduce their usage. All participants thought that the app would be a good aid for those who want to reduce their smartphone usage.
|
5 |
Interpreting "Big Data": Rock Star Expertise, Analytical Distance, and Self-QuantificationWillis, Margaret Mary January 2015 (has links)
Thesis advisor: Natalia Sarkisian / The recent proliferation of technologies to collect and analyze “Big Data” has changed the research landscape, making it easier for some to use unprecedented amounts of real-time data to guide decisions and build ‘knowledge.’ In the three articles of this dissertation, I examine what these changes reveal about the nature of expertise and the position of the researcher. In the first article, “Monopoly or Generosity? ‘Rock Stars’ of Big Data, Data Democrats, and the Role of Technologies in Systems of Expertise,” I challenge the claims of recent scholarship, which frames the monopoly of experts and the spread of systems of expertise as opposing forces. I analyze video recordings (N= 30) of the proceedings of two professional conferences about Big Data Analytics (BDA), and I identify distinct orientations towards BDA practice among presenters: (1) those who argue that BDA should be conducted by highly specialized “Rock Star” data experts, and (2) those who argue that access to BDA should be “democratized” to non-experts through the use of automated technology. While the “data democrats” ague that automating technology enhances the spread of the system of BDA expertise, they ignore the ways that it also enhances, and hides, the monopoly of the experts who designed the technology. In addition to its implications for practitioners of BDA, this work contributes to the sociology of expertise by demonstrating the importance of focusing on both monopoly and generosity in order to study power in systems of expertise, particularly those relying extensively on technology. Scholars have discussed several ways that the position of the researcher affects the production of knowledge. In “Distance Makes the Scholar Grow Fonder? The Relationship Between Analytical Distance and Critical Reflection on Methods in Big Data Analytics,” I pinpoint two types of researcher “distance” that have already been explored in the literature (experiential and interactional), and I identify a third type of distance—analytical distance—that has not been examined so far. Based on an empirical analysis of 113 articles that utilize Twitter data, I find that the analytical distance that authors maintain from the coding process is related to whether the authors include explicit critical reflections about their research in the article. Namely, articles in which the authors automate the coding process are significantly less likely to reflect on the reliability or validity of the study, even after controlling for factors such as article length and author’s discipline. These findings have implications for numerous research settings, from studies conducted by a team of scholars who delegate analytic tasks, to “big data” or “e-science” research that automates parts of the analytic process. Individuals who engage in self-tracking—collecting data about themselves or aspects of their lives for their own purposes—occupy a unique position as both researcher and subject. In the sociology of knowledge, previous research suggests that low experiential distance between researcher and subject can lead to more nuanced interpretations but also blind the researcher to his or her underlying assumptions. However, these prior studies of distance fail to explore what happens when the boundary between researcher and subject collapses in “N of one” studies. In “The Collapse of Experiential Distance and the Inescapable Ambiguity of Quantifying Selves,” I borrow from art and literary theories of grotesquerie—another instance of the collapse of boundaries—to examine the collapse of boundaries in self-tracking. Based on empirical analyses of video testimonies (N=102) and interviews (N=7) with members of the Quantified Self community of self-trackers, I find that ambiguity and multiplicity are integral facets of these data practices. I discuss the implications of these findings for the sociological study of researcher distance, and also the practical implications for the neoliberal turn that assigns responsibility to individuals to collect, analyze, and make the best use of personal data. / Thesis (PhD) — Boston College, 2015. / Submitted to: Boston College. Graduate School of Arts and Sciences. / Discipline: Sociology.
|
6 |
Solving Quantified Boolean FormulasSamulowitz, Horst Cornelius 28 July 2008 (has links)
Abstract
Solving Quantified Boolean Formulas
Horst Samulowitz
Doctor of Philosophy
Graduate Department of Computer Science
University of Toronto
2008
Many real-world problems do not have a simple
algorithmic solution and casting these
problems as search problems is often not only
the simplest way of casting them, but also
the most efficient way of solving them.
In this thesis we will present several
techniques to advance search-based algorithms
in the context of solving quantified boolean
formulas (QBF). QBF enables complex realworld
problems including planning, two-player games
and verification to be captured in a compact
and quite natural fashion. We will discuss
techniques ranging from straight forward
pre-processing methods utilizing strong rules
of inference to more sophisticated online
approaches such as dynamic partitioning.
Furthermore, we will show that all of the
presented techniques achieve an essential
improvement of the search process when
solving QBF. At the same time the displayed
empirical results also reveal the
orthogonality of the different techniques
with respect to performance. Generally
speaking each approach performs well on a
particular subset of benchmarks, but performs
poorly on others. Consequently, an adaptive
employment of the available techniques that
maximizes the performance would result in
further improvements.
We will demonstrate that such an adaptive
approach can pay off in practice, by
presenting the results of using machine
learning methods to dynamically select the
best variable ordering heuristics during
search.
|
7 |
Solving Quantified Boolean FormulasSamulowitz, Horst Cornelius 28 July 2008 (has links)
Abstract
Solving Quantified Boolean Formulas
Horst Samulowitz
Doctor of Philosophy
Graduate Department of Computer Science
University of Toronto
2008
Many real-world problems do not have a simple
algorithmic solution and casting these
problems as search problems is often not only
the simplest way of casting them, but also
the most efficient way of solving them.
In this thesis we will present several
techniques to advance search-based algorithms
in the context of solving quantified boolean
formulas (QBF). QBF enables complex realworld
problems including planning, two-player games
and verification to be captured in a compact
and quite natural fashion. We will discuss
techniques ranging from straight forward
pre-processing methods utilizing strong rules
of inference to more sophisticated online
approaches such as dynamic partitioning.
Furthermore, we will show that all of the
presented techniques achieve an essential
improvement of the search process when
solving QBF. At the same time the displayed
empirical results also reveal the
orthogonality of the different techniques
with respect to performance. Generally
speaking each approach performs well on a
particular subset of benchmarks, but performs
poorly on others. Consequently, an adaptive
employment of the available techniques that
maximizes the performance would result in
further improvements.
We will demonstrate that such an adaptive
approach can pay off in practice, by
presenting the results of using machine
learning methods to dynamically select the
best variable ordering heuristics during
search.
|
8 |
Exploiting Problem Structure in QBF SolvingGoultiaeva, Alexandra 27 March 2014 (has links)
Deciding the truth of a Quantified Boolean Formula (QBF) is a canonical PSPACE-complete problem. It provides a powerful framework for encoding problems that lie in PSPACE. These include many problems in automatic verification, and problems with discrete uncertainty or non-determinism. Two person adversarial games are another type of problem that are naturally encoded in QBF.
It is standard practice to use Conjunctive Normal Form (CNF) when representing QBFs. Any propositional formula can be efficiently translated to CNF via the addition of new variables, and solvers can be implemented more efficiently due to the structural simplicity of CNF. However, the translation to CNF involves a loss of some structural information. This thesis shows that this structural information is important for efficient QBF solving, and shows how this structural information can be utilized to improve state-of-the-art QBF solving.
First, a non-CNF circuit-based solver is presented. It makes use of information not present in CNF to improve its performance. We present techniques that allow it to exploit the duality between solutions and conflicts that is lost when working with CNF. This duality can also be utilized in the production of certificates, allowing both true and false formulas to have easy-to-verify certificates of the same form.
Then, it is shown that most modern CNF-based solvers can benefit from the additional information derived from duality using only minor modifications. Furthermore, even partial duality information can be helpful. We show that for standard methods for conversion to CNF, some of the required information can be reconstructed from the CNF and greatly benefit the solver.
|
9 |
Exploiting Problem Structure in QBF SolvingGoultiaeva, Alexandra 27 March 2014 (has links)
Deciding the truth of a Quantified Boolean Formula (QBF) is a canonical PSPACE-complete problem. It provides a powerful framework for encoding problems that lie in PSPACE. These include many problems in automatic verification, and problems with discrete uncertainty or non-determinism. Two person adversarial games are another type of problem that are naturally encoded in QBF.
It is standard practice to use Conjunctive Normal Form (CNF) when representing QBFs. Any propositional formula can be efficiently translated to CNF via the addition of new variables, and solvers can be implemented more efficiently due to the structural simplicity of CNF. However, the translation to CNF involves a loss of some structural information. This thesis shows that this structural information is important for efficient QBF solving, and shows how this structural information can be utilized to improve state-of-the-art QBF solving.
First, a non-CNF circuit-based solver is presented. It makes use of information not present in CNF to improve its performance. We present techniques that allow it to exploit the duality between solutions and conflicts that is lost when working with CNF. This duality can also be utilized in the production of certificates, allowing both true and false formulas to have easy-to-verify certificates of the same form.
Then, it is shown that most modern CNF-based solvers can benefit from the additional information derived from duality using only minor modifications. Furthermore, even partial duality information can be helpful. We show that for standard methods for conversion to CNF, some of the required information can be reconstructed from the CNF and greatly benefit the solver.
|
10 |
Doing the self : an ethnographic analysis of the quantified selfDudhwala, Farzana January 2017 (has links)
'Wearables' and 'self-quantifying technologies' are becoming ever more popular and normalised in society as a means of 'knowing' the self. How are these technologies implicated in this endeavour? Using insights from a four year multi-sited ethnography of the 'Quantified Self', I explore how the self is 'done' in the context of using technologies that purport to quantify the self in some way. Drawing on Science and Technology Studies (STS) sensibilities, I conduct a four- pronged investigation into 'self-making' by drawing upon, and expanding, existing theories of agency and performativity, number, data-visualisation, and enactment. I find that self-quantifying technologies are productive in the doing of the self and are implicated in the process of making boundaries around that which comes to be known as the 'self' in a particular moment. The numbers and visualisations that result from practices of self-quantification enable a new way of 'seeing' the self, and provide a way of communicating this self with others. The self is thus not a pre-existing entity that simply requires these technologies as a means to 'know' it. Rather, the self is constantly being done with these technologies and within the surrounding practices of self-quantification. In order to highlight the different parts of this process, I proffer the term 'entractment'. This term explains how these different elements come together to culminate in the production of a momentarily constant self in a particular context. It is a way of simultaneously encapsulating the processes of intra-action, extra-action and enactment with/in a community. In sum, it captures the conclusion that, in the context of self-quantification, we must understand the self as a collective enactment, achieved, at least in part, through the use of self-quantifying technologies that produce numerical data which facilitate visualisations that are imperative to the doing of the self.
|
Page generated in 0.0445 seconds