Soccer players inescapably live under stress during the sportive career, and many real-life aspects of soccer situations operate in the ongoing performance. This study’s main objective was to elaborate the List of Stressors in Professional Indoor and Field Soccer, a self-report instrument designed to measure the impact of 77 soccer situations upon the sport performance. Participants were 138 indoor and field soccer players from the Brazilian Premier League. Each situation was evaluated on a 7-point scale, ranging from the most negative (...) to the most positive. Data were analyzed according to the players’ perception of the items: distress or eustress and its intensity, and after that, situations perceived as plus −1 and +1 were compared by time in which they were experienced and distributed among five categories established by the literature: Expectations about the Performance, Personal Factors, Competition Aspects, Training Demands, and Relationship with Significant People. Narratives of athletes’ experiences were also used to discuss the results. An Exploratory Structural Equation Modeling using Bi-factorial was employed to assess the factor structure. For the total participants, 49 situations were perceived as distress and 28 as eustress. Using the criteria established a priori, the distribution was among the five categories in the remaining 32 situations. Differences in perception between less and more experienced players were found in 11 situations. The results revealed that Brazilian professional soccer players experience various stressful situations. These events are important representations of environmental demands and could predict the performance as they are perceived as eustress or distress. Some of these stressful situations are inherent in sport and others adjacent to the sports system or environment. Coach pressure to win and conflicts with teammates are examples of stressors in-sport, family problems and disputes with press or fans are examples of stressors external to the team, also called peripheral opponents, and showed the relative social influence of significant others in soccer performance. We can conclude that the knowledge of the direction of a given stress situation has important practical implications in preparing athletes and helping them face the performance stressors that are part of soccer daily life. (shrink)

Did you know that Hillary Clinton sold weapons to ISIS? Or that Mike Pence called Michelle Obama “the most vulgar First Lady we’ve ever had”? No, you didn’t know these things. You couldn’t know them, because these claims are false.1 But many American voters believed them.One of the most distinctive features of the 2016 campaign was the rise of “fake news,” factually false claims circulated on social media, usually via channels of partisan camaraderie. Media analysts and social scientists are still (...) debating what role fake news played in Trump’s victory.2 But whether or not it drove the outcome, fake news certainly affected the choices of some individual voters.Why were people willing to believe easily... (shrink)

Deepfake technology uses machine learning to fabricate video and audio recordings that represent people doing and saying things they've never done. In coming years, malicious actors will likely use this technology in attempts to manipulate public discourse. This paper prepares for that danger by explicating the unappreciated way in which recordings have so far provided an epistemic backstop to our testimonial practices. Our reasonable trust in the testimony of others depends, to a surprising extent, on the regulative effects of the (...) ever-present possibility of recordings of the events they testify about. As deepfakes erode the epistemic value of recordings, we may then face an even more consequential challenge to the reliability of our testimonial practices themselves. (shrink)

Lean is a new open source theorem prover being developed at Microsoft Research and Carnegie Mellon University, with a small trusted kernel based on dependent type theory. It aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. Lean is an ongoing and long-term effort, but it already provides many useful components, integrated development environments, and a rich API (...) which can be used to embed it into other systems. It is currently being used to formalize category theory, homotopy type theory, and abstract algebra. We describe the project goals, system architecture, and main features, and we discuss applications and continuing work. (shrink)

Slips of the tongue, unwitting favoritism and stereotyped assumptions are just some examples of microaggression. Nearly all of us commit microaggressions at some point, even if we don’t intend to. Yet over time a pattern of microaggression can cause considerable harm by reminding members of marginalized groups of their precarious position. The Ethics of Microaggression is a much needed and clearly written exploration of this pervasive yet complex problem. What is microaggression and how do we know when it is occurring? (...) Can we be held responsible for microaggressions and if so, how? How has social media affected the problem? What role can philosophy play in understanding microaggression? Regina Rini explores these highly topical and controversial questions in an engaging and fair-minded way, arguing that an event is a microaggression precisely because it causes a marginalized person to experience an ambiguous encounter with oppression. She illustrates her argument with compelling examples from media, politics and psychology and explains the significance of essential concepts, such as media representation, reparative renaming, and safe spaces. The Ethics of Microaggression explains what microaggression is and offers strategies for combating it. Assuming no prior knowledge of the topic or philosophy, it demystifies a controversial and extremely important topic in clear language. It is ideal for anyone coming to the topic for the first time and for students in philosophy, gender studies, race theory, disability theory and social and political philosophy. (shrink)

Deepfakes are algorithmically modified video and audio recordings that project one person’s appearance on to that of another, creating an apparent recording of an event that never took place. Many scholars and journalists have begun attending to the political risks of deepfake deception. Here we investigate other ways in which deepfakes have the potential to cause deeper harms than have been appreciated. First, we consider a form of objectification that occurs in deepfaked ‘frankenporn’ that digitally fuses the parts of different (...) women to create pliable characters incapable of giving consent to their depiction. Next, we develop the idea of ‘illocutionary wronging’, in which an individual is forced to engage in speech acts they would prefer to avoid in order to deny or correct the misleading evidence of a publicized deepfake. Finally, we consider the risk that deepfakes may facilitate campaigns of ‘panoptic gaslighting’, where many systematically altered recordings of a single person's life undermine their memory, eroding their sense of self and ability to engage with others. Taken together, these harms illustrate the roles that social epistemology and technological vulnerabilities play in human ethical life. (shrink)

Children with HIV are dependent on taking continuous medication and care, and family preparation is required when disclosing HIV. This study aimed to unveil families’ experiences with HIV disclosure to children under 13 years old. Eight family members who have disclosed HIV to seropositive children were interviewed in‐depth and individually. The fieldwork took place at a public paediatric outpatient hospital in Rio de Janeiro. The results showed that the family members’ discourse highlighted two ways of knowing their own condition and (...) disclosing the condition of the children with HIV. First, they needed to address the communication of bad news and discover their own HIV status through their children's disease. Second, the disclosure was a process constituted by four stages: preparing for disclosure, identifying the time, deciding how and where to tell, and instilling silence after disclosure. They also recognized that nurses had a role in the process as part of an interprofessional team. Nurses can develop advocacy care and empower family members in the preparation of safe HIV disclosure. By systematizing and institutionalizing the care advocacy process, nurses may enable caretakers and children to participate in their therapeutic management, improving adherence to the treatment and self‐care with autonomy. (shrink)

Contemporary and emerging chatbots can be fine-tuned to imitate the style, tenor, and knowledge of a corpus, including the corpus of a particular individual. This makes it possible to build chatbots that imitate people who are no longer alive — deathbots. Such deathbots can be used in many ways, but one prominent way is to facilitate the process of grieving. In this paper, we present a framework that helps make sense of this process. In particular, we argue that deathbots can (...) serve as affective scaffolds, modulating and shaping the emotions of the bereaved. We contextualize this affective scaffolding by comparing it to earlier technologies that have also been used to scaffold the process of grieving, arguing that deathbots offer some interesting novelties that may transform the continuing bonds of intimacy that the bereaved can have with the dead. We conclude with some ethical reflections on the promises and perils of this new technology. (shrink)

Since at least 2016, many have worried that social media enables authoritarians to meddle in democratic politics. The concern is that trolls and bots amplify deceptive content. In this chapter I argue that these tactics have a more insidious anti-democratic purpose. Lies implanted in democratic discourse by authoritarians are often intended to be caught. Their primary goal is not to successfully deceive, but rather to undermine the democratic value of testimony. In well-functioning democracies, our mutual reliance on testimony also generates (...) a distinctively democratic value: decentralized testimonial networks evade control by the state or powerful actors. The deliberate exposure of deception in democratic testimonial networks undermines this value by implicating citizens in their own epistemic corruption, weakening the resilience of democratic society against authoritarian pressure. In this chapter I illustrate that danger through a close reading of recent Russian social media interference operations, showing both their epistemic underpinnings and their ongoing political threat. (shrink)

Many of our cognitive capacities are the result of enculturation. Enculturation is the temporally extended transformative acquisition of cognitive practices in the cognitive niche. Cognitive practices are embodied and normatively constrained ways to interact with epistemic resources in the cognitive niche in order to complete a cognitive task. The emerging predictive processing perspective offers new functional principles and conceptual tools to account for the cerebral and extra-cerebral bodily components that give rise to cognitive practices. According to this emerging perspective, many (...) cases of perception, action, and cognition are realized by the on-going minimization of prediction error. Predictive processing provides us with a mechanistic perspective that helps investigate the functional details of the acquisition of cognitive practices. The argument of this paper is that research on enculturation and recent work on predictive processing are complementary. The main reason is that predictive processing operates at a sub-personal level and on a physiological time scale of explanation only. A complete account of enculturated cognition needs to take additional levels and temporal scales of explanation into account. This complementarity assumption leads to a new framework—enculturated predictive processing—that operates on multiple levels and temporal scales for the explanation of the enculturated predictive acquisition of cognitive practices. Enculturated predictive processing is committed to explanatory pluralism. That is, it subscribes to the idea that we need multiple perspectives and explanatory strategies to account for the complexity of enculturation. The upshot is that predictive processing needs to be complemented by additional considerations and conceptual tools to realize its full explanatory potential. (shrink)

Timothy Williamson has brought valuable contributions to the understanding of the relationship between vagueness and knowledge. The philosopher argues that for a belief in a vague proposition to be considered knowledge, it is essential that it is not too close to indefinite conceptual boundaries. Williamson warns that even true beliefs can be merely coincidentally true if there is not an adequate margin of safety against error. Williamson argues that in sorites situations, problems extend beyond semantics to encompass epistemic issues. The (...) author concludes that true beliefs, when too close to vague boundaries, are essentially true by chance, rendering them unsuitable for being considered knowledge. However, it is emphasized that vagueness is not a universal boundary and recognizes the existence of vague terms with relative and absolute boundary cases. While the former have uncertain application due to the lack of decisive methods for their use, the latter face an inherent incompleteness in the question. In summary, we will explore the essence of Williamson's argument, using simple and everyday examples to unravel the complexities of the relationship between vagueness and knowledge. (shrink)

O objetivo deste artigo é discutir o modo como Husserl desenha a originalidade da subjetividade transcendental, frente à sua homônima psicológica. Se é certo que a noção de “imanência autêntica” pode apontar para as diferentes fronteiras entre o transcendental e o psicológico, resta que por si só ela não permite decidir nada quanto ao “modo de ser” transcendental, em sua diferença face ao “mundano”. Sendo assim, procura-se reconstituir alguns dos momentos centrais do esforço husserliano para construir um conceito de “subjetivo” (...) e de “subjetividade” que não se confunda mais com o “psíquico” da psicologia tradicional. (shrink)

Recent empirical work appears to suggest that the moral intuitions of professional philosophers are just as vulnerable to distorting psychological factors as are those of ordinary people. This paper assesses these recent tests of the ‘expertise defense’ of philosophical intuition. I argue that the use of familiar cases and principles constitutes a methodological problem. Since these items are familiar to philosophers, but not ordinary people, the two subject groups do not confront identical cognitive tasks. Reflection on this point shows that (...) these findings do not threaten philosophical expertise—though we can draw lessons for more effective empirical tests. (shrink)

Husserlian phenomenology has been interpreted as a method of knowledge that can be applied to different domains and which would compete with other methods to give us a better understanding of the “real”, the “man” or “society”. Moreover, “phenomenological idealism” has been presented as an “ontological” or “metaphysical” thesis, in the pre-critical sense of the term. The goal of this study is to suggest that these two theses imply the tacit identification of the natural attitude and the phenomenological one, avoiding (...) the difference between the objects to which these attitudes relate. Therefore, a phenomenological truth does not anticipate any opinion about the “world”. (shrink)

O artigo visa estabelecer a ideia de valor e sua formação, tomando como base o livro “Les Mots et Les Choses” de Michel Foucault, explorando a concepção epistemológica das coisas no âmbito político-econômico-informacional. A metodologia utilizada neste artigo, segue a leitura sintópica da fonte bibliográfica indicada, complementada pela análise conceitual dos capítulos “Échanger” e “Travail, Vie et Langage” da obra, na transversalidade disciplinar, integrando a filosofia da informação e a economia política, numa perspectiva que articula as dimensões da semiótica com (...) a teoria do valor econômico no campo informacional da epistemologia das coisas. (shrink)

Neste artigo, buscaremos discutir o modo pelo qual a literatura pode conduzir – e, talvez, mesmo exigir – uma mudança no próprio estatuto da filosofia, especialmente no caso da fenomenologia, ao tornar explícita a existência de um outro modelo de racionalidade, distinto de sua concepção clássica. Para isso, trabalharemos a partir das descrições propostas por Merleau-Ponty sobre o tema, concentrando-nos, nesse artigo, no período de sua obra entre o final dos anos quarenta e início dos anos cinquenta. Ao lado da (...) questão da literatura, a correlata recompreensão da noção de metafísica terá papel central nessa investigação. (shrink)

A microaggression is a small insulting act made disproportionately harmful by its part in an oppressive pattern of similar insults. How should you respond when made the victim of a microaggression? In this paper I survey several morally salient factors, including effects upon victims, perpetrators, and third parties. I argue, contrary to popular views, that ‘growing a thicker skin’ is not good advice nor is expressing reasonable anger always the best way to contribute to confronting oppression. Instead, appropriately responding to (...) microaggression involves difficult application of practical wisdom that does not easily fall under a simple prescription. (shrink)

Nesta apresentação, breve homenagem ao professor Franklin Leopoldo e Silva, nossa proposta é investigar o modo pelo qual o autor compreende a relação entre literatura e filosofia, sobretudo a partir de certa aproximação proposta por ele entre a obra de Proust e o pensamento de Bergson. Para essa discussão, nos apoiamos aqui especialmente em seu ensaio Bergson, Proust: tensões do tempo.

Husserl places “around 1898” the introduction of the notion of ‘ phenomenon’ in his philosophy. If one of the tasks of the history of philosophy is to circumscribe the problems which originated the creation of a new concept in some doctrine, the purpose of this paper is to investigate what difficulties had roused the invention of the idea of ‘phenomenon” in the husserlian philosophy.

Este artigo busca tratar da aproximação entre linguagem e pintura proposta por Merleau-Ponty, buscando mostrar que ela se baseia no reconhecimento de um vínculo intrínseco existente entre a percepção e a expressão e, por meio dele, de uma passividade inerente a toda criação. Trabalharemos, desse modo, a compreensão do filósofo de que é impossível manter os pressupostos da ontologia dualista que opera com a distinção completa entre o subjetivo e o objetivo, na medida em que a estrutura perceptiva explicita um (...) movimento significativo que desconhece a antinomia dos termos, oferecendo-se como solo comum que tanto a pintura quanto a linguagem retomam, revelando ambas não como constituição pura, mas como transformação e subversão. (shrink)

Apresentaremos as possíveis aplicações pedagógicas das suas reflexões, como a utilização da imprecisão científica de Heisenberg e da concepção de técnica em Heidegger, a partir da análise histórico-filosófica dos seus escritos, tomando-os como fundamentação a necessária e significativa melhoria da educação técnico-científica.

Este artigo tem como objetivo principal investigar a relação existente entre a percepção da felicidade dos brasileiros, sua satisfação com a vida e a satisfação com o regime democrático no período de 2017 a 2020. Nossa hipótese de trabalho postula que o declínio da felicidade e da satisfação com a vida, de uma forma geral, guarda relação de associação com a satisfação com a democracia e suas instituições. Assim, o artigo sugere que felicidade e democracia no Brasil são duas variáveis (...) associadas que ajudam a explicar em parte as fragilidades de nosso regime democrático e devem ser foco de atenção de nossas políticas públicas. A base empírica deste artigo é a sétima onda da Pesquisa Mundial de Valores (WVS, 2017-2020), por meio de pesquisa quantitativa, tipo survey, que utilizaremos para demonstrar nosso argumento. (shrink)

Compreender a violência na sociedade contemporânea requer o mapeamento dos fatores geradores de atos violentos bem como sua prevenção por meio de políticas públicas e de processos educacionais. Este artigo traz algumas reflexões sobre a racionalidade comunicativa e a violência escolar no contexto da crescente exclusão social e a crise de horizontes utópicos para a construção da educação e da formação de sujeitos de direitos. A abordagem metodológica está ancorada na perspectiva da análise de conteúdo de Laurence Bardin (2016), do (...) documento ‘Violência escolar e bullying: relatório sobre a situação mundial’, publicado pela Organização das Nações Unidas para a Educação, a Ciência e a Cultura (UNESCO). São analisadas as pretensões de validade das informações e dos dados considerados relevantes por meio da elaboração de dois eixos principais para analisar a violência escolar apresentada no relatório: a) definições e amparos legais; b) impactos e principais desafios sobre a violência escolar e o bullying. Nessa perspectiva, recorreremos à Racionalidade Comunicativa, ponto central da Teoria do Agir Comunicativo, de Jürgen Habermas, para refletir sobre os achados e saber quais as bases consideradas relevantes para se construir uma educação para a paz alicerçada no diálogo e no entendimento. (shrink)

Este texto procura circunscrever alguns traços de um tipo de racionalidade formal, que encontra no cinismo uma de suas expressões privilegiadas. Buscamos delimitar algumas características do modo de operação dessa razão, sobretudo enquanto negatividade ou recusa da significação própria ao seu objeto e, no limite, ao mundo. Nessa direção, tentamos, ainda, apontar alguns limites para esse projeto de formalização total e de negação completa do mundo enquanto tal.

The aim of this paper is to expose an idea of causality present in Marx’s conception, considering some of his claims regarding history. Precisely, claims regarding modes of production as progressive epochs of human society, present in the Preface of 1859. With this I intend to maintain that Marx still resorts to an idea of causality in a strong sense, closer to natural sciences. I think that the use of this category as a theoretical resource goes against the idea of (...) a social philosophy as a social science; to which all causality is not foreign, but it is convenient to take it in a weak sense. Because I intend to consider the idea of causality without forgetting to consider the idea of unpredictability as a significant marker regarding the human sciences. (shrink)

Although there is broad support in the current Brazilian legislation and many curricular documents published in the last three decades, we still face the challenge of the inclusive education in our classrooms. This is a qualitative research in which we investigate the perception of three school pedagogical coordinators about the inclusion of disabled children in regular classes of Elementary and High School of the schools that self-declared favorable to the Inclusive Education. The results suggest perceptions of Inclusive Education with specific (...) goal to comply with current legislation, which aims exclusively at the socialization of the disabled as a target of charity, without great teaching learning goals that allow equal access to school knowledge and continuity of study in the educational system. (shrink)

O artigo está contextualizado no âmbito do debate da filosofia política acerca do cosmopolitismo, isto é, de uma orientação politico-filosófica que considera que teorias de justiça devem ir além das fronteiras nacionais em suas abordagens. Propostas normativas liberais (tais como as de Thomas Pogge e Charles Beitz) recolocaram como foco central da preocupação com a justiça a esfera global e ocuparam o protagonismo dos debates no âmbito da filosofia política no final da década de noventa. Já no campo crítico-discursivo, o (...) ideal cosmopolita foi tematizado de forma menos sistemática, com exceções, como Seyla Benhabib e Jurgen Habermas. Mais recentemente Brian Milstein (2015), efetua o resgate do ideal cosmopolita e estabelece de que forma a teoria crítica com um ponto de vista cosmopolita é central para se pensar possibilidades emancipatórias. Neste texto irei apresentar as principais discussões e desafios que as teorias cosmopolitas enfrentaram e demonstrarei os elementos centrais da proposta de Milstein tendo como objetivo central sustentar que o projeto cosmopolita não deve ser descartado, ao contrário, trata-se de perspectiva urgente para pensarmos os principais desafios de justiça de nosso tempo. (shrink)

This short piece draws on political philosophy to show how social media interference operations can be used by hostile states to weaken the apparent legitimacy of democratic governments. Democratic societies are particularly vulnerable to this form of attack because democratic governments depend for their legitimacy on citizens' trust in one another. But when citizen see one another as complicit in the distribution of deceptive content, they lose confidence in the epistemic preconditions for democracy. The piece concludes with policy recommendations for (...) how democratic governments should protect themselves. (shrink)

O artigo visa discutir o papel que a obra de John Rawls possui para o projeto teórico de Rainer Forst. Trata-se de acompanharas principaisleituras que Forst realiza sobre esse autor e discutir algumas consequências que podem ser delas depreendidas para seu modelo crítico. Assim, em primeiro lugar, discute-se a tentativa de Forst em aproximar os critérios de reciprocidade e universalidade, de seu princípio de justificação, à teoria de Rawls, ao mesmo tempo em que acusa Rawls de que sua configuração da (...) posição original atribui conteúdos substantivos aos princípios de justiça, que, na verdade, só poderiam ser concebidos comoum princípio fundamental de justificação (I). Em seguida, observa-se a leitura que Forst realiza sobre o debate entre Habermas e Rawls, a fim de extrair uma alternativa a ambos. Novamente Forst faz um movimento de aproximação e crítica a Rawls (II). Em um terceiro momento, examina-se outra tentativa de aproximação e superação à obra de Rawls, mas dessa vezatravés da distinção entre duas imagens da justiça(III). Por fim, o artigo apresenta duas interpretações gerais sobe essas leituras: que existem certas constantes nos argumentos que unem e que pretendem superar Rawls; e que contém possíveis problemas,com consequências que ocasionam certos entraves para sua teoriaem sua pretensão de ser crítica. (shrink)

Con base en una investigación de la obracompleta de Feuerbach, se buscan los matices de Incomprensión feuerbachiana del materialismo a lo largo de la evolución de su pensamiento. En contra de los dualismos exaltados, Feuerbach quiere fundar un materialismo antropológicoy racional, en el marco delreconocimiento de la Naturaleza, de la intuición y del amor. Desde el punto de vista ontológico, queda, sin embargo, en cierto modo, abierta la cuestión de si ese materialismo es consecuente, sobre todo en lo que respecta (...) al papel de la praxis y de la subjetividad como condición de posibilidad de la materialidad. (shrink)

O texto que ora apresentamos é o conteúdo de uma Palestra proferida em Agosto de 2011, em Lisboa, e discute alguns pareceres de Hegel sobre o ensino da filosofia na Universidade, e especilamente nos Liceus. Nosso objetivo é discorrer sobre as três fundamentais “lições” que se pode inferir das meditações hegelianas acerca do ensino da filosofia, a saber: 1) o professor tem que pensar; 2) a filosofia (e o filosofar) não é tão-somente um mero formalismo; 3) a dialéctica se configura (...) como textura, conteúdo, do real e como ocupação nuclear de uma penetração pensante do ser. Primeiramente, nossa argumentação evidencia que, para Hegel, o professor tem que pensar porque este ato é uma exigência fundante do seu trabalho docente de formação. No segundo momento, demonstramos que Hegel se posiciona contrário à tese que afirma o formalismo na contraposição filosofia versus filosofar. Em terceiro lugar, expomos que, para Hegel, o ensino e a aprendizagem devem se ocupar, necessariamente, da dialéctica, na medida em que esta não é um mero instrumento da técnica pedagógica, mas porque ela é constitutiva do pensar e da manifestação do ser no mundo. (shrink)

Normal 0 21 false false false MicrosoftInternetExplorer4 Este trabalho objetiva assinalar as pressões sociais e os valores culturais que participam do processo de construção das identidades brasileiras na sociedade hipermoderna das grandes cidades por meio da análise de um representante dela, que é o universo publicitário. Irei descrever alguns dos resultados encontrados em minha tese de doutorado (2007) em que, ao analisar as estratégias emocionais de persuasão publicitá­rias mais utilizadas nas revistas de maior circulação do país, levantei os conteúdos ideológicos (...) empregados nesses anúncios e, neste momento quero refletir sobre os possíveis modos de convivência social promovi­dos pelas identidades que são ressaltadas. Os meios de comunicação social são fonte de influência e manutenção de modos de viver, logo representam material rico de reflexão para se compreender os impasses dos relacionamentos sociais contemporâneos. Palavras-chave: identidade, publicidade, sociedade, hipermodernidade. (shrink)

O objetivo deste artigo é discutir a noção humiana de "crença", frequentemente vita como adendo "psicológico" à correta doutrina epistemológica do autor. Tenta-se sugerir que são partilha das obsessões da epistemologia contemporânea.

To be usable in practice, interactive theorem provers need to provide convenient and efficient means of writing expressions, definitions, and proofs. This involves inferring information that is often left implicit in an ordinary mathematical text, and resolving ambiguities in mathematical expressions. We refer to the process of passing from a quasi-formal and partially-specified expression to a completely precise formal one as elaboration. We describe an elaboration algorithm for dependent type theory that has been implemented in the Lean theorem prover. Lean’s (...) elaborator supports higher-order unification, type class inference, ad hoc overloading, insertion of coercions, the use of tactics, and the computational reduction of terms. The interactions between these components are subtle and complex, and the elaboration algorithm has been carefully designed to balance efficiency and usability. We describe the central design goals, and the means by which they are achieved. (shrink)