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)

Purpose: Performance measurement systems (PMS) in Nonprofit Organizations (NPOs) are more complex than in for-profit organizations. NPOs have an orientation towards social mission and values, and they consider not only organizational efficiency and viability, but also the social impact of the organization. This research provides a comprehensive synthesis of PMSs in NPOs. Design/methodology/approach: Using a literature review, supported by bibliometric and network analyses. A paper set of 240 articles related to this research field is examined. Topics that are the most (...) prevalent in this research area and their interrelationships are identified, presenting an outline of current efforts. Findings: Despite the descriptive analyses for the paper set, a framework is proposed for organizing the design-implementation factors of PMSs in nonprofit organizations, identifying the main requirements for their successful development. Originality/value: Investigation on performance measurement in nonprofit organizations is still in its early stages of development with many opportunities to further develop the field. Conceptual frameworks and models, as well as specific theories, are being generated for this field of research, and the process of adapting models from the general field of performance measurement is taking place. The meta-framework that organizes the main research topics of PMS in nonprofit organizations and the framework that consolidates factors that influence the design-implementation of PMSs in nonprofit organizations developed represents this paper contribution. (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.

This book throws new light on the way in which the Internet impacts on democracy. Based on Jürgen Habermas' discourse-theoretical reconstruction of democracy, it examines one of the world's largest, most diverse but also most unequal democracies, Brazil, in terms of the broad social and legal effects the internet has had. Focusing on the Brazilian constitutional evolution, the book examines how the Internet might impact on the legitimacy of a democratic order and if, and how, it might yield opportunities for (...) democratic empowerment. The book also assesses the ways in which law, as an institution and a system, reacts to the changes and challenges brought about by the Internet: the ways in which law may retain its strength as an integrative force, avoiding a 'virtual' legitimacy crisis. (shrink)

La palabra alegría es muy importante para Fernando Savater... Y es el tema central en tomo al que se articula el libro "Misterios gozosos", una antología de textos, a cargo de Héctor Subirats, que recorre 25 años de la producción filosófica y literaria de Savater. El escritor definió la palabra alegría como "afirmación del presente, no nostalgia del pasado ni del futuro". Misterios gozosos se divide, en cinco capítulos en los que se recogen las razones para la (su) alegría: (...) el solo hecho de vivir, el gusto por la comida, el buen vino, el regocijo por la polémica, el entusiasmo por lo admirado, desde figuras históricas como Voltaire o Spinoza a personajes míticos como Groucho Marx o King Kong. De hecho, Savater aparece en la portada, del libro con un pequeño King Kong en las manos. El escritor, siempre vitalista, reflexiona también en su libro sobre cuestiones de primordial interés como las drogas, la salud, los derechos humanos, el amor, la muerte o la soledad.Subirats explicó que seleccionó los textos con "mala leche, para mostar la evolución o involución de Savater". Preguntado sobre cómo ha sido la involución del escritor, Subirats respondió que "Savater permanece en su sitio. Ha sido el mundo el que se ha echado para atrás". Y Savater precisó: "Las ideas no entran en uno como en la religión. A los 20 años se piensa de una manera y a los 50, de otra. Si uno lee, va al cine, sigue atento la marcha del país... y sigue pensando invariablemente lo mismo es que no ha pensado nunca". "El resultado del pensamiento no es siempre gozoso: lo gozoso es pensar", añadió. (En "Fernando Savater defiende la alegría de vivir en "Misterios gozosos"". Madrid : El País. 28 de febrero de 1995). (shrink)

Fernando Coni Campos é considerado um dos maiores roteiristas da nossa cinematografia, autor de filmes importantes como 'A Viagem Ao Fim do Mundo', 'Ladrões de Cinema' e 'O Mágico e o Delegado'. 'Cinema - Sonho e Lucidez' é uma reunião da reflexão sobre cinema do cineasta, morto em 1988, acrescida de alguns contos que mostram todo o seu domínio em contar histórias.

Nietzsche apresenta, no decorrer de sua obra, um persistente interesse pelo problema da linguagem, abordando sua origem terrena e sua dimensão demasiado humana, sua ligação ao âmbito instintivo de uma espécie animal e seu caráter artificial e plástico. O objetivo deste artigo é sugerir que tal tema relaciona-se à tentativa nietzschiana de superação da metafísica, em duas frentes. Negativamente, no reconhecimento dos limites da linguagem e da influência de certas seduções gramaticais em nossas concepções do que seria a estrutura fundamental (...) do mundo. Positivamente, na elaboração de uma sintomatologia e de sua arte do estilo, elementos importantes de sua crítica da cultura e postura filosófica. Pretendemos, assim, indicar que a tematização e uso nietzschiano da linguagem possui papel central na elaboração de sua tarefa filosófica de intervenção cultural. (shrink)

Nada hay más confortable para el hombre, ni más peligroso, que las certezas. Nuestra mejor defensa es la filosofía, que consiste engran medida en el arte de cuestionarlas, de atreverse a pensar, de interpelar las verdades establecidas y ver qué esconden. En estepaseo por la historia de la filosofía, Fernando Savater nos presenta a los grandes personajes que con sus preguntas, y en ocasiones con sus respuestas, han marcado el pensamiento occidental. Platón, Aristóteles, Hobbes, Tomás de Aquino, Nietzsche, Marx, (...) Ortega, Wittgenstein y hasta dieciocho filósofos más desfilan por estas páginas de la mano de Savater, que con su habitual estilo lúcido, ameno e inteligente explica sus ideas más importantes y resume sus trayectorias. Un canto al irrenunciable ejercicio de la libertad intelectual, este libro es en realidad una invitación a huir de los tópicos y a compartir con los grandes filósofos la maravillosa aventura de pensar. (shrink)

The long 19th century was a period of many developments and technical innovations in agriculture and animal biology, during which actors sought to incorporate new practices in light of new information. By the middle of the century, however, while heredity steadily became the dominant concept in animal husbandry, some policies related to livestock improvement in Brazil seemed to have been tailored following a climate-deterministic concept established in the mid-18th century by the French naturalist Georges-Louis Leclerc, the Comte de Buffon. His (...) theory of animal degeneration posited, among other things, the necessity of recurrent crossbreeding to preserve animal species living in nonnative environments from climate-induced degeneration. Although largely discredited by the early 19th century, the teachings of the French naturalist seem to have found supporters in a Brazilian program to modernize national agriculture through the application of the natural sciences. Herein I examine the revival of Buffon’s theories in that government-sponsored program to improve animal husbandry and breeding techniques, including actual applications of this theory in the real world. Ultimately, I argue that Buffon’s theory of degeneration was used to tailor public policies and funding for the improvement of domesticated animals in Brazil between 1856 and 1860. (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)

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)

The ethics of autonomous vehicles has received a great amount of attention in recent years, specifically in regard to their decisional policies in accident situations in which human harm is a likely consequence. Starting from the assumption that human harm is unavoidable, many authors have developed differing accounts of what morality requires in these situations. In this article, a strategy for AV decision-making is proposed, the Ethical Valence Theory, which paints AV decision-making as a type of claim mitigation: different road (...) users hold different moral claims on the vehicle’s behavior, and the vehicle must mitigate these claims as it makes decisions about its environment. Using the context of autonomous vehicles, the harm produced by an action and the uncertainties connected to it are quantified and accounted for through deliberation, resulting in an ethical implementation coherent with reality. The goal of this approach is not to define how moral theory requires vehicles to behave, but rather to provide a computational approach that is flexible enough to accommodate a number of ‘moral positions’ concerning what morality demands and what road users may expect, offering an evaluation tool for the social acceptability of an autonomous vehicle’s ethical decision making. (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)

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.

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)

Primeiramente fazemos uma breve discussão sobre a concepção defendida por Gramsci acerca do que caracteriza um intelectual, bem como sua função social nas distintas formações sociais, como desdobramento de tal reflexão do autor sardo, apresentamos sua conhecida distinção, operada no “Caderno 12”, entre os „intelectuais tradicionais‟ e os „intelectuais orgânicos‟ destacando sua práxis social. Por fim, valendo-nos dos escritos do autor no “Caderno 13”, ressaltamos a importância do intelectual orgânico na constituição do partido revolucionário.First we give a brief discussion about (...) the concept advocated by Gramsci about what characterizes an intellectual as well as its social function in different social formations, as a consequence of such a reflection of the author Sardinian, presented his famous distinction, operated in the "Notebook 12" between the 'traditional intellectuals' and 'organic intellectuals' highlighting its social praxis. Finally, drawing upon the writings of the author in "Notebook 13", highlight the importance of the organic intellectual in the constitution of the revolutionary party. (shrink)

We generalize a previous result about dynamically consistent menu preferences to the case where preferences are not necessarily complete. We show that, as it is the case when preferences are complete, a subjective state space version of dynamic consistency is linked to a comparative theory of preference for flexibility. In words, an objective signal is interpreted as an event in the agent’s subjective state space and the agent acts in a dynamically consistent way after that if and only if we (...) can attribute all the differences between the agent’s preferences before and after the signal to the fact that the agent values flexibility more before the signal than after. (shrink)

We present the system SUBSEXPL used for simulating and comparing explicit substitutions calculi. The system allows the manipulation of expressions of the λ-calculus and of three different styles of explicit substitutions: the λσ, the λse and the suspension calculus. A variation of the suspension calculus, which allows for combination of steps of β-contraction is included too. Implementations of the η-reduction are provided for each style. Other explicit substitutions calculi can be easily incorporated into the system due to its modular structure. (...) The uses of the system include: the visualization of the contractions of the λ-calculus in de Bruijn notation, and of guided one-step reductions as well as normalization via each of the associated substitution calculi. Many useful facilities are included: reductions can be easily recorded as text files, LATEX outputs can be generated and several examples for dealing with arithmetic operations and computational operators such as conditionals and repetitions in the λ-calculus are available. The system can be executed over Emacs using the x-symbol mode in such a way that λ-terms and terms of the explicit substitutions calculi are represented in its natural syntax avoiding the necessity of repeatedly generating LATEX outputs. The system has been of great help for systematically comparing explicit substitutions calculi, as well as for understanding properties of explicit substitutions such as the Preservation of Strong Normalization. In addition, it has been used for teaching basic properties of the λ-calculus such as: computational adequacy, the usefulness of de Bruijn's notation and of making explicit substitutions in real implementations. (shrink)

This article proposes a reflection on the persistence of Nazi jurisdictional models in contemporary legal theory, briefly comparing the work of authors such as Wolf, Larenz, Schmitt, Dworkin and Alexy. It aims to demonstrate the authoritarian and radically undemocratic character of certain theoretical constructions used in adjudication, particularly in Brazil. For this purpose, three representative judicial decisions from 2016 are analyzed, highlighting typical structural features of Nazi legal theory which remain accepted by current legal theory, such as the disregard for (...) legality, the personification of the community as judge and the appeal to social values which are taken as self-evident. (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)

O pensamento de Merleau-Ponty como instituição.

Ao longo da trajetória intelectual de Merleau-Ponty, as reflexões sobre arte cumprem um papel crucial em sua preocupação de restituir o espetáculo do mundo, através da volta ao brotamento do sentido do ser na experiência antepredicativa do ser humano dada na percepção. Um sinal disso é que, em cada um dos momentos de seu pensamento, ele escreveu um ensaio no qual o tema central é a contribuição da expressão artística para uma reflexão filosófica interessada na abertura humana corporal no mundo. (...) Este artigo tem como propósito realizar uma aproximação de tais ensaios – recorrendo a uma abordagem cronológica – com vistas a demarcar como eles auxiliam no reconhecimento de certas nuances e articulações de seu pensamento, enfatizando a constante ontológica presente em suas discussões sobre arte. Assim, o trabalho realiza uma visão horizontal sobre o percurso merleau-pontiano de pensamento – transitando da fenomenologia da percepção à ontologia da carne –, com incursões verticais sobre as relações entre percepção, expressão e instituição nos ensaios. A hipótese é que tais temas fornecem a base para a compreensão da arte como experiência de fundação do ser. (shrink)

To begin with -- Genealogy of the cerebral subject -- Disciplines of the neuro -- Cerebralizing distress -- Brains on screen and paper -- Up for grabs.

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)

Mapeando brevemente alguns eventos desencadeados pelo período denominado, por alguns cientistas, como Antropoceno, este estudo busca estabelecer um observatório deste período através da ótica do campo das artes, do cinema e da filosofia. Pretende-se compreender como práticas artísticas podem ser concebidas de forma a sublinhar as incoerências referentes à intervenção humana no sistema e na atmosfera terrestre. Para tal, este estudo recruta trabalhos de artistas como Alice Miceli, Andrei Tarkovsky e Jacob Kirkegaard, em suas potencialidades de prevenção, educação e crítica (...) em relação a distintas implicações relacionadas ao desastre nuclear de Chernobyl. Assim, é compreendida a possibilidade de trabalhos de arte em atuar como revisita histórica e análise geo-histórica, bem como meios de potencializar críticas às injustiças provocadas pelo Antropoceno.Palavras-chave: Arte contemporânea; Antropoceno; Energia nuclear; Justiça Climática. (shrink)

Considering the basic assumption that the modern Law and State theory does not only bear similarities, but also draws true epistemological parallels to theconstructions of Theology, Hans Kelsen intends to lay bare the ideological meaning that lies at the very core of the traditional dualism which constitutes Law and State into autonomous entities. Taking into account Kelsen´s original perceptions – which are seconded by more recent contributions from Claude Lefort and Hans Lindahl’s political and symbolic concepts and from Carl Schmitt’s (...) notions on political theology – our intention is now to demonstrate the highly conservative role played by the duality of the Law/State structure, whose aim is to remove, from under the sway of legal control, a considerable part of the State’s actions.Herebelow, therefore, we will analyse the very legitimacy of the so-called “Public Law,” which seems to point to a trend towards shunning the legal power regulation. Finally, based on the functional method pioneered by Ernst Cassirer, legal institutions such as “collective will” and “public interest” will be problematised, in order to ascertain whether they contain theological, conservative and authoritarian traits incompatible with the conceptual and substantial unity intrinsic to the Rule of Law. (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.

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)

This work offers an analysis of all the legal and moral issues surrounding humanitarian intervention: the deaths of innocent persons and the Doctrine of Double Effect Governmental legitimacy - The Doctrine of Effective Political Control; UN Charter and evaluation of the Nicaragua ruling; The Morality of not intervening; US-led invasion of Iraq; Humanitarian intervention authorised by the UN Security Council - Iraq, Somalia, Haiti, Rwanda, and Bosnia among others highlight NATO's intervention in Kosovo; The Nicaragua Decision; and The precedents of (...) Panama, Liberia and Sierra Leone. The book's features include: a new framework based on the doctrine of double effect; basic principles of international ethics; outline of the moral argument for humanitarian intervention; explores the morality and legality of military action to end tyranny or anarchy; arguments in a much more detailed and complete fashion than in previous editions; in-depth examination of philosophy of international law; the relationship between custom and moral theory; new discussion of the question of right authority; and a full analysis of recent interventions in Kosovo and Iraq. book addresses a broad interdisciplinary audience of international lawyers, philosophers, and political scientists. In this new edition, the author responds to critics while updating the discussion in the light of the momentous events that took place at the beginning of the new millennium. (shrink)

Formal verification involves the use of logical and computational methods to establish claims that are expressed in precise mathematical terms. These can include ordinary mathematical theorems, as well as claims that pieces of hardware or software, network protocols, and mechanical and hybrid systems meet their specifications. In practice, there is not a sharp distinction between verifying a piece of mathematics and verifying the correctness of a system: formal verification requires describing hardware and software systems in mathematical terms, at which point (...) establishing claims as to their correctness becomes a form of theorem proving. Conversely, the proof of a mathematical theorem may require a lengthy computation, in which case verifying the truth of the theorem requires verifying that the computation does what it is supposed to do. The gold standard for supporting a mathematical claim is to provide a proof, and twentieth-century developments in logic show most if not all conventional proof methods can be reduced to a small set of axioms and rules in any of a number of foundational systems. With this reduction, there are two ways that a computer can help establish a claim: it can help find a proof in the first place, and it can help verify that a purported proof is correct. Automated theorem proving focuses on the “finding” aspect. Resolution theorem provers, tableau theorem provers, fast satisfiability solvers, and so on provide means of establishing the validity of formulas in propositional and first-order logic. Other systems provide search procedures and decision procedures for specific languages and domains, such as linear or nonlinear expressions over the integers or the real numbers. Architectures like SMT combine domain-general search methods with domain-specific procedures. Computer algebra systems and specialized mathematical software packages provide means of carrying out mathematical computations, establishing mathematical bounds, or finding mathematical objects. A calculation can be viewed as a proof as well, and these systems, too, help establish mathematical claims. Automated reasoning systems strive for power and efficiency, often at the expense of guaranteed soundness. Such systems can have bugs, and it can be difficult to ensure that the results they deliver are correct. In contrast, interactive theorem proving focuses on the “verification” aspect of theorem proving, requiring that every claim is supported by a proof in a suitable axiomatic foundation. This sets a very high standard: every rule of inference and every step of a calculation has to be justified by appealing to prior definitions and theorems, all the way down to basic axioms and rules. In fact, most such systems provide fully elaborated “proof objects” that can be communicated to other systems and checked independently. Constructing such proofs typically requires much more input and interaction from users, but it allows us to obtain deeper and more complex proofs. The Lean Theorem Prover 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. The goal is to support both mathematical reasoning and reasoning about complex systems, and to verify claims in both domains. (shrink)

Why should sovereign states obey international law? What compels them to owe allegiance to a higher set of rules when each country is its own law of the land? What is the basis of their obligations to each other? Conventional wisdom suggests that countries are too different from one another culturally to follow laws out of mere loyalty to each other or a set of shared moral values. Surely, the prevailing view holds, countries act simply out of self-interest, and they (...) eventually consent to norms of international law to regulate matters of common interest.In this groundbreaking book, Fernando Tesón goes against this prevailing thought by arguing, in the Kantian tradition, that a shared respect for individual human rights underpins not just the obligation countries feel to follow international law but also international laws themselves and even the very legitimacy of nations in the eyes of the international community. Tesón, both a lawyer and a philosopher, proposes that an overlapping respect for human rights has created a moral common ground among the countries of the world; and moreover, that such an outlook is the only one that is rationally defensible. It is this common set of values rather than self-interest that ultimately provides legitimacy to international law. Using the tools of moral philosophy, Tesón analyzes the concepts of sovereignty, intervention, and national interest; the contributions of social contact theory, game theory, and feminist theory; and the puzzles of self-determination and group rights.More than simply outlining his theory, Tesón goes on to give detailed examples of international laws, international institutions, and their human rights foundations, putting his ideas to work and addressing legal reforms called for by the theory. He suggests that treaties, for example, should be considered binding if, and only if, the consent to the treaty was given by a genuinely representative government, one that acts out of interest for the human rights of its citizens. Although the theoretical achievement of this book is to challenge received wisdom on the foundation of international law, the practical ambition is a call to reform the international legal system for the post–Cold War era, to substitute for the old order one that gives primacy to human dignity and freedom over state power. (shrink)