We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions. It is practically relevant because it makes it possible to use a decision procedure for the guarded fragment in order to decide regular grammar logics with (...) converse. The class of regular grammar logics includes numerous logics from various application domains. A consequence of the translation is that the general satisfiability problem for every regular grammar logics with converse is in EXPTIME. This extends a previous result of the first author for grammar logics without converse. Other logics that can be translated into GF2 include nominal tense logics and intuitionistic logic. In our view, the results in this paper show that the natural first-order fragment corresponding to regular grammar logics is simply GF2 without extra machinery such as fixed-point operators. (shrink)

We study a knowledge logic that assumes that to each set of agents, an indiscernibility relation is associated and the agents decide the membership of objects or states up to this indiscernibility relation. Its language contains a family of relative knowledge operators. We prove the decidability of the satisfiability problem, we show its EXPTIME-completeness and as a side-effect, we define a complete Hilbert-style axiomatization.

This paper concerns model-checking of fragments and extensions of CTL* on infinite-state Presburger counter systems, where the states are vectors of integers and the transitions are determined by means of relations definable within Presburger arithmetic. In general, reachability properties of counter systems are undecidable, but we have identified a natural class of admissible counter systems (ACS) for which we show that the quantification over paths in CTL* can be simulated by quantification over tuples of natural numbers, eventually allowing translation of (...) the whole Presburger-CTL* into Presburger arithmetic, thereby enabling effective model checking. We provide evidence that our results are close to optimal with respect to the class of counter systems described above. (shrink)

This work is divided in two papers (Part I and Part II). In Part I, we study a class of polymodal logics (herein called the class of "Rare-logics") for which the set of terms indexing the modal operators are hierarchized in two levels: the set of Boolean terms and the set of terms built upon the set of Boolean terms. By investigating different algebraic properties satisfied by the models of the Rare-logics, reductions for decidability are established by faithfully translating the (...) Rare-logics into more standard modal logics. The main idea of the translation consists in eliminating the Boolean terms by taking advantage of the components construction and in using various properties of the classes of semilattices involved in the semantics. The novelty of our approach allows us to prove new decidability results (presented in Part II), in particular for information logics derived from rough set theory and we open new perspectives to define proof systems for such logics (presented also in Part II). (shrink)

This work is divided in two papers (Part I and Part II). In Part I, we introduced the class of Rare-logics for which the set of terms indexing the modal operators are hierarchized in two levels: the set of Boolean terms and the set of terms built upon the set of Boolean terms. By investigating different algebraic properties satisfied by the models of the Rare-logics, reductions for decidability were established by faithfully translating the Rare-logics into more standard modal logics (some (...) of them contain the universal modal operator).In Part II, we push forward the results from Part I. For Rare-logics with nominals (present at the level of formulae and at the level of modal expressions), we show that the constructions from Part I can be extended although it is technically more involved. We also characterize a class of standard modal logics for which the universal modal operator can be eliminated as far as satifiability is concerned. Although the previous results have a semantic flavour, we are also able to define proof systems for Rare-logics from existing proof systems for the corresponding standard modal logics. Last, but not least, decidability results for Rare-logics are established uniformly, in particular for information logics derived from rough set theory. (shrink)

We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions. It is practically relevant because it makes it possible to use a decision procedure for the guarded fragment in order to decide regular grammar logics with (...) converse. The class of regular grammar logics includes numerous logics from various application domains. A consequence of the translation is that the general satisfiability problem for every regular grammar logics with converse is in EXPTIME. This extends a previous result of the first author for grammar logics without converse. Other logics that can be translated into GF2 include nominal tense logics and intuitionistic logic. In our view, the results in this paper show that the natural first-order fragment corresponding to regular grammar logics is simply GF2 without extra machinery such as fixed-point operators. (shrink)

We show the completeness of a Hilbert-style system LK defined by M. Valiev involving the knowledge operator K dedicated to the reasoning with incomplete information. The completeness proof uses a variant of Makinson's canonical model construction. Furthermore we prove that the theoremhood problem for LK is co-NP-complete, using techniques similar to those used to prove that the satisfiability problem for propositional S5 is NP-complete.

Like modal logic, temporal logic, and description logic, separation logic has become a popular class of logical formalisms in computer science, conceived as assertion languages for Hoare-style proof systems with the goal to perform automatic program analysis. In a broad sense, separation logic is often understood as a programming language, an assertion language and a family of rules involving Hoare triples. In this survey, we present similarities between separation logic as an assertion language and modal and temporal logics. Moreover, we (...) propose a selection of landmark results about decidability, complexity and expressive power. (shrink)

We define cut-free display calculi for knowledge logics wherean indiscernibility relation is associated to each set of agents, andwhere agents decide the membership of objects using thisindiscernibility relation. To do so, we first translate the knowledgelogics into polymodal logics axiomatised by primitive axioms and thenuse Kracht's results on properly displayable logics to define thedisplay calculi. Apart from these technical results, we argue thatDisplay Logic is a natural framework to define cut-free calculi for manyother logics with relative accessibility relations.

In this paper a unified framework for dealing with a broad family of propositional multimodal logics is developed. The key tools for presentation of the logics are the notions of closure relation operation and monotonous relation operation. The two classes of logics: FiRe-logics (finitely reducible logics) and LaFiRe-logics (FiRe-logics with local agreement of accessibility relations) are introduced within the proposed framework. Further classes of logics can be handled indirectly by means of suitable translations. It is shown that the logics from (...) these classes have the finite model property with respect to the class of -formulae, i.e. each -formula has a -model iff it has a finite -model. Roughly speaking, a -formula is logically equivalent to a formula in negative normal form without occurrences of modal operators with necessity force. In the proof we introduce a substantial modification of Claudio Cerrato's filtration technique that has been originally designed for graded modal logics. The main core of the proof consists in building adequate restrictions of models while preserving the semantics of the operators used to build terms indexing the modal operators. (shrink)

In this paper a unified framework for dealing with a broad family of propositional multimodal logics is developed. The key tools for presentation of the logics are the notions of closure relation operation and monotonous relation operation. The two classes of logics: FiRe-logics (finitely reducible logics) and LaFiRe-logics (FiRe-logics with local agreement of accessibility relations) are introduced within the proposed framework. Further classes of logics can be handled indirectly by means of suitable translations. It is shown that the logics from (...) these classes have the finite model property with respect to the class of ♦-formulae, i.e. each ♦-formula has a ℒ-model iff it has a finite ℒ-model. Roughly speaking, a ♦-formula is logically equivalent to a formula in negative normal form without occurrences of modal operators with necessity force. In the proof we introduce a substantial modification of Claudio Cerrato's filtration technique that has been originally designed for graded modal logics. The main core of the proof consists in building adequate restrictions of models while preserving the semantics of the operators used to build terms indexing the modal operators. (shrink)

We present an overview of linear-time temporal logics with Presburger constraints whose models are sequences of tuples of integers. Such formal specification languages are well-designed to specify and verify systems that can be modelled with counter systems. The paper recalls the general framework of LTL over concrete domains and presents the main decidability and complexity results related to fragments of Presburger LTL. Related formalisms are also briefly presented.

Motivated by the verification of programs with pointer variables, we introduce a temporal logic whose underlying assertion language is the quantifier-free fragment of separation logic and the temporal logic on the top of it is the standard linear-time temporal logic LTL. We analyze the complexity of various model-checking and satisfiability problems for , considering various fragments of separation logic , various classes of models , and the influence of fixing the initial memory state. We provide a complete picture based on (...) these criteria. Our main decidability result is pspace-completeness of the satisfiability problems on the record fragment and on a classical fragment allowing pointer arithmetic. -completeness or -completeness results are established for various problems by reducing standard problems for Minsky machines, and underline the tightness of our decidability results. (shrink)

There exist valuable methods for theorem proving in non classical logics based on translation from these logics into first-order classical logic (abbreviated henceforth FOL). The key notion in these approaches istranslation from aSource Logic (henceforth abbreviated SL) to aTarget Logic (henceforth abbreviated TL). These methods are concerned with the problem offinding a proof in TL by translating a formula in SL, but they do not address the very important problem ofpresenting proofs in SL via a backward translation. We propose a (...) framework for presenting proofs in SL based on a partial backward translation of proofs obtained in a familiar TL: Order-Sorted Predicate Logic. The proposed backward translation transfers some formulasF TL belonging to the proof in TL into formulasF SL , such that the formulasF SL either (a) belong to a corresponding deduction in SL (in the best case) or, (b) are semantically related in some precise way, to formulas in the corresponding deduction in SL (in the worst case). The formulasF TL andF SL can obviously be considered aslemmas of their respective proofs. Therefore the transfer of lemmas of TL gives at least a skeleton of the corresponding proof in SL. Since the formulas of a proof keep trace of the strategy used to obtain the proof, clearly the framework can also help in solving another fundamental and difficult problem:the transfer of strategies from classical to non classical logics. We show how to apply the proposed framework, at least to S5, S4(p), K, T, K4. Two conjectures are stated and we propose sufficient (and in general satisfactory) conditions in order to obtain formulas in the proof in SL. Two particular cases of the conjectures are proved to be theorems. Three examples are treated in full detail. The main lines of future research are given. (shrink)

L'évolution de la clinique psychiatrique a mis au centre de ses recherches l'écoute et la parole du patient. Cependant le plus souvent la parole échoit dans les discours et l'écoute se décentre vers la vérification des a priori théo­riques. L'empathie ou les règlements qui incitent le clinicien à mettre le patient au centre de ses préoccupations apportent confort et sécurité mais ratent la rencontre clinique qui échoit dans le relationnel. Une relation n'est pas une rencontre. Le contexte de...

This paper presents the hypothesis that concept possession is sufficient and necessary for self-consciousness. If this is true it provides a yardstick for gauging the validity of different research paradigms in which claims for self-consciousness in animals or human infants are made: a convincing demonstration of concept possession in a research subject, such as a display of inferential reasoning, may be taken as conclusive evidence of self-consciousness. Intuitively, there appears to be a correlation between intelligence in animals and the existence (...) of self-consciousness. I present three discussions to support the hypothesis: an analogy between perception and conception, where both are self-specifying; an argument that any web of concepts will always include the self-concept; and a fresh interpretation of Bermũdez showing how his theory of non-conceptual content provides strong support for the concept possession hypothesis. (shrink)

Subjectivism about well-being holds that an object contributes to one's well-being to the extent that one has a pro-attitude toward this object under certain conditions. Most subjectivists have contended that these conditions should be ideal. One reason in favor of this idea is that when people adapt their pro-attitudes to situations of oppression, the levels of well-being they may attain is diminished. Nevertheless, I first argue that appealing to idealized conditions of autonomy or any other condition to erase or replace (...) adaptive pro-attitudes is mistaken. Second, I show that the most natural version of subjectivism that does not appeal to any such idealizing condition can explain why the well-being of people having adaptive pro-attitudes should not be restricted to the fulfillment of these pro-attitudes. In sum, the existence of adaptive preferences does not militate in favor of the introduction of conditions of idealization but against it. (shrink)

This article renders a close reading of those passages in Walter Benjamin's work where he uses the term “unscheinbar.” Arguing that this concept cannot be reduced to its privative prefix “un-,” the article explores how moments in time, objects or images that are not meaningful in themselves can nevertheless trigger an experience that is to be called such. The article analyzes Benjamin's ideas on friendliness, commemoration, melancholy, mémoire involontaire and photography with the purpose of understanding how a detail or fragment (...) strikes us as significant, despite the fact that it cannot become visible as a unity or whole in its own right. (shrink)

Smallholder farmers in Rattanakmondol District, Battambang Province, Cambodia face challenges related to soil erosion, declining yields, climate change, and unsustainable tillage-based farming practices in their efforts to increase food production within maize-based systems. In 2010, research for development programs began introducing agricultural production systems based on conservation agriculture to smallholder farmers located in four communities within Rattanakmondol District as a pathway for addressing these issues. Understanding gendered practices and perspectives is integral to adapting CA technologies to the needs of local (...) communities. This research identifies how gender differences regarding farmers’ access to assets, practices, and engagement in intra-household negotiations could constrain or facilitate the dissemination of CA. Our mixed-methods approach includes focus group discussions, semi-structured interviews, famer field visits, and a household survey. Gender differences in access to key productive assets may affect men’s and women’s individual ability to adapt CA. Farmers perceive the practices and technologies of CA as labor-saving, with the potential to reduce men’s and women’s labor burden in land-preparation activities. However, when considered in relation to the full array of productive and reproductive livelihood activities, CA can disproportionately affect men’s and women’s labor. Decisions about agricultural livelihoods were not always made jointly, with socio-cultural norms and responsibilities structuring an individual’s ability to participate in intra-household negotiations. While gender differences in power relations affect intra-household decision-making, men and women household members collectively negotiate the transition to CA-based production systems. (shrink)

Stéphane Lemaire | : Subjectivists about well-being claim that an object is good for someone if and only if this individual holds a certain type of pro-attitude toward this object. In this paper, I focus on the dispute among subjectivists that opposes those who think that the relevant pro-attitudes are actual to those who think that they are counterfactual under some idealized conditions. My main claim is that subjectivism should be stringently actualist, though our actual pro-attitudes may be criticized from (...) an intrinsic perspective. To defend this claim, I first present three desiderata that a subjectivist theory of well-being should fulfil. Two of these desiderata result from the fact that a subjectivist theory of well-being should not be implicitly paternalist, while the other is that it should be able to play a normative role. I then show that several actualist theories that introduce light forms of idealization or other conditions that have a similar aim, fail to satisfy at least one of the antipaternalist desiderata. This gives some legitimacy to a very stringent version of actualism. I then describe three features of the kind of stringent actualism that I want to defend, which will explain the ability of what is good for someone to play its normative role. Finally, I show how these features allow us to deal with the classic objection that the objects of actual “defective attitudes” cannot be good for the holder of these pro-attitudes. | : Les subjectivistes à propos du bien-être soutiennent qu’un objet est bon pour un individu si et seulement si cet individu possède un certain type d’attitude positive à l’égard de cet objet. Dans cet article, je me concentre sur le débat à l’intérieur du camp subjectiviste qui oppose ceux qui pensent que les attitudes positives pertinentes sont actuelles à ceux qui pensent qu’elles sont contrefactuelles sous une condition d’idéalisation. Ma thèse principale est que le subjectivisme devrait être rigoureusement actualiste bien que nos attitudes positives actuelles puissent être critiquées d’un point de vue qui leur est interne. Afin de défendre cette position, je présente d’abord trois desiderata qu’une théorie subjectiviste du bien-être devrait satisfaire. Deux de ces desiderata résultent du fait qu’une théorie subjectiviste du bien-être ne devrait pas être implicitement paternaliste, alors que le troisième résulte de ce qu’elle devrait pouvoir jouer un rôle normatif. Je montre ensuite que plusieurs théories actualistes qui introduisent des formes modestes d’idéalisation ou d’autres conditions ayant la même visée échouent à satisfaire au moins un des desiderata anti-paternalistes. Une version très rigoureuse de l’actualisme subjectiviste s’en trouve ainsi légitimée. Je décris ensuite les trois aspects de l’actualisme rigoureux que je souhaite défendre et qui permettront d’expliquer dans quelle mesure ce qui est bon pour un individu peut jouer un rôle normatif. Enfin, je montre comment ces aspects nous permettent de répondre à l’objection classique selon laquelle les objets d’« attitudes défectives » actuelles ne peuvent être bons pour ceux qui ont ces attitudes. (shrink)

Local sustainable food systems have captured the popular imagination as a progressive, if not radical, pillar of a sustainable food future. Yet these grassroots innovations are embedded in a dominant food regime that reflects productivist, industrial, and neoliberal policies and institutions. Understanding the relationship between these emerging grassroots efforts and the dominant food regime is of central importance in any transition to a more sustainable food system. In this study, we examine the encounters of direct farm marketers with food safety (...) regulations and other government policies and the role of this interface in shaping the potential of local food in a wider transition to sustainable agri-food systems. This mixed methods research involved interview and survey data with farmers and ranchers in both the USA and Canada and an in-depth case study in the province of Manitoba. We identified four distinct types of interactions between government and farmers: containing, coopting, contesting, and collaborating. The inconsistent enforcement of food safety regulations is found to contain progressive efforts to change food systems. While government support programs for local food were helpful in some regards, they were often considered to be inadequate or inappropriate and thus served to coopt discourse and practice by primarily supporting initiatives that conform to more mainstream approaches. Farmers and other grassroots actors contested these food safety regulations and inadequate government support programs through both individual and collective action. Finally, farmers found ways to collaborate with governments to work towards mutually defined solutions. While containing and coopting reflect technologies of governmentality that reinforce the status quo, both collaborating and contesting reflect opportunities to affect or even transform the dominant regime by engaging in alternative economic activities as part of the ‘politics of possibility’. Developing a better understanding of the nature of these interactions will help grassroots movements to create effective strategies for achieving more sustainable and just food systems. (shrink)

In _The Marriage of Aesthetics and Ethics_, fifteen authors reflect on the nature of friendship and love and on the complex relation between art and morality.

Que l’idéologie raciste nazie ait pu engendrer la Shoah relève de l’évidence, la plus effrayante sans aucun doute de toute l’histoire du XXe siècle. Que des juristes catholiques et patriotes aient pu se montrer les complices actifs de la persécution des Juifs ne s’explique que dans le contexte d’une IIIe République déchirée et agonisante, accouchant du régime de Vichy. Mais..

Résumé — Au début du traité Della ragione di Stato, Boreto déclare son opposition résolue au machiavélisme. Il récuse en effet une conception de la raison d’État fondée sur l’immoralisme, sur la transgression répétée des commandements divins. Mais Botero ne prône pas un simple retour à une fondation théologique du politique. Il reprend plutôt à son compte, sous le nom de raison d’État, une conception du politique délivrée de toute relation à la moralité transcendante venue de Dieu, une conception amorale (...) telle que Machiavel l’envisageait déjà. Et dans cette perspective il introduit la distinction entre raison d’État ordinaire et raison d’État extraordinaire et prétend montrer de quelle manière une raison d’État ordinaire, pourtant conduite par le seul désir de domination, peut employer des moyens tout à fait compatibles avec les exigences de la morale chrétienne.— At the beginning of the treatise Della ragione di Stato, Botero claims his determined opposition to Machiavellism. He impugns any notion of the reason of State that would be based on immorality, that is on constant transgression of God’s prescriptions. But Botero doesn’t advocate the return to a theological foundation of politics. He uses the expression ragione di Stato to denote a notion of politics released from every relation to transcendent morality coming from God, an amoral notion that Machiavelli was already contemplating. In this matter, it is necessary to distinguish the ordinary from the extraordinary reason of State, because Botero shows how an ordinary reason of State, even looking for the only domination, is able to work in a way which is in full accordance with Christian morality. (shrink)

Plusieurs textes de Giordano Bruno définissent le statut des mathématiques en reprenant la classification aristotélicienne des sciences théorétiques. Toutefois cette classification change radicalement de sens à la lumière du monisme brunien. Les mathématiques restent certes une science abstraite, mais, pour le métaphysicien, elles deviennent l’instrument qui permet de penser le rapport de la substance aux modes, le déploiement dans l’unité de la substance de la pluralité infinie des formes; en d’autres termes, elles deviennent une véritable logique de l’être.