3 resultados para proof of knowledge

em Nottingham eTheses


Relevância:

100.00% 100.00%

Publicador:

Resumo:

This paper examines the relationship between the state and the individual in relation to an aspect of mundane family life – the feeding of babies and young children. The nutritional status of children has long been a matter of national concern and infant feeding is an aspect of family life that has been subjected to substantial state intervention. It exemplifies the imposition upon women the ‘biologico-moral responsibility’ for the welfare of children (Foucault 1991b). The state’s attempts to influence mothers’ feeding practices operate largely through education and persuasion. Through an elaborate state-sponsored apparatus, a strongly medicalised expert discourse is disseminated to mothers. This discourse warns mothers of the risks of certain feeding practices and the benefits of others. It constrains mothers through a series of ‘quiet coercions’ (Foucault 1991c) which seek to render them self-regulating subjects. Using data from a longitudinal interview study, this paper explores how mothers who are made responsible in these medical discourses around child nutrition, engage with, resist and refuse expert advice. It examines, in particular, the rhetorical strategies which mothers use to defend themselves against the charges of maternal irresponsibility that arise when their practices do not conform to expert medical recommendations.

Relevância:

100.00% 100.00%

Publicador:

Resumo:

Coinduction is a proof rule. It is the dual of induction. It allows reasoning about non--well--founded structures such as lazy lists or streams and is of particular use for reasoning about equivalences. A central difficulty in the automation of coinductive proof is the choice of a relation (called a bisimulation). We present an automation of coinductive theorem proving. This automation is based on the idea of proof planning. Proof planning constructs the higher level steps in a proof, using knowledge of the general structure of a family of proofs and exploiting this knowledge to control the proof search. Part of proof planning involves the use of failure information to modify the plan by the use of a proof critic which exploits the information gained from the failed proof attempt. Our approach to the problem was to develop a strategy that makes an initial simple guess at a bisimulation and then uses generalisation techniques, motivated by a critic, to refine this guess, so that a larger class of coinductive problems can be automatically verified. The implementation of this strategy has focused on the use of coinduction to prove the equivalence of programs in a small lazy functional language which is similar to Haskell. We have developed a proof plan for coinduction and a critic associated with this proof plan. These have been implemented in CoClam, an extended version of Clam with encouraging results. The planner has been successfully tested on a number of theorems.

Relevância:

100.00% 100.00%

Publicador:

Resumo:

Proof critics are a technology from the proof planning paradigm. They examine failed proof attempts in order to extract information which can be used to generate a patch which will allow the proof to go through. We consider the proof of the $quot;whisky problem$quot;, a challenge problem from the domain of temporal logic. The proof requires a generalisation of the original conjecture and we examine two proof critics which can be used to create this generalisation. Using these critics we believe we have produced the first automatic proofs of this challenge problem. We use this example to motivate a comparison of the two critics and propose that there is a place for specialist critics as well as powerful general critics. In particular we advocate the development of critics that do not use meta-variables.