Sunday, October 26, 2014



Soy un nuevo usuario

Olvidé mi contraseña

Entrada usuarios

Lógica Matemáticas Astronomía y Astrofísica Física Química Ciencias de la Vida
Ciencias de la Tierra y Espacio Ciencias Agrarias Ciencias Médicas Ciencias Tecnológicas Antropología Demografía
Ciencias Económicas Geografía Historia Ciencias Jurídicas y Derecho Lingüística Pedagogía
Ciencia Política Psicología Artes y Letras Sociología Ética Filosofía

rss_1.0 Clasificación por Disciplina

Nomenclatura Unesco > (11) Lógica

Mostrando recursos 281 - 300 de 131,932

281. A System for Compositional Verification of Asynchronous Objects - Wolfgang Ahrendt; Maximilian Dylla
We present a semantics, calculus, and system for compositional verification of Creol, an object-oriented modeling language for concurrent distributed applications. The system is an instance of KeY, a framework for object-oriented software verification, which has so far been applied foremost to sequential Java. Building on KeY characteristic concepts, like dynamic logic, sequent calculus, symbolic execution via explicit substitutions, and the taclet rule language, the presented system addresses functional correctness of Creol models featuring local cooperative thread parallelism and global communication via asynchronous method calls. The calculus heavily operates on communication histories specified by the interfaces of Creol units. Two example...

First introduction Where is logic heading today? There is a general feeling that the discipline is broadening its scope and agenda beyond classical foundational issues, and maybe even a concern that, like Stephen Leacock’s famous horseman, it is ‘riding off madly in all directions’. So, what is the resultant vector? There seem to be two broad answers in circulation today. One is logical pluralism, locating the new scope of logic in charting a wide variety of reasoning styles, often marked by non-classical structural rules of inference. This is the new program that I subscribed to in my work on sub-structural...

In the last few years, preference logic and in particular, the dynamic logic of preference change, has suddenly become a live topic in my Amsterdam and Stanford environments. At the request of the editors, this article explains how this interest came about, and what is happening. I mainly present a story around some recent dissertations and papers, which are found in the references. There is no pretense at complete coverage of preference logic (for that, see Hansson 2001) or even of preference change (Hansson 1995).

284. The information in intuitionistic logic - Johan Van Benthem
Issues about information spring up wherever one scratches the surface of logic. Here is a case that raises delicate issues of ‘factual’ versus ‘procedural’ information, or ‘statics’ versus ‘dynamics’. What does intuitionistic logic, perhaps the earliest source of informational and procedural thinking in contemporary logic, really tell us about information? How does its view relate to its ‘cousin ’ epistemic logic? We discuss connections between intuitionistic models and recent protocol models for dynamic-epistemic logic, as well as more general issues that emerge.

285. Classical truth in higher types - Ulrich Berger
We study, from a classical point of view, how the truth of a statement about higher type functionals depends on the underlying model. The models considered are the classical set-theoretic finite type hierarchy and the constructively more meaningful models of Continuous Functionals, Hereditarily Effective Operations, as well as the closed term model of Gödel’s system T. The main results are characterisations of prenex classes for which truth in the full set-theoretic model transfers to truth in the other models. As a corollary we obtain that the axiom of choice is not conservative over Gödel’s system T with classical logic for...

286. Observable Behavior of Distributed Systems: Component Reasoning for Concurrent Objects - Crystal Chang Din; Johan Dovland; Einar Broch Johnsen; Olaf Owe
Distributed and concurrent object-oriented systems are difficult to analyze due to the complexity of their concurrency, communication, and synchronization mechanisms. Rather than performing analysis at the level of code in, e.g., Java or C++, we consider the analysis of such systems at the level of an abstract, executable modeling language. This language, based on concurrent objects communicating by asynchronous method calls, avoids some difficulties of mainstream object-oriented programming languages related to compositionality and aliasing. To facilitate system analysis, compositional verification systems are needed, which allow components to be analyzed independently of their environment. In this paper, a proof system for...

287. Type systems for object-oriented languages based on coinductive logic - Davide Ancona; Giovanni Lagorio

288. On topological models of GLP - Lev Beklemishev; Guram Bezhanishvili; Thomas Icard
We develop topological semantics of a polymodal provability logic GLP. Our main result states that the bimodal fragment of GLP, although incomplete with respect to relational semantics, is topologically complete. The topological (in)completeness of GLP remains an interesting open problem.

289. Ordinal Completeness of Bimodal Provability Logic GLB - Lev Beklemishev
Bimodal provability logic GLB, introduced by G. Japaridze, currently plays an important role in the applications of provability logic to proof-theoretic analysis. Its topological semantics interprets diamond modalities as derived set operators on a scattered bitopological space. We study the question of completeness of this logic w.r.t. the most natural space of this kind, that is, w.r.t. an ordinal α equipped with the interval topology and with the so-called club topology. We show that, assuming the axiom of constructibility, GLB is complete for any α ≥ ℵω. On the other hand, from the results of A. Blass it follows that,...

290. Lazy Behavioral Subtyping - Johan Dovland , Einar Broch Johnsen, Olaf Owe, Martin Steffen
Inheritance combined with late binding allows flexible code reuse but complicates formal reasoning significantly, as a method call’s receiver class is not statically known. This is especially true when programs are incrementally developed by extending class hierarchies. This paper develops a novel method to reason about late bound method calls. In contrast to traditional behavioral subtyping, reverification of method specifications is avoided without restricting method overriding to fully behavior-preserving redefinition. The approach ensures that when analyzing the methods of a class, it suffices to consider that class and its superclasses. Thus, the full class hierarchy is not needed, and incremental...

291. Combining Algebraic and Set-Theoretic Specifications - Claus Hintermeier; Hélène Kirchner; Peter D. Mosses
Specification frameworks such as B and Z provide power sets and cartesian products as built-in type constructors, and employ a rich notation for defining (among other things) abstract data types using formulae of predicate logic and lambda-notation. In contrast, the so-called algebraic specification frameworks often limit the type structure to sort constants and first-order functionalities, and restrict formulae to (conditional) equations. Here, we

292. Modal Matters in Interpretability Logics - Evan Goris; Joost J. Joosten
In this paper we expose a method for building models for interpretability logics. The method can be compared to the method of taking unions of chains in classical model theory. Many applications of the method share a common part. We isolate this common part in a main lemma. Doing so, many of our results become applications of this main lemma. We also briefly describe how our method can be generalized to modal logics with a different signature. With the general method, we prove completeness for the interpretability logics IL, ILM, ILM0 and ILW ∗. We also apply our method to...

293. A Hoare Logic for Concurrent Objects with Asynchronous Method Calls - Johan Dovland; Einar Broch Johnsen; Olaf Owe
The Creol language proposes high level language constructs to unite object orientation and distribution in a natural way. In this report, we show how the semantics of Creol programs may be defined in terms of standard sequential constructs. The highly nondeterministic nature of distributed systems is captured by introducing communication histories to record the observable activity of the system. Hoare rules expressing partial correctness are then derived based on the semantics.

294. Multilanguage First Order Theories of Propositional Attitudes - Fausto Giunchiglia; Luciano Serafini
The goal of this paper is to present a new family of formal systems, so called multilanguage systems (ML-systems), which allow the use of multiple distinct first order languages and inference rules whose premises and consequences need not belong to the same language. ML-systems are argued to formalize naturally and elegantly notions like belief, knowledge and, more in general, various forms of propositional attitudes. Some instances of ML-systems are defined and proved equivalent to the modal logic K and some of Konolige's logics for belief.

295. La Gestión De Las Emociones En El Mercado Informal De Los Cuidados a Mayores - Ramos Espina, Santiago; Rodríguez Rodríguez, Vicente; Lardiés Bosque, Raúl
El papel de las organizaciones y entidades sin ánimo de lucro es esencial para entender itinerarios de inserción tan complejos como el de los inmigrantes sin papeles. En este delicado ámbito de intervención se puede decir que la gestión justa y eficiente de un mercado informal de los cuidados es un nuevo reto para estas organizaciones del tercer sector. Uno de estos desafíos es lidiar con aspectos tan complejos como la contradictoria lógica entre emociones e intereses dentro de las relaciones laborales de los cuidadores y las familias en el seno de los hogares; este artículo pretende realizar un abordaje...

296. El conflicto de valores: Reflexión desde una perspectiva lógico-filosófica - Peña, Lorenzo
Los valores no se confunden con las valoraciones subjetivas, sino que poseen una objetividad, aunque, desde las diferentes perspectivas históricamente cambiantes, son susceptibles de modificación, que no afecta a su esencia sino a sus atributos accidentales --entre ellos su peso y su prioridad. Los valores tienen un anclaje ontológico, habiendo un vínculo entre el ser y el ser-valioso. El nexo viene establecido gracias a una concepción gradualista contradictorial tanto del ser cuanto del valer. Por último el trabajo defiende una escala axiológica en la que se enarbola la bandera antinietzscheana de la moral de los esclavos.

297. Género y novela autobiográfica - Bonatto, Adriana Virginia
En su intervención durante el II Seminario Internacional del Instituto de Semiótica Literaria y Teatral, Darío Villanueva (1993) recuperaba el carácter ficticio de la autobiografía apuntado en sucesivas formulaciones por la crítica tanto estructuralista como deconstructivista, dedicada al estudio del género (Lejeune, Olney, Gursdorf, Barthes, De Man), pero con el fin de sugerir, esta vez, que la clave de la autobiografía no se encuentra en el pacto referencial entre el autor y el lector ni en las figuras retóricas de la metáfora (Olney 1972) o de la prosopopeya (De Man 1979) sino en la de la paradoja, “figura lógica que...

298. LOGIC : un service GeoWeb d’aide à la décision en matière d’implantations commerciales. - Jaspard, Mathieu; Christopanos, Pierre
Peer reviewed

299. A Conversão do Grupo de Esquadrões em Grupo de Ciclistas, na frente ocidental da Grande Guerra - Martins, Miguel
O presente trabalho pretende estudar e dar a conhecer o processo da conversão do Grupo de Esquadrões em Grupo de Ciclistas na frente Ocidental da Grande Guerra. Tendo como principal objetivo analisar as principais alterações orgânicas e o emprego tático das unidades de ciclistas. Os objetos de estudo deste trabalho são o processo de conversão do Grupo de Esquadrões em Grupo de Ciclistas e, a organização e emprego tático das unidades de ciclistas. Ao longo do trabalho iremos utilizar uma metodologia com referência a um método de investigação histórico, baseado numa abordagem diacrónica, analisando o processo de conversão da unidade de Cavalaria...

300. Processos de inclusão excludente presentes no ensino superior privado - Nunes,Mário Luiz Ferrari; Neira,Marcos Garcia
As pressões locais e globais por melhora nas formas de organização social incidiram em políticas públicas que visam garantir o acesso ao ensino superior de parcela da população, outrora desprivilegiada. Este artigo trata dos efeitos que esses processos de inclusão podem gerar. Os dados coletados através de uma etnografia em uma Instituição de Ensino Superior privado foram analisados mediante as noções de identidade e diferença produzidas pelos Estudos Culturais. Considera que os processos de inclusão reforçam e validam as identidades que se adéquam às imposições de consumo e performatividade, características do neoliberalismo, e marcam a diferença por meio de processos...


Busque un recurso