Maxim Fradkin

Gilion Hautvast

Marcel Breeuwer

C Ciofolo

Automatic delineation of myocardial contours in late-enhancement long-axis cardiac MR images

Introduction

Viability assessment is essential for therapy planning following a myocardial infarction. In particular, the proportion of viable myocardium is a major factor in determining whether a patient may benefit from revascularization [1]. In addition to estimating the left ventricular myocardial thickness and thickening with functional imaging, it is possible to visualize normal and non-viable areas with high spatial resolution, using late-enhancement cardiac MR imaging (LECMR). To locate and quantify non-viable tissue, it is first necessary to delineate the endo-and epicardial contours on every available view of the LECMR acquisition. In particular long-axis (LA) views are useful because they provide a visualization of the apical area, which is often not well visible on or not covered well by short-axis slices. While manual delineation is a tedious and time-consuming task, its automation is challenging and, to our knowledge, not yet addressed by any publication or commercial product. This is mainly due to the non-homogeneous intensity of the myocardium resulting from contrast agent accumulation in infarcted areas.

Purpose

We propose a novel method to delineate the endo-and epicardial contours in lateenhancement long-axis cardiac MR images with a minimal user-input in order to provide an accurate quantitative viability assessment.

Methods

Before running the automatic segmentation process, the user selects one enhancement type from four pre-defined ones (no enhancement, diffuse/small enhancement, large/transmural scar, sub-endocardial enhancement), depending on his own observation of the LA view. Then the delineation of the myocardial contours is performed by alternating automatic deformation of a geometrical template and computation of a binary map of the enhanced areas. The template is ribbon-shaped with a variable width, its position is updated depending on image gray values. The map is a 2D binary image showing enhanced areas, it is updated by thresholding the image gray values in a region of interest centered on the endocardium, in order to include sub-endocardial scars. The segmentation is performed as follows: (1) automatic delineation of myocardial contours on short-axis LECMR slices [2], (2) initialization of the geometrical template position and binary map based on step (1) results, (3) iterative loop between geometrical template deformation and update of enhanced areas map: each new position of the template leads to a new map computation, which is then used to deform the template again.

Results

The method was tested on 20 LA LECMR images acquired in a multi-center study between 2004-2007 (Philips Intera scanner 1.5T, M FFE sequence, TE=1.7ms, TR=4.5ms, flip angle=15°). All images are 256x256, with pixel size around 1.5mm. Three experienced users manually delineated the myocardial contours to quantitatively assess the precision of the proposed method and evaluate inter-observer variability. The average error between the manual and automatic contours was 2.4+/-1.0mm for the endocardium and 2.2+/-1.1mm for the epicardium (see Tab.1 for detailed results). The inter-observer variability was computed as an average distance from each manual contour to the other ones and was equal to 1.7+/-0.7mm for the endocardium and 1.5+/-0.9mm for the epicardium. As shown in Fig. 1, the visual quality is good, the contours successfully surround both normal and abnormal parts of the myocardium, which allows a reliable assessment of the percentage of non-viable tissue. Moreover, the accuracy (~1.5 pixel) is in the same range as inter-observer variability (>1 pixel). Remark: as accurate delineation of the valve plane is not required for viability assessment as long as myocardial contours are correct, it was not addressed in this study.

Conclusion

We presented a robust and efficient method for the automatic delineation of the myocardial contours in long-axis LECMR images.

[1] Marshall et. al., Circulation vol. 67, pp. 766-778, 1983[2] Ciofolo et. al., Proc. SCMR'08, pp. 203-204, 2008 1.0 ± 0.6 1.6 ± 0.7 1.6 ± 0.6 1.5 ± 0.6 pixels 1.5 ± 0.9 2.4 ± 1.1 2.4 ± 0.9 2.3 ± 1.0 mm Epicardium 1.1 ± 0.5 1.5 ± 0.5 1.7 ± 0.6 1.6 ± 0.6 pixels 1.7 ± 0.7 2.3 ± 0.8 2.6 ± 0.9 2.4 ± 0.9 mm Endocardium Inter-observer variability D Ref3 D Ref2 D Ref1 Unit Contour 1.0 ± 0.6 1.6 ± 0.7 1.6 ± 0.6 1.5 ± 0.6 pixels 1.5 ± 0.9 2.4 ± 1.1 2.4 ± 0.9 2.3 ± 1.0 mm Epicardium 1.1 ± 0.5 1.5 ± 0.5 1.7 ± 0.6 1.6 ± 0.6 pixels 1.7 ± 0.7 2.3 ± 0.8 2.6 ± 0.9 2.4 ± 0.9 mm Endocardium

  Mean positioning error with respect to 3 manual contours and inter-observer variability. D Refi is the mean distance to reference contour number i.

Fig. 1 :

 1 Fig. 1: Final myocardium contours on 4 different patients Fig. 1: Final myocardium contours on 4 different patients


Social Inscription of Sexualities in an Era of AIDS 1

Evelyne Micollier, Permanent Research Fellow in Anthropology at IRD (French Research Institute for Development), UMR 145, Montpellier, France Scientific Coordinator of Social Sciences Programme, IRD-PUMC/CAMS, Beijing, China.

Contemporary Chinese society provides several socially pre-constructed models of representations and practices that interact to produce tensions that must be managed, and values, behaviour and actions are subject to renegotiation: the first system arises from pluralist and dynamic Chinese tradition (local traditional discourse), the second is twofolded-one was inherited from the 1919 intellectual and reform movement in the historical context of the fall of the Empire and the first republican revolution (1911), the other was introduced by Marxist ideology and nurtured the project to construct a socialist society (official discourse); the third reflects the global model that is producing changes in China just as it is elsewhere (local global or 'glocalised' discourse). Except the first model, the others are broad projects of modernization of the Chinese society as well.

As in other Asian developing countries, the AIDS epidemic was denied for more than a decade (1985)(1986)(1987)(1988)(1989)(1990)(1991)(1992)(1993)(1994)(1995)(1996) by the Chinese authorities and not publicly acknowledged as a major epidemic until 2001 [START_REF] Gill | China and HIV-A Window of Opportunity[END_REF]. From 2003, economical stakes related to SARS and Avian flu epidemic risk succeeded in mobilising official actors, prompting their actions and rising their awareness about epidemic risk from infectious diseases including AIDS (Kaufman et al. 2006: 4-5). At the end of 2003, a broad response based on a national programme stemmed from these changes, showing a strong shift in policies assessing a striking change in the government approach. In April 2005, the law on infectious diseases was revised and AIDS was removed from the list of diseases requiring mandatory quarantine (FIDH, 2005). In 2006, were issued regulations for HIV/AIDS prevention and control, highlighting the responsibilities of both central and local governments and 'stipulating the rights and responsibilities of infected persons' [START_REF] Gill | China and HIV-A Window of Opportunity[END_REF]: 1801).

Ideological and behavioural models underlying sexual life of individuals are transmitted in messages from family or the State through conduits such as schools or family planning organisations and through new, uncontrollable messages from a society on the path of transition to a consumer society that is subject to economic and cultural globalisation processes, and concomitantly experiencing a cultural revitalization and revaluation of tradition. The family is an essential means of relaying official State advice, along with schools and workplaces, and can become a useful locus for sexual health education and prevention and care of STIs (Sexually Transmitted Infections) including HIV infection. While the HIV sexually transmitted epidemics is expanding, a drastic increase in just a few years of HIV infected women is observed globally and in China, an epidemiological factor highlighting the need to evaluate the vulnerability of women in context and to build up 'gender-oriented' preventive strategies. Therefore, the feminisation of HIV/AIDS in China (in 1999, the estimate ratio is 9:1, in 2004 3:1 and in 2006 2.6:1) reflects global trends: briefly speaking, women are more vulnerable to HIV infection because of biological factors (physically, teenage girls as their biological maturity is not reached; young women as AIDS death rate is high among women in their 20s) and social factors: among them, the most significant are gender stereotypes, lack of power in sexual relations, lower status and economic dependency, their traditional role of care-givers meaning that the main psychological and physical burdens of AIDS care bear on their shoulders [START_REF] Ruixiang | Human rights, discrimination, poverty and gender, UNIFEM[END_REF].

At this stage, it is useful to recall that married women are recognized at a global scale as the most at risk population for HIV/AIDS infection following a discussion at a WHO conference (1995) questioning the relevance of the so-called 'traditional high-risk' groups in the context of the HIV/AIDS epidemics (CSW 'commercial sex workers', MSN 'men who have sex with men', and IDU 'injecting drug users'), a label reinforcing de facto the social stigma and widespread discrimination against the persons concerned and therefore their vulnerability towards HIV/AIDS infection. Kaufman et al. (2006: 3) Therefore, acknowledging the social inscription of sexual transmission in the larger context of the social inscription of sexualities while sexual transmission is becoming the leading mode of HIV transmission, may contribute to reframe social inscription of sexualities and vice-versa, documenting the latter may contribute to reframe efforts for HIV/AIDS prevention and care.

Theoretical pointers and contextualization

The way in which sexually transmitted diseases are considered in society may be examined using questions of risk, sexuality and social relationships between the sexes (gender). The AIDS 'social phenomenon' brings to light news questions about sexuality such as the identification of the sexual partners networks and the notion of risk, which constitute a marker to grasp the evolutions of social constructions of sexuality (Giami, 1991 :51).

From an anthropological and 'constructionist' perspective, sexuality is a unique viewpoint from which to explore social behaviour in its many guises, in the context of the HIV/AIDS epidemic. This epidemic is recognised to be one of the most urgent threats to public health globally, and in particular in developing countries, and is considered as a 'social' disease because of its implications and connotations. Three main factors explain that the HIV-AIDS epidemic has globally stimulated, or caused to be developed, social sciences studies on sexuality, namely the situation of a medical emergency, lack of treatment for curing AIDS and an dramatically expanding sexually transmitted epidemic.

Two theoretical approaches-essentialist versus constructionist/constructivist offer a framework for studies on sexuality. Essentialist approaches are based on the hypothesis that biological factors are the most determinants and the substratum of what constitutes the human being, male and female as well.

A constructivist/constructionist approach relies on identification of social and cultural factors, consideration of these factors as determiners of sexuality, and a reformulation of the body of knowledge about sexuality, in the light of the social and historical conditions under which this body of knowledge was gathered: the term 'constructivist' is used more in the fields of epistemology and theories of learning, and has a more cognitivist connotation, while the more general term 'constructionism' primarily encompasses the social dimensions of behaviour and social practices (Long, 2001: 244). The current consensus view on sexuality is that it is a social construct which is located in an open and dynamic context of emotional, social, political and economic relationships.

Setting aside the naturalistic theory of social relations between the sexes, the idea of gender arises as a pertinent way of understanding the 'structural force' (Bourdieu, 1998: 140-147) behind the social and symbolic inequality between men and women and in the relationships between them, including sexual relationships. However, we should also emphasise that in all societies, sexuality casts light on and is the result of economic and political (and other types of) reality, which have no direct link with sex or gender (Godelier, 2003: 194). The way in which the AIDS epidemic, and in particular its prevention and care, has been considered in a social context has contributed to a recognition of the diversity of 'sexual cultures', which reveals, at the same time, the unity of mankind and the diversity of its cultures. In this article, the concept of 'sexual culture' refers to a consensual model of ideas associated with sexual behaviour in a group. Underlying this model is a vision of the world and of values with regard to the nature and purpose of sexual relations. It also implies an affective model of emotional states and moral principles, aiming to institutionalise what is experienced as normal, natural, necessary or approved of by a group of participants (Herdt, 1997: 10). Sexuality is therefore considered in terms of acts, representations and relationships which take place within the affective and sexual lives of individuals, who move in social contexts [START_REF] Bajos | Sexualité et sida. Recherches en sciences sociales (Sexuality and AIDS : Studies in Social Sciences)[END_REF].

The notion of 'sexual health' was discussed at a WHO conference in 1975, and refers not only to pathology arising from sexual activity and requiring care, but also to the psychological, emotional and social aspects of sexual activity; it also introduces the idea of individual or political 'responsibility' of public healthcare institutions, which ideally should organize 'sexual health' services that are suitable for the context in which they operate (Giami, 2002: 9). Following this discussion, a 'legitimized' modern sexology has been revitalized and developed at the international level: Haeberle (1998) argued that such discussion basically reflected the expression of Western, middle class sexual values. The concept of sexual health, drawing on that of reproductive health but dissociating sexuality from procreation, raises the idea of 'responsible sexuality' and the division of this responsibility among men and women (Bonnet, Guillaume, 2004: 15). When applied in the context of HIV infection and its psychological, social and economic implications, this idea of 'responsibility' obtains all its meaning from the constraints relating to prevention and care of this 'medical situation'. We should also emphasise that the main aspects of sexuality that are currently 'medicalised', or which arise from problems of public health, are contraception, abortion, prevention of STIs (including HIV) and of sexual abuse, and care of sexual disorders (Giami, 2002: 7).

Methodological pointers

Investigation about HIV/AIDS vulnerability and the social construction of sexuality in the context of a flourishing sex industry were carried out late 1990s in southern China (Shanghai, Guangxi: Beihai resort) and in Taiwan (Taipei). The methods used relied on collecting qualitative, ethnographic data, with the aim of producing an anthropological analysis: a series of interviews with and observations of various participants in the sex industry were carried out at places where sexual transactions regularly took place; by developing longer-term relationships with female sex workers, their life stories were obtained (Micollier, 2004). In addition to these data gathered on the field, a documentary research was conducted: as far as possible, a number of recent Chinese academic and popularised sources on sexology and human sexual studies were gathered and analysed, and these studies helped to decode representations of social groups and individuals in this context. A few interviews among sex workers and young women were recently conducted in Beijing.

(1) HIV -Sexual transmission and dynamics of the epidemic: epidemiological pointers in social context

During the 1990s, this epidemic initially spread through sharing of infected needles by drug users, and then by the heterosexual route, and similar epidemic models were observed in Thailand, Vietnam, Burma and southern China. Since the Chinese government started to collect more representative data on HIV/AIDS by producing better estimates in the most vulnerable groups and by using more reliable methods of estimation, the estimated number of people living with AIDS (PWHIV) has been revised downwards in 2005, bringing the number to 650,000 as against 840,000 in 2003 which includes approximately 75,000 people suffering from AIDS. The recalculated average rate of infection has fallen by half (approximately 0.05% of the general population). At the end of 2006, less than 200 000 infected people had been identified: more than two third of estimated HIV infected people are not aware of their HIV status. 25,000 people (between 20,000 and 30,000) have died of AIDS (UNAIDS, 2006: i). However, the number of new infections is constantly increasing (an estimated 70,000 new infections in 2005) particularly by sexual transmission (49.8%) and through infected blood (injecting drugs: 48.6% according to UNAIDS, 2006: 1). The number of infections by sexual transmission has increased exponentially over recent years, which confirms that there is a risk of spreading HIV into the general population: the number of HIV infections estimated to be contracted through heterosexual transmission rose to 5.5% of the total number of infections in 1997, to 10.9% in 2002 (UNAIDS, 2003: 14) and this figure reached 19.8% in 2004, to which should be added the 11.1% of infections transmitted by homosexual sex (UNAIDS, 2004: 4) which brings the rate of infection through sex to 30.9%. In 2005 this figure rose to 43.6% (UNAIDS, 2006: 4).

Male homosexuals are the group who are, after intravenous drug users and sex workers, most vulnerable to HIV infection. Preventive policies catering to MSM have recently been integrated in the national scheme of HIV/AIDS prevention and care. From 2006, a number of online sources, some of which are government supported, are designed for MSM (Xinhua, 2006, April 8) and whose objectives and questions needing to be addressed have been discussed on CCTV and on China's biggest national network (tudou net) [START_REF] Zunyou | HIV Testing and Individual Rights[END_REF]). However, these prevention strategies from websites may still be impeded as they were before (Human Rights Watch, 2005) while the extent of the epidemic among homosexuals may be masked by the fact that, according to researchers' estimations, between 80% and 90% of homosexuals marry and have heterosexual relationships with their spouses at least for procreation purposes (Kaufman, Jing 2002, Pan 1995, 1996[START_REF] Yanhai | Becoming a Gay Activist in Contemporary China[END_REF], 1996[START_REF] Zhou Huashan | Beijing tongzhi gushi, Xiangkang: Xiangkang tongzhi yanjiushe[END_REF]. Sex workers and their clients make up 19.6% of the total number of PWHIV and men who have sex with men (MSM) 7.3%; among sex workers, the rate of HIV infection has risen from 0.02% in 1996 to approximately 1% in 2004 (UNAIDS, 2006: 2 and 4).

According to data processed from national surveillance sites, 11% of IDU (Injecting Drug Users) are involved in high risk sexual behavior impacting their own vulnerability and generating an accelerated HIV spreading among vulnerable groups (IDU, SW and their clients) (UNAIDS, 2006: 5).

Individual internal and external (cross-border) mobility, which is promoted by movement of goods and people, and by regional economic integration in east and south-east Asia, as well as mobility of participants in the sex industry (e.g. sex workers SW, clients, owners of various facilities used by the sex industry, procurers, smugglers, carriers, authorities) is known to be an important factor in spreading HIV. In the UNAIDS report of June 2002, which was notable in that it really alerted local and international bodies to the extent of the epidemic risk of HIV in China, other factors were mentioned, particularly a very neglected public health system in rural areas, which has the immediate consequence that many people are excluded from the prevention and care system; in addition, the report pointed out that PWHIV are significantly stigmatised, and that ethnic minority groups in China (56 such groups are officially registered) are populations more vulnerable to HIV infection, a vulnerability increased by poor socio-economic conditions (poverty).

In the 2006 UNAIDS report, are added other propagating factors such as the increase of risky sexual behaviors and the rise of STI infected people. In 2005, the MoH acknowledged that sexual transmission is becoming the leading mode of HIV transmission2 and should be the focus of HIV prevention interventions. From last year, there is a recognition that the virus is spreading from vulnerable groups, namely sex workers, MSM, and migrants, to the general population (UNFPA report, 2007). About 75% of infected persons reside in the five most affected provinces: Yunnan, Xinjiang, Henan, Guangdong, Guangxi. In a number of localities in the first three provinces, the epidemic is spreading into the general population with an increasing number of infected women and of HIV infections caused by sexual transmission and a prevalence rate above 1% among pregnant women screened during the compulsory premarital clinical examination (UNAIDS, 2006 : 5). Let us notice that such checking is not compulsory anymore raising the question of inter-sectoral cooperation for the improvement and implementation of AIDS policies. According to some (remaining confidential) sources, in a few localities in Yunnan, HIV infection among sex workers rate may be as high as 10%, an indicator confirming the risk of propagation into the general population.

(2) Situation of sexually transmitted infection within society and the position of sexual and social sub-groups

Sex work in the context of an expanding sex industry

In the context of the risk of HIV, the social significance of the resonance of commercial sex in sexual activity should be emphasised, within the framework of the local sexual culture: the sale and purchase of sex, understood as a social practice and a 'mark of social distinction' (status symbol) for men, does not generate head-on contradiction or paradoxical restriction of the role of women in the context of local family structures and norms, but rather it generates tensions that need to be managed; therefore, a sexual culture emerges that is implicitly structured by commercial sex exchanges in tension with matrimonial exchanges (Micollier, 2004: 3-22). The Confucian principles and values of the family do not permit pleasureoriented sexuality within the family unit; instead, conjugal sexuality is oriented towards reproduction. Until the 1930s, erotic desire-led sexuality was lived outside the family setting, particularly in the courtesan system and other categories of sex workers. There is a real social stratification of courtesans, which mirrors that of their clients, and this model was welldocumented in 1930s Shanghai, by the social historical studies of [START_REF] Henriot | Prostitution in Shanghai. A Social History[END_REF] and [START_REF] Hershatter | Dangerous Pleasures. Prostitution and Modernity in Twentieth Century Shanghaï[END_REF]. As in many societies, 'sexuality for desire' is distinguished from 'sexuality for reproduction' and 'desire is not recognised as the departure point for a legitimate union between the sexes' (Godelier, 2003: 195).

In contemporary China, a seven tier hierarchical categories of sex work and of sex workers have been identified reflecting both the clientele's social stratification and, as a social process, a resurgence of pre-1949 concubine system: the first category is the second wife (ernai), who offers sexual services instead of the emotional, reproduction services, and co-habitation usually or ideally provided by the first wife and/or concubine. The second layer is the hired prostitute for a business trip or for a longer period but within the context of business activities (baopo). The third layer is constituted by escort girls working in three different settings (santing: singing parlours or karaoke bars, dance halls, and restaurantsbars), who provide 'on-the-spot escort,' consisting of titillation sexual services without actual sexual intercourse, and/or 'follow you escort' including sexual intercourse. 'Chink girls' (dingdong xiaojie) who live in their own room in a hotel on a relatively stable basis (zhudian de), and solicit hotel customers by telephone, are part of the fourth layer. They offer a onetime sexual intercourse service rather than all-night sex. The fifth layer is composed of barbershop or massage girls (falang mei) working at barbershops, sauna centres, and feetwashing rooms: their services consist of washing hair or feet and giving massages.

Streetwalkers (jienü) who find customers in recreational places and offer one-time sexual intercourse service are the sixth layer. The seventh layer are the prostitutes for poor transient peasants or workers called 'women who go to, or live in a shed,' (xia gongpeng, zhu gongpeng) playing the role of public wife who charges for the services she provides [START_REF] Suiming | Three 'Red Light Districts' in China[END_REF](Pan, : 28-29, 1999 : 23-25) : 23-25).

In addition to these seven categories identified in the 1990s, two other categories emerge in the 2000s while patterns of sex work are evolving over time: (8) married couples organizing commercial sex work together as the husband works as gate-keeper or as controller (fuqi dian), and (9) independent female sex workers calling clients by internet or SMS by mobile phone, and working in her own home. These spaces are usually rented rooms. There is no specific name to label them or such label has not yet emerged. Sex work through web networks has dramatically increased these last years (Pan 2007). These new trends show that the number of independent sex workers is on the rise meaning concomitantly that the role of mummies and bosses are much less central; another relatedfactor is an increase in mobility in order to remain independent. Hopefully, according to Pan, crime related to sex work will be reduced.

The situation of male sex workers is much less documented although a few recent The main issues faced by sex workers needing to be addressed in the context of HIV/AIDS prevention and care are as follows: wide-spread stigma and discrimination, violence, police monitoring and law enforcement. For instance, there is a contradiction between the objective of promoting condom use and at the same time, using condoms as evidence to charge sex workers. AIDS education should not only cater to sex workers but also involve them directly by transferring skills through a (real) peer-education process [START_REF] Slamah | Right-based approach to sex work: situation in Asia, APNSW (Asia Pacific Network of Sex Workers)[END_REF]. During the recent international workshop on HIV prevention targeting sex work (Beijing, April 2007), the issue was raised following the unfortunate assessment that there was no Chinese sex worker at all attending the conference. The cooperation in programs is controlled by the powerful actors in the sex industry (captains, mummies, and brothel-owners) but not directly by sex workers showing a top-down attitude enforcement. It is well-known that the central government has some difficulty to accept the contributions of civil society to governance (FIDH, 2007) even though aware and informed of the benefits of local AIDS NGOs role in interventions: Piot, director of UNAIDS, strongly suggested that their role and the role of (self-organized) vulnerable groups and PWHIV should be reinforced [START_REF] Afp | La lutte contre le sida en Chine ne peut être gagnée si le rôle des patients et des ONG n'est pas renforcé[END_REF] At the same workshop, Pan underlined the responsibility of rich clients (da guan), those who have more sexual partners, a well-documented risk factor in HIV spreading.

Perception of sex work, youth sexual behavior and the construction of masculinity

A paradoxical tension can be analyzed in the social construction of masculinity: while hiring sex workers is part of entertainment and leisure routine among middle-class men and is widely perceived by others as a status pointer, the practice may simultaneously induce a feeling of shame and inconvenience. As far as it is documented, middle-class men are much more discrete about their patronizing of sex works than men belonging to lower social categories (personal communication, field data collected by Pan and Huang 2005). These latter give details more freely about their frequentation of sex workers as they may not experience that tension. Western ideas about sex work, modernity, and also socialist ideas previously disseminated in China may have an impact. Traditional ideas about sex work may be challenged by or in contrast to a more globalized approach related to modernity, Christian and Western ideas. There may be the expression of a tension in the construction of masculinity between revitalized traditional ideas (an eventual result of a socialist governmentdriven repressive attitude towards sex), on-going consumerism and globalizing ideas still driven by Western-oriented ideas even though there may occur a real mixing of ideas in the future. A powerful contradiction is stemming from the value system, matrimonial exchanges rules, gender roles and gender-powered relations based on a (eventually revitalized) 'Confucian'-oriented worldview. Indeed, psychological intrinsic tension between family, marriage based on socio-economic criteria and family choice rather than individual choice, on dutiful feeling rather than on a sexuality driven by an individual quest for pleasure, erotic desire being related to narcissism and a valuation of the Ego. Discretion is prescribed about the purchase of sexual services: therefore, enjoying this whole range of entertainments in bars, karaoke halls enrolling peer-group clients and sex workers appears as a mean of assessing status although a non openly legitimate one. Even though illegitimate, such mean is not transgressive as it is clearly normative and in line with activities helping in the male orientation and identity building, namely in the psychosocial construction of masculinity.

The frequentation of sex workers among young men aimed at sexual initiation is decreasing while young women accept more easily premarital sexual relations. However, young men still have this idea that they will prefer to get married with a virgin. The latter may be among the reasons to explain the relatively more conservative behavior of women and their lower awareness, interest and level of health education towards sex than their male counterparts. As Pan's most recent studies (2007) show, while the increase in premarital male sexual activity was documented earlier in time, there is today a shift towards a relative increase of female 'openness' but no revolution and no significant 'openness' among university students as the rate of women experiencing premarital sex is rising more quickly than that of men. This overall situation has an impact on sex work whose patterns are changing too, more independence of female sex workers using new technologies (internet, mobile phones) who may work alone, and the emergence of husband/wife collaborative unit in sex work.

Following [START_REF] Tiantian | Cool masculinity: male clients' sex consumption and business alliance in urban's China sex industry[END_REF] analysis focusing on male clients from the business milieu, the consumption of sexual services is 'a criterion to evaluate one another's deference, reliability, self-control, and sexual potency. Sex consumption becomes a business ritual for conducting the pre-selection of, and bonding with, potential partners to reach mutual trust in their social alliance in the current Chinese state-clientelism'.

The overall situation of MSM 4

According to statistics from the public security forces (police), 1% of the male population of Beijing is homosexual, which is a conservative figure that is nonetheless acceptable for Li (1992, 1998a, 1998b) who carried out sociological studies on homosexuality, but this figure is too conservative for other sociologists (Pan, 1995(Pan, , 1996) ) and activist gay researchers such as [START_REF] Zhou Huashan | Tongzhi: Politics of Same-Sex Eroticism in Chinese Societies[END_REF][START_REF] Zhou Huashan | Homosexuality and the Cultural Politics of Tongzhi in Chinese Societies[END_REF] who proposes a rate of between 3% and 5%; and in Shanghai, the official estimate is 0.5%.

In China, homosexuality was de facto decriminalised in 1997 following the criminal law suppression and 'de-pathologised' in 2001, under pressure from American psychiatric and psychological associations and in accordance with the WHO International Classification of Diseases (ICD), and certainly also because Chinese society has shown increasing tolerance towards homosexual people, who are also becoming more visible. Homosexuality, until this point, had been included on the 'Chinese list of mental disorders'. In Asia, only four countries -Japan, Korea, Taiwan and the People's Republic of China (including Hong Kong) have officially stopped considering homosexuality as a psychiatric disorder.

In Western countries, while the epidemics had largely become a homosexual epidemic, the experience related to AIDS impacted deeply the social experience and the identity construction of homosexuality, both male and female (Broqua et al. 2003: XIII).

Even though such a situation diverges from the situation in developing countries where the epidemic has not been driven by 'homosexual' transmission, AIDS projects did stimulate the development of gay/lesbian movements, or did at least favor their visibility in major Chinese cities: AIDS activism acted to reveal and defend these movements. It was the driving force that encouraged separate groups to organise together, especially using virtual networks and also meeting places, discussion forums and information that were very real, such as specific bars and salons in Beijing which were closed on a regular basis after police visits, but which then re-opened elsewhere in the capital.

To understand the local dynamics involved in defending the rights of homosexual groups, their visibility and 'coming out', it must first be remembered that there is a specific local image of homosexual practices which tend to be able to adapt, especially to the context of the Chinese family, which always represents the most stable institution in the Chinese world. I use the term 'homosexual practices' rather than 'gay', the term that refers to the identity construction associated with the practices, because according to surveys on sexuality (Liu, 1992;Liu 1993;Pan 1995Pan , 1996)), the vast majority of homosexuals in China do not identify with a sexual minority. The reason for this could be associated above all with the social pressure and preoccupation with being a father and husband in order to honour the filial duty owed to their parents and to ensure descendants for the ancestors; they therefore decide to get married and have children, marriage being above all a social institution to ensure biological and social reproduction. Although new research acknowledges some change among urban MSM in their attitude towards marriage at least in Shanghai and Hong Kong (Sun 2006;Kong 2005), it remains significant to explain the conception and practice of homosexuality in the context of the Chinese family (Young 200234-35, Rofel 1999). Wan believes that at least 90% of gays, lesbians and bisexuals are married, and Zhou (1997:76) believes that 99% of the total population marry. According to [START_REF] Zhou Huashan | Homosexuality and the Cultural Politics of Tongzhi in Chinese Societies[END_REF], the problem of sexual orientation, involving categorisation according to the gender of the object of the erotic desire did not arise in Chinese civilisation: the distinction between heterosexuals, homosexuals and bisexuals did not exist. Sexual activity between people of the same sex in traditional China and depictions of it have today been documented (Hinsch, 1990;[START_REF] Vitiello | Zhongguo dalu tongzhi de xiankuang (Appendice: La situation actuelle des homosexuels de Chine continentale)[END_REF]Sang, 2002: part I). The essential role of the family in the daily life of people of the Chinese culture makes marriage and procreation compulsory, independent of sexual orientation.

Note that in the 1990s, four of the most successful Chinese films that had most international recognition were about male homosexuality in the traditional Chinese world transmission of HIV, as in the early 1990s, when the study was carried out, the epidemic risk of AIDS was denied. However, STIs including AIDS had been noted as problems arising from sexuality and that should be treated in the context of health and social care. The Liu report (Liu, Dalin et al. 1992 In the context of prevention and care of HIV/AIDS in China, the idea of 'sexual health' acts as an heuristic for studies on sexuality, which recently have been produced in ever-greater numbers and on increasingly diverse subjects, and in defending social and individual rights. Such a concept is effectively a useful pragmatic component of negotiations of these rights with official institutional bodies, and can indeed be indispensable if this discussion is to take place at all, even if it nevertheless should be noted that some sexological studies, particularly emerging from the medical field, reveal that the notion of 'sexual health' is being used as a political tool (McMillan, 2006), and that these studies, in terms of their ethical framework and effectiveness at serving public health, are controlled by dubious official action and discourse.

As [START_REF] Giami | The influence of an epidemiological representation of sexuality: The ACSF questionnaire[END_REF] showed in studies carried out on HIV/AIDS in France, we should note that, in the same context in China, an 'epidemiological construction of sexuality' emerges, or continues out of the long history of modernisation and normalisation of sexuality in Chinese society [START_REF] Dikötter | Sex, Culture and Modernity in China. Medical Science and the Construction of Sexual Identities in the Early Republican Period[END_REF][START_REF] Dikötter | La sexualité et les maladies sexuellement transmissibles en Chine : discours médical et représentations sociales (Sexuality and STDs in China : medical discourse and cultural representations)[END_REF] and this appears to be a new product of ideological interference which link science (represented here by the fields of epidemiology and public health), morality and sexuality.

Conclusion

As shown by official studies such as the Liu report (1992), or Pan (1993) on sexual behaviour, or more balanced and problematised studies on sexual representations and practice (for example Li 1998a, and her qualitative study 1998b), it is necessary to 'contextualise' sexualities, while avoiding 'culturalisation' of sexuality, in order to optimise HIV/AIDS prevention and care actions. There is a need to 'contextualise' them in space and time: in the context of HIV spreading, shifts in sex work patterns, and changes in behavior and ideas of clients and young people are assessed but still not well documented. These factors may strongly impact the future development of the HIV epidemic dynamics, namely a confinement of the epidemic in a number of groups and localities or a spread into the general population through a widespread sexual transmission. Economic and political aspects such as the relations between the authorities of different sectors (for instance the tension between health official actors and the police in the context of AIDS prevention and control), the collusion of interests between the business alliance, organized crime and officials in the sex industry, the difficulty to integrate non-governmental actors and organized patients' or vulnerable groups in the governance process need to be recognized and negotiated.

However, in China as elsewhere, the emergence and recognition of minority groups (either sexual or social), and of the rights of these groups, as well as the way in which these groups negotiate with other participants in traditional normative contexts (the family), informal networks of social relations, intimate or official contexts, have been facilitated by collective anti-AIDS action by civil and official bodies even though these rights are still only timidly granted in a limited context. In addition to these, let us recall that this action has been somewhat delayed due to an official denial of the existence of a broad epidemic until 2001 and reduced in its scope by the difficulty to build up a grass-roots and broader participation of civil actors to governance.

  identified seven risk factors for the development of a widespread sexual epidemic: 'the size of China's young sexually active population, changing sexual behaviors and norms, widespread prostitution, massive internal migration, low knowledge about transmission routes among the general population, an HIV/AIDS epidemic among MSM that has only recently been recognized'. Arising from a background description which provides pointers to the theory, methodology and Chinese context, are the following points: (1) sexual transmission of HIV in the context of an epidemic dynamics; (2) its situation within society and the position of sexual and social sub-groups (sex workers/potential clients, MSM, and migrants as potential bridge populations for HIV transmission), and (3) late 1980s development of studies on sexuality in the context of 'sexual health' and 'sexology'-oriented awareness as assessing a social inscription of sexualities as well.

  studies tackle the subject (Kong 2005; Sun et al. 2006): young men labelled « money boys» (shaoye) sell sex to an exclusively male clientele. Most of them are from rural origin and poorly educated 3 : approximately 20 000 are estimated working in bars in northern Chinese big cities (Beijing, Harbin, Shenyang) (Pan 2005, personal communication).

  [Chinese version]/Ng, Man-lun and Erwin J. Haeberle 1997 [English translation]) is based on a sexual behaviour survey of 20,000 people carried out in China in 1989 and 1990. The aim of this enquiry was to identify and clarify problems linked to human sexuality in contemporary China. Sexuality in adolescents and young people, control and management of sexuality, and the rapid spread of STIs (and possibly HIV) in the 1990s are included in these problems. The 'Centre for sociological research on sexuality in Shanghai', directed by Liu, benefited from the favourable political and social climate in the late 1980s, and organised this survey, which was carried out in the context of official organisations. During this period of reform and increased openness, social and biological problems associated with sexuality and the need for sexual health education were officially recognised and became subsidised. Official discourse was also emphasising 'the historical need to confront and resolve problems that are difficult to accept, such as the development of the sex industry and the spread of STIs' (Liu, 1992: 21). During the late 1980s, doctors in Beijing such as Dr Wu (1988), then director of the Academy of Medical Sciences, and Professor Ruan (1991) from the Medical University injected dynamism into sexological research, and two sociological research institutes have been specialising in such sexuality studies for the past couple of decades; one was founded by Liu in Shanghai and the other by Pan in Beijing. Moreover, sexuality has become a discreet but dynamic area of reformed China: according to Pan (1993: 5), the scientific discourse of sexology has produced a neutral language in which sexuality and sex education can be expressed, which facilitates communication in this area; he notes that more than 200 books about sexology were in circulation in 1991, versus only six in 1979. He links diversification, visibility and even the increase in sexual activity to many factors: of these, he considers changes in living conditions to be significant, namely moving away from courtyard-based houses into apartments in blocks where private life is better separated, in spatial terms, from collective life (Pan 1993: 13).

Part of this paper is revised and data updated from Micollier E.

Even though HIV-infection caused by contaminated blood still constitute the leading mode of HIV transmission among reported HIV positive people, such mode of transmission remains hardly significant for epidemic prospective as most infections occurred before 1996.

Same sociological findings in a Shanghai's study, see[START_REF] Zhongxin | Choi Kyung-Hee Sexual Identity Among Men Who Have Sex with Men in Shanghai[END_REF]

This section is revised from Micollier 2005a.

A Human Rights in China Report, 1997. Hinsch B. Passions of the Cut Sleeve. The Male Homosexual Tradition in China. Berkeley: University of California Press; 1990. Huang Yingying, Henderson GE, Pan Suiming, Cohen MS. HIV/Risk among Brothel-Based Female Sex Workers in China. Sexually Transmitted Diseases 2004; 31(11): 695-700. Human Rights Watch 2005; 17. Kaufman J, Jing Jun. China and AIDS. The Time to Act is Now. Nature 2002; 296 (5577): 2339. Kaufman J., Kleinman A., Saich T., eds, AIDS and Social Policy in China, Harvard University Asia Center, Cambridge, Mass; 2006. Kinsey A. Sexual Behavior in the Human Male. US; 1948. Kinsey A. Sexual Behavior in the Human Female. US; 1953. Kipnis A. 'Face': An Adaptable Discourse of Social Surfaces. Positions. East Asia Cultures Critique 1995; 3(1): 119-48. Kong, Travis SK The Hidden Voices: The Sexual Politics of Chinese Male Sex Workers, Research Report, Hong Kong, Hong Kong Polytechnic University; 2005. Liu Dalin, Ng Man-lun, Zhou Liping, Haeberle EJ Zhongguo Dangdai Xing Wenhua : Zhongguo Liangwan Lie 'Xing Wenming' Diaocha Baogao (Contemporary Chinese Sexual Culture: Report of the 'Sex Civilization' Survey on 20000 subjects). Shanghai: Sanlian Bookstore, Chinese Edition; 1992. Li Yinhe, Wang Xiaobo. Tamende shijie: Zhongguo nan tongxinglian qunluo toushi (Their world : Radioscopy of Chinese Male Homosexual Communities). Hong Kong: Tiandi tushu youxian gongsi;1992. Li Yinhe. Tongxinglian ya wenhua (Homosexual Sub-Cultures). Beijing: Jinri zhongguo chubanshe; 1998a. Li Yinhe. Zhongguo nuxing de ganqing yu xing (Feelings and Sexuality of Chinese Women). Beijing: Jinri zhongguo chubanshe; 1998b. Long N. Development Sociology. Actor perspectives. London and New York: Routledge; 2001. McMillan J. Sex, Science and Morality in China. London and New York: Routledge; 2006. Micollier E. The Social Construction of Sex Work in China: Implicitly Shaping a Sexual Culture? in Micollier E., ed. Sexual Cultures in East Asia. The Social Construction of Sexuality and Sexual Risk in a Time of AIDS. London and New York: RoutledgeCurzon; 2004 : 3-22. Micollier E. Collective mobilisation and transnational solidarity to combat Aids in China: local dynamics and visibility of groups sexual and social minorities. Face to face. Perspectives on Health 2005a ; 7 (available online, www.ssd.u-bordeaux2.fr/faf ): 31-40 Micollier E. AIDS in China: discourses on sexuality and sexual practices. China Perspectives 2005b ; 89 (available online, www.cefc.com.hk) : 2-15. Micollier E. Sexualities and HIV/AIDS vulnerability in China, an anthropological perspective. Sexologies (European Journal of Sexual Health) 2006; 15(3): 191-201. Pan Suiming. A Sex Revolution in current China. Journal of Psychology and Human Sexuality 1993; 6: 1-14. Pan Suiming. Homosexual behaviors in Contemporary China. Journal of Psychology and Human Sexuality 1995; 7(4): 1-17. Pan Suiming. Male homosexual behavior and HIV-related risk in China. In: Aggleton P, editor. Bisexuality and AIDS: International Perspectives. London: Taylor-Francis Group; 1996: 178-90. Pan Suiming. Zhongguo dixia 'xing changye' kaocha (Investigation on China' Underground Sex Industry). Beijing : Qunyan chubanshe; 1999.

(Chen Kaige 1993 'Farewell my concubine', Chinese People's Republic, Tsai Ming-Liang 1995 'Long Life to Love aiqing wansui', Taiwan; Zhang Yuan 1996 'East palace, West palace' or in a transnational setting (Ang Lee 1993 'The wedding banquet', filmed outside the borders of the Chinese world). The life stories recounted by [START_REF] Zhou | Histoires de "camarades": les homosexuels en Chine[END_REF], [START_REF] Rofel | Qualities of Desire: Imagining Gay Identities in China[END_REF] and in Ang Lee's film show that Chinese homosexuals today negotiate a level of social and family tolerance without challenging the model of the family as the foundation of social structure and values. Chinese gay/lesbian organisations adopt action strategies and claim their rights using methods that are less conflictual with regard to tradition and the post-socialist State than those of western movements. We do find here a constant factor in the way in which the emerging civil society deals with social problems in China: local organisations working for the recognition and easing of these problems negotiate with political or symbolic authorities, avoiding direct confrontation and conflict.

In China, the question of sexual identity is less central than it has been and still is in Western social contexts: for example, the acceptance of marriage and reproduction in negotiations with the parents, a way of reconciling filial love with choice in matters of erotic desire. Rofel (1999:460-464) clearly shows through discussions in homosexual bars in Beijing that maintaining good relations with parents by marrying in order to have a son to assume the responsibility of providing descendants for the family or the lineage is an essential preoccupation which often comes up in debates. In his film, Ang Lee (1993) shows a 'happy ending' with the parents accepting their son's lover as another son, on the tacit condition that he gives them a son by marrying a woman. This 'happy ending' is not pure fiction: Zhou The major quantitative studies, which follow more or less the same model as the Kinsey reports (1948-1953, first editions), should be distinguished from sociological studies based on collection of quantitative (and possibly qualitative) data, which in turn should be distinguished from more detailed sociological or ethnological studies, which use qualitative data as the principal material for analysis. The national sexuality report, published in 1992, which is commonly referred to as the Chinese Kinsey report (Liu report), and the critical analysis that has been done of it, shed light on the plurality of discourse about sexuality.

Unlike recent reports published in other countries, it does not draw a direct link with sexual


Clément Houtmann

Henri Poincaré -Nancy 1 -Loria

Three Dimensional Proofnets for Classical Logic

published or not. The documents may come

Introduction

The witness property is an important advantage of intuitionistic logic over classical logic. Indeed witnesses of existential statements can always be obtained when the statement is proved in the former. Nevertheless and from the programming point of view, constructivity is only required for Σ 0 1 -statements for which Friedman demonstrated that classical and intuitionistic provability coincide [START_REF] Friedman | Classically and intuitionistically provably recursive functions[END_REF]. Initiated by [START_REF] Griffin | A formulae-as-types notion of control[END_REF], studies on the algorithmic meaning of classical constructions is today an active and successful field of research. Griffin first demonstrated that control operators can be typed by Pierce's law [START_REF] Griffin | A formulae-as-types notion of control[END_REF]. This foundational work was then followed by a range of studies about computational interpretations of classical logic as well as sequent calculus. While beta-reduction is usually considered as the cut-elimination procedure for natural deduction, a wide range of cut-elimination procedures can be imagined for sequent calculus [Gen35, CH00, UB01, BL08]. Strong normalisation or confluence may not hold for these reduction procedures. Yet they lead to extractions of programs from classical proofs, as demonstrated for instance by [START_REF] Miquel | Relating classical realizability and negative translation for existential witness extraction[END_REF].

By several aspects, proofnets appear as a good solution to the problem of representing proofs in classical logic. Indeed they contain and organize all the necessary information that a proof must include without getting tangled in the bureaucracy of syntax. Proofnets originate from Girard's Linear Logic [START_REF] Girard | Linear logic[END_REF] and elegantly adapt to classical logic [START_REF] Miller | A compact representation of proofs[END_REF][START_REF] Robinson | Proof nets for classical logic[END_REF][START_REF] Lamarche | Naming proofs in classical propositional logic[END_REF]. In particular Lamarche and Straßburger demonstrate that confluence and strong normalisation of the unrestricted cutelimination procedure can be recovered in the propositional case [START_REF] Lamarche | Naming proofs in classical propositional logic[END_REF]. As usual with classical logic, problems arise when adding quantifiers, as shown by the ongoing work of McKinley and Heijltjes [START_REF] Mckinley | The alpha-epsilon calculus[END_REF][START_REF] Heijltjes | Proof forests with cut based on Herbrand's theorem[END_REF].

The various existing approaches to proofnets for classical logic significantly differ by the criterion that they adopt to characterize correct proofnets. For example Robinson [Rob03] uses switchings à la Danos-Regnier whereas Lamarche and Straßburger use conjunctive resolutions [START_REF] Lamarche | Naming proofs in classical propositional logic[END_REF]. This latter criterion nicely relates to sequent calculus proofs in the following way: when considering a proofnet associated with some sequent S, conjunctive resolutions exactly correspond to the atomic sequents that one could obtain from S by decomposing all its connectives using sequent calculus inferences. Therefore the criterion states that if all these conjunctive resolutions are actually proved, then the proofnet is correct. It corresponds for instance to the tableaux method criterion if all branches of a tableau are closed, the formula represented by the tableau is unsatisfiable. The advantage of this last criterion is that branches of a tableau as well as branches of a sequent calculus derivation are easily extractable. On the contrary, the extraction of subnets using conjunctive resolutions is not trivial: a proofnet may have an exponantial number of conjunctive resolutions whereas a derivation always have a linear number of branches. These complexities reflect the fact that proofnets are compressed derivations. In order to check their value as a certificate, their information must be decoded through conjunctive resolutions.

In this paper, we propose a rendering of proofnets in a three dimensional space. This rendering is meant to ease the extraction of subnets using conjunctive resolutions. It is based on the De Morgan duality: the (horizontal) axis which is usually employed in order to write sequents is split into an axis for conjunctions and an axis for disjunctions. Sequents and proofnets therefore become respectively two-dimensional and threedimensional objects. Conjunctive resolutions appear as paths and surfaces which follow to the disjunction axis. Checking the validity of a proofnet therefore becomes geometrical. As far as we know, our idea of using the De Morgan duality to represent proofnets and sequent calculus derivations in a three-dimensional space is completely novel. The only other instance of a rendering of proofs in a three-dimensional space is Yves Guiraud's work which represents SKS derivations as three-dimensional penrose diagrams [START_REF] Guiraud | The three dimensions of proofs[END_REF]. This paper is organized as follows. In section 2, we reformulate the definitions of classical proofnets and conjunctive resolutions. Then in section 3, we present successively the rendering of sequents as two-dimensional planar acyclic graphs and the rendering of proofnets and sequent calculus derivations in a three-dimensional space. Finally we present the ongoing implementation of a prototype in section 4.

Proofnets in Classical Logic

This section introduces proofnets for classical logic. Our presentation is greatly inspired by the work of Lamarche and Straßburger [START_REF] Lamarche | Naming proofs in classical propositional logic[END_REF]. The set of formulae is defined by the grammar ϕ, ψ ::

= P | P | | ⊥ | {z } atoms | ϕ ∧ ψ | ϕ ∨ ψ .
Formulae are built from atomic predicates (P ), negated atomic predicates ( P ), false (⊥), true ( ), conjunctions (ϕ ∧ ψ) and disjunctions (ϕ ∨ ψ). The negation ¬ϕ of a formula ϕ is defined inductively by

¬P = P , ¬ P = P , ¬⊥ = , ¬ = ⊥ , ¬(ϕ ∧ ψ) = (¬ϕ) ∨ (¬ψ) , ¬(ϕ ∨ ψ) = (¬ϕ) ∧ (¬ψ) .
We suppose given an infinite countable set of names. Symbols x, y, z will range over this set of names. A named formula is a pair containing a name x and a formula ϕ and denoted x : ϕ. A sequent L is a set of named formulae such that to any name x corresponds at most one formula ϕ such that x : ϕ ∈ L. Such a sequent is denoted x1 : ϕ1, . . . , xn : ϕn or ϕ1, . . . , ϕn when names are insignificant. A position is a finite binary sequence. The empty position will be denoted ε. If ϕ is a formula and l is a position, the subformula of ϕ occurring at position l, denoted ϕ |l , is defined by

P |ε = P , P|ε = P , ⊥ |ε = ⊥ , |ε = , (ψ0 ∧ ψ1) |i•l = ψi |l , (ψ0 ∨ ψ1) |i•l = ψi |l ( i ∈ {0, 1} ) .
Remark that ϕ |l is not defined for all formulae and all positions. If ϕ is a formula, the set of positions of ϕ, denoted Pϕ is the set of positions l such that ϕ |l is actually defined. Let us consider for example the formula ∨ (P ∧ ). It admits five positions, namely ε, 0, 1, 10 and 11. They correspond respectively to the subformulae ∨ (P ∧ ), , P ∧ , P and . A sequent position is a pair containing a name x and a position l and denoted x • l. In what follows, we will improperly say position instead of sequent position. Let L be a sequent. The set of (sequent) positions of L is the set

PL = { x • l / x : ϕ ∈ L and l ∈ Pϕ } .
Therefore if L = x1 : ϕ1, . . . , xn : ϕn is a sequent and xi • l ∈ PL, the subformula of L occurring at position xi • l, denoted L |x i •l , is the formula ϕi |l . We are now able to define proofnets.

Definition 1 (Proofnets).

A proofnet is a pair (L, ∼) where L is a sequent and ∼ is symmetric relation on PL such that whenever l ∼ m, then either If s is a conjunctive resolution for L, the set of positions of s, denoted P s L , is the subset of positions

L |l = ¬L |m or L |l = L |m = .
(x • l) ∈ PL such that for all (x • m) ∈ P ∧ L , if m is a strict prefix of l, then the binary sequence m • s(m) is also a prefix of l.
Definition 2 (Valid Proofnets). A proofnet (L, ∼) is valid if for all conjunctive resolution s of L, the restriction of ∼ to P s L (that is to say the set ∼ ∩(P s L × P s L )) is not empty. Let us consider for example the proofnet depicted in figure 1. Its conjunctive positions are x•1 and y. Therefore the sequent corresponding to this proofnet admits four conjunctive resolutions which are

 x • 1 → 0 y → 0 ,  x • 1 → 1 y → 0 ,  x • 1 → 0 y → 1 and  x • 1 → 1 y → 1 .
These conjunctive resolutions correspond to the positions of the subtrees depicted in figure 2. This figure also represents the restriction of the relation associated with each conjunctive resolution. Notice that the third conjunctive resolution returns an empty restriction of the proofnet relation. Consequently the proofnet of figure 1 is not a valid proofnet. This can easily be corrected though, for example by linking the position x • 0 to itself. In order to represent proofnets with cuts, Lamarche and Straßburger use a new binary connective [START_REF] Lamarche | Naming proofs in classical propositional logic[END_REF]. This connective is in fact just a conjunction (and is indeed treated as a conjunction), consequently replacing the cut rule

Cut Γ, ϕ, ∆ Γ, ¬ϕ, ∆ Γ, ∆ by the rule Cut' Γ, ϕ ∧ (¬ϕ), ∆ Γ, ∆ .
Therefore cut-formulae are special conjunctions that are denoted ϕ ψ instead of ϕ ∧ ψ. They cannot occur inside another (cut)-formula: in a sequent L = x1 : ϕ1, . . . , xn : ϕn, the only positions corresponding to cut-formulae are of the form xi • ε. In addition, if (L, ∼) is a proofnet and xi • ε is a position corresponding to a cut-formula, then for all l ∈ PL, (xi • ε) ∼ l. Cut-formulae are handled in the same way as conjunctions with respect to conjunctive resolutions. If L is a sequent containing no 1 cut-formula and L is a sequent only containing cut-formulae, then any proofnet (L ∪ L , ∼) will be said to be a proofnet for L with cuts L . If L is empty, the proofnet is cut-free.

Valid proofnets are sound and complete with respect to the classical cut-free sequent calculus and valid proofnets with cuts are sound and complete with respect to the classical sequent calculus with cuts as demonstrated by the following theorem.

Theorem 1. For some sequent L, there exists a valid proofnet for L if and only if there exists a derivation of L in the cut-free classical sequent calculus. For some sequent L, there exists a sequent L as well as a valid proofnet for the sequent L with cuts L if and only if there exists a derivation of L in the classical sequent calculus with cuts.

Proof. Adaptation of the proof available in [START_REF] Lamarche | Naming proofs in classical propositional logic[END_REF].

We will not formally introduce a cut-elimination procedure for classical proofnets in this paper. One is described by Lamarche and Straßburger in [START_REF] Lamarche | Naming proofs in classical propositional logic[END_REF] for their presentation of proofnets. Let us remark that their B-nets are a subclass of our valid proofnets: they just restrict the use of links l ∼ m to positions l and m corresponding to atoms. In addition, their cutelimination procedure does not use any restricting strategy and remains confluent and strongly normalising on B-nets. Therefore we believe that it could be extended to an unrestricted confluent and strongly normalising cut-elimination procedure for our presentation of proofnets. However we leave the formalisation of such a procedure for a subsequent paper.

Third Dimension

Before representing proofnets in a three-dimensional space, we represent sequents in a two-dimensional space. This is done using planar acyclic directed graphs having exactly one source and one sink. We first define two auxiliary operations on such graphs. If A and B are two acyclic

P P P ⊥ ⊥ Figure 3: ∨ (P ∧ ), (P ∨ ( P ∨ ⊥)) ∧ ( ∨ ⊥)
directed graphs, the graph A|B is the acyclic directed graph obtained by linking the sink of A with the source of B; the graph A B is the graph obtained by adding a fresh source linked to the sources of A and B and a fresh sink to whom the sinks of A and B are linked. These operations preserve both properties of being acyclic and planar. Now let us consider the list of atoms that occur in a sequent. Such a list is obviously a one-dimensional object that does not render the logical structure of the sequent. This logical structure is inherited from the connectives of the sequent and is translated into conjunctive resolutions that select sublists of the initial list of atoms. Then in order to prove the sequent, a link must be found for each sublist. We propose to replace the one-dimensional list of atoms by a two-dimensional object representing the whole sequent and therefore containing the logical structure which corresponds to the conjunctive resolutions: the rendering of a formula ϕ, denoted ϕ , is the acyclic directed planar graph with exactly one source and one sink defined as

• a graph with a single node labelled by ϕ if ϕ is an atom ;

• ψ1 | ψ2 if ϕ = ψ1 ∨ ψ2 ; • ψ 1 ψ 2 if ϕ = ψ1 ∧ ψ2 .
The graph ϕ1, . . . , ϕn associated with a sequent ϕ1, . . . , ϕn is the graph ϕ1 | . . . | ϕn . For example, the graph ∨ (P ∧ ), (P ∨ ( P ∨ ⊥)) ∧ ( ∨ ⊥) is represented in figure 3. Now let L be some sequent. Each directed path from the source of L to its sink corresponds to a sequent a1, . . . , an where the ai are the labels of the nodes of the path. These are exactly the sequents that one would obtain by decomposing all the connectives of L using sequent calculus rules. These also are precisely the sequents that appear in the subnets corresponding to each conjunctive resolution of L. In particular it holds for the graph in figure 3 and the conjunctive resolutions in figure 2: in this case, the sequents are , P, P, P , ⊥ , , , P, P , ⊥ , , P, , ⊥ and , , , ⊥ .

For any sequent L, the graph L is meant to be rendered on the plane. If we choose the horizontal axis to represent disjunctions (following the tradition of writing sequent ϕ1, . . . , ϕn horizontally) and the vertical axis to represent conjunctions. A graph ϕ∨ψ = ϕ | ψ is then rendered as the horizontal sequence ϕ → ψ and a graph ϕ∧ψ = ϕ ψ is rendered as the vertical fork • ϕ ψ • . This rendering behaves quite well with respect to negation which then stands for an exchange of the disjunction axis and the conjunction axis (for example a ninety degree rotation): the graph associated with the negation of the sequent ∨ (P ∧ ), (P ∨ ( P ∨ We are now able to render sequents in a two-dimensional space. This rendering is a recursive decomposition of the connectives in the sequent. We can render this iteration with respect to a third axis called decomposition axis which is added to the conjunction axis and the disjunction axis. Disjunctions and conjunctions are rendered in the following way. The rendering of a formula consists in the recursive rendering of its connectives, therefore obtaining a three-dimensional tree. The rendering of a whole sequent consists in the rendering of each of its formulae side by side along the disjunction axis. Each step of such a rendering corresponds to a partially computed graph. Each decomposition of a connective corresponds to a computation further towards the final graph corresponding to the initial sequent. The final three-dimensional forest displays on top of it the completed graph corresponding to the initial sequent. For example, figure 5 displays the three-dimensional proofnet associated with the sequent ∨ (P ∧ ), (P ∨ ( P ∨ ⊥)) ∧ ( ∨ ⊥). It also displays several graphs corresponding to partial decompositions of its connectives, that is to say from bottom to top the graphs for

[ ∨ (P ∧ )] | [(P ∨ ( P ∨ ⊥)) ∧ ( ∨ ⊥)] , [ ] | [(P ∧ )] | [P ∨( P ∨⊥)] [ ∨⊥] , [ ] | [P ] [ ] | [P ] | [ P ∨⊥] [ ] | [⊥]
and

[ ] | [P ] [ ] | [P ] | [ P ] | [⊥] [ ] | [⊥]
.

Note that we could also have represented oblique graphs such as the one corresponding to the decomposition step [ ]

| [P ] [ ] | [P ∨( P ∨⊥)] [ ∨⊥]
. We have not dealt yet with the rendering of the relation ∼ of a proofnet (L, ∼). If l and m are positions of L such that l ∼ m, both positions l We have seen that in terms of two-dimensional graphs, negation stands for the exchange of the disjunction axis and the conjunction axis. It also remarkably holds for three-dimensional proofnets: the vertices corresponding to formulae as well as the triangles corresponding to decompositions of connectives are unchanged. However all the parts of the threedimensional proofnet only corresponding to the directed graphs have to be switched as done in figure 4.

If L is a sequent, each directed path from the source of L to its sink correspond to an atomic sequent. The list of such paths (or equivalently such sequents) is an expanded version of the graph L . Let us remark that the size of the list of paths can be exponantial with respect to the size of the initial graph (think of a sequent ϕ1 ∧ ψ1, ϕ2 ∧ ψ2, . . . , ϕn ∧ ψn). This expansion corresponds to the expansion that one must perform to transform a proofnet into a sequent calculus derivation. Each two-dimensional graph can be expanded into a two-dimensional list of sequents and each three-dimensional proofnet can be expanded into a three-dimensional sequent calculus derivation. This expansion is also known as sequentialization. The difference between proofnets and sequent calculus is that in the latter only one connective is decomposed at a time. The contexts (that is to say the other formulae of the sequent) are just copied in the conclusion and in the premisses of the inference. Sequentialization therefore stands for transforming one big step containing several simultaneous decompositions into several steps each containing a decomposition and several duplications. These smaller steps correspond either to a sequent calculus introduction of the ∧ connective or to a sequent calculus introduction of the ∨ connective. The following picture displays on its left a three-dimensional sequent calculus introduction of a conjunction and on its right a three-dimensional sequent calculus introduction of a disjunction. In such three-dimensional inferences, a sequent is represented by a segment parallel to the disjunction axis. From the bottom-up point of view, on the left the decomposition of a segment . . . ϕ1, ψ1 ∧ ψ2, ϕ2, ϕ3 . . . creates two new segments . . . ϕ1, ψ1, ϕ2, ϕ3 . . . and . . . ϕ1, ψ2, ϕ2, ϕ3 . . . ; on the right the decomposition of a segment . . . ϕ1, ψ1 ∨ ψ2, ϕ2, ϕ3 . . . creates one new segment . . . ϕ1, ψ1, ψ2, ϕ2, ϕ3 . . . . The duplication of contexts is represented by the dashed lines. Using these three-dimensional inferences, we can build three-dimensional sequent calculus derivations. For example the three-dimensional derivation corresponding to , P, P, P , ⊥ , P, P, ( P ∨ ⊥)

, P, (P ∨ ( P ∨ ⊥))

, P, , ⊥ , P, ( ∨ ⊥)

, P, (P ∨ ( P ∨ ⊥)) ∧ ( ∨ ⊥)

, , P, P , ⊥ , , P, ( P ∨ ⊥)

, , (P ∨ ( P ∨ ⊥))

, , , ⊥ , , ( ∨ ⊥)

, , (P ∨ ( P ∨ ⊥)) ∧ ( ∨ ⊥)

, P ∧ , (P ∨ ( P ∨ ⊥)) ∧ ( ∨ ⊥) ∨ (P ∧ ), (P ∨ ( P ∨ ⊥)) ∧ ( ∨ ⊥)
is displayed in figure 6. Let us remark that between the sequent calculus derivation and its three-dimensional rendering, there is a one-to-one correspondence between vertices and formulae occurrences as well as sequents occurrences and segments parallel to the disjunction axis. The same three-dimensional derivation can be obtained by sequentializing the three-dimensional proofnet of figure 5. Sequentialization mainly consists in the choice of an order for the decompositions of the connectives of the initial sequent. For example if a sequent contains both formulae ϕ1 ∧ ϕ2 and ψ1 ∨ ψ2, one can either choose to decompose the conjunction or the The sequentialization of a three-dimensional proofnet is therefore not unique: the precise critical pair underlined by these two sequent calculus derivations is translated into sequentialization steps from threedimensional proofnets to three-dimensional sequents in figure 7. Note that the sequents that appear on top of each sequent derivations are exactly those on top of each three-dimensional derivation and are also precisely the paths of the directed graph on top of the three-dimensional proofnet. This illustrates perfectly Kleene's well-known result [START_REF] Stephen | Permutability of inferences in gentzen's calculi lk and lj[END_REF] which states that the order for decomposing propositional connectives is irrelevant in sequent calculus.

Prototype

We are currently developping a prototype for rendering derivations and proofnets using 3D computer graphics. It will include several features enhanced by a point-and-click interface based on the three-dimensional rendering. In particular we will implement methods for checking derivations and proofnets as well as procedures for automatic and interactive proof construction. Sequentialization will also be implemented. For this prototype, we have chosen the tom language1 [BBK + 07] which provides powerful associative rewriting capabilities and strategic programmation on top of java. It is especially designed to manipulate tree structures with the following advantages. First of all, the expressiveness of the language allows for clean and short code. This is particularly important because we wish to implement a proofchecking kernel. The smaller the proofchecker is, the easier it is to convince everyone that it is actually sound. Another interesting feature of tom is the expression of tacticals by strategies.

Figure 8: A 3d proofnet rendered by an early version of our prototype

The tom strategy language is directly inspired from early research on elan [VB98] and ρ-calculus and allows to compose basic strategies to express complex programs using strategy combinators. We therefore believe that tom is greatly adapted to the implementation of automatic and interactive proof-search strategies. Finally since tom works on top of java, implementing our prototype in tom allows us to access any java library designed to render three-dimensional objects such as OpenGL implementations. A picture produced by an early version of our prototyped are displayed in figure 8.

Conclusion

We have presented a two-dimensional rendering of formulae and sequents through planar acyclic directed graphs. Such a graph contains the whole logical structure of the corresponding sequent: conjunctive resolutions exactly match the maximal paths of the graph (also known as the paths from the source to the sink). Then we have presented a three-dimensional rendering of proofnets which depicts the iterative construction of a graph from a given sequent. The two-dimensional graphs as well as the threedimensional proofnets are constructed on top of the De Morgan duality between conjunctions and disjunctions. Indeed the two-dimensional space that is used to render formulae and sequents is defined by a conjunction axis and a disjunction axis respectively designed to represent conjunctions and disjunctions. Interestingly negation then stands for an exchange of these two axis and does not modify further the placement of the nodes in a graph neither the structure of a proofnet. We also have presented a three-dimensional rendering of sequent calculus derivations. It is based on the same duality between the conjunction axis and the disjunction axis and sequents are displayed as segments along this latter axis. This rendering of derivations does not behave so well with respect to negation. However its main advantage is the one of sequent calculus derivations over proofnets: the former stand for a fully expanded certificate. Indeed proofnets can be unfolded into sequent calculus derivations through a sequentialization process. We have shown how this process can be rendered into a three-dimensional sequentialization transforming three-dimensional proofnets into three-dimensional derivations. Finally we have presented the current state of the implementation of our prototype for a prover based on this three-dimensional rendering of proofnets and sequent calculus derivations. We also have explained our choice of tom on top of java for an implementation language. This work opens several perspectives. First of all and without thinking about three-dimensional rendering, the proofnet approach remains fairly unexplored, especially with respect to full predicate logic with quantifiers. In particular the question of the existence of a confluent and strongly normalising cut-elimination procedure for proofnets with quantifiers remains unanswered (as far as we know). Let us also remark that we leave the treatment of cut-elimination for a subsequent paper. These developments will then lead to developments with respect to our three-dimensional rendering. Indeed rendering proofnets with quantifiers as well as rendering cut-elimination are the next extensions that we wish to study. These extensions should also be implemented along all the implementation objectives listed in section 4.

Figure 1 Figure 1 :

 11 Figure 1 depicts a proofnet whose sequent is x : ∨ (P ∧ ), y : (P ∨ ( P ∨ ⊥)) ∧ ( ∨ ⊥) and whose relation is the symmetric closure of {(x • 11, x • 11), (x • 1, y • 01), (y • 00, y • 010)}. Proofnets are meant to represent possibly unfinished derivations in the cut-free classical sequent calculus. In a proofnet (L, ∼), a link x•l ∼ y •m with ϕ = L |x•l = ¬L |y•m represents the use of the rule axiom and a link l ∼ m with L |x•l = L |y•m = represents the use of the rule introducing . It is obviously important to characterize which proofnets represent completed derivations. For that we reformulate the notion of conjunctive resolution that is introduced by Lamarche and Straßburger [LS05]. The conjunctive positions of a sequent L are the positions x • l such that L |x•l is a conjunction. The set of conjunctive positions of a sequent L is denoted P ∧ L . A conjunctive resolution for a sequent L is a function s : P ∧ L → B.

Figure 2 :

 2 Figure 2: Conjunctive resolutions for the proofnet in figure 1

Figure 4 :

 4 Figure 4: Negation of the graph in figure 3

Figure 5 :

 5 Figure 5: A three-dimensional proofnet

Figure 6 :

 6 Figure 6: A three-dimensional sequent calculus derivation

Figure 7 :

 7 Figure 7: Sequentialization steps

tom.loria.fr