Parameterised Resource-Bounded ATL

It is often advantageous to be able to extract resource requirements in resource logics of strategic ability, rather than to verify whether a fixed resource requirement is sufficient for achieving a goal. We study Parameterised Resource-Bounded Alternating Time Temporal Logic where parameter extraction is possible. We give a parameter extraction algorithm and prove that the model-checking problem is 2EXPTIME-complete.

From Waste Lands to Wasted Lives: Enclosure as Aesthetic Regime and Property Regime

This chapter traces relationships between material processes and cultural logics of enclosure. Waste land—land not under cultivation, producing no revenue for the state—was the raw material of colonial capitalism. Waste also names the by-products of such transformations: lives and lands laid waste. These processes entail ways of seeing and knowing; aesthetic regimes help to naturalize property regimes. The literary personification of nature (as in the pathetic fallacy) is bound up with the objectification of humans: aesthetic renderings of landscape can reinforce a dehumanizing, anti-commons common sense. These resource logics understand nature as separate from humans, disposed for their use, and subject to their control. The chapter considers the role of European imperialism in consolidating ideas about nature and natural resources, situating new materialist accounts of non-human agency within a broader historical context. Mahasweta Devi’s “Dhowli” anchors an examination of a worldwide history of waste, which begins (for John Locke) when “all the world was America.” Devi’s story bears the traces of successive waves of conquest and enclosure in India and offers an Anthropocene allegory avant la lettre—which the chapter juxtaposes with East India Company officials’ observations of the effects of deforestation, a foundation for modern climate science.

Extending the Curry-Howard interpretation to linear, relevant and other resource logics

The so-called Curry-Howard interpretation (Curry [1934], Curry and Feys [1958], Howard [1969], Tait [1965]) is known to provide a rather neat term-functional account of intuitionistic implication. Could one refine the interpretation to obtain an almost as good account of other neighbouring implications, including the so-called ‘resource’ implications (e.g. linear, relevant, etc.)?We answer this question positively by demonstrating that just by working with side conditions on the rule of assertability conditions for the connective representing implication (‘→’) one can characterise those ‘resource’ logics. The idea stems from the realisation that whereas the elimination rule for conditionals (of which implication is a particular case) remains virtually unchanged no matter what kind of conditional one has (i.e. linear, relevant, intuitionistic, classical, etc., all have modus ponens), the corresponding introduction rule carries an element of vagueness which can be explored in the characterisation of several sorts of conditionals. The rule of →-introduction is classified as an ‘improper’ inference rule, to use a terminology from Prawitz [1965]. Now, the so-called improper rules leave room for manoeuvre as to how a particular logic can be obtained just by imposing conditions on the discharge of assumptions that would correspond to the particular logical discipline one is adopting (linear, relevant, ticket entailment, intuitionistic, classical, etc.). The side conditions can be ‘naturally’ imposed, given that a degree of ‘vagueness’ is introduced by the presentation of those improper inference rules, such as the rule of →-introduction:which says: starting from assumption ‘A’, and arriving at ‘B’ via an unspecified number of steps, one can discharge the assumption and conclude that ‘A’ implies ‘B’.