bluuebunny/crossref_metadata_2025 huggingface dataset:
Interaction of hypothalamic Na,K-ATPase inhibitor with isolated human peripheral blood mononuclear cells
Authors: Anner Beatrice M. , Lacotte Danielle , Anner Rolf M. , Moosmayer Marlis
Published: February 2005

A ligand for the digitalis receptor located on the membrane-embedded Na,K-ATPase (NKA; EC 3.6.1.37) has been isolated from bovine hypothalamus (hypothalamic inhibitory factor; HIF) and identified as isomeric ouabain (Tymiaket al, 1993,Proc. Natl. Acad. Sci.90: 8189–8193). In analogy to cardioactive steroids (CS) derived from plants or from toad, HIF inhibits the Na/K-exchange process and the ATPase activity of isolated Na,K-ATPase although by a different molecular action mechanism. In the present work we show that, as plant-derived ouabain, HIF inhibits86Rb-uptake by isolated human lymphocytes with an IC50 of about 20 nM; above this concentration HIF reduces cell viability in contrast to ouabain. The decrease in cell viability by excess HIF is accompanied by discrete morphological alterations (mitochondrial swelling) visible by transmission electron microscopy of ultra-thin sectioned peripheral blood mononuclear cells. Taken together the results show that the hypothalamic NKA inhibitor blocks NKA of isolated human lymphocytes with high potency at nanomolar concentrations without toxicity; concentrations exceeding the ones required to block86Rb-uptake reduce cell viability, probably due to leak formation across the NKA molecule. Thus, lymphocytes constitute a potential target for HIF action and by their altered NKA status a possible messenger between the nervous and the immune system.
Safety and progress of recursive procedures
Authors: Hesselink Wim H.
Published: February 2005

Temporal weakest precondions are introduced for calculational reasoning about the states encountered during execution of not-necessarily terminating recursive procedures. The formalism can distinguish error from useful nontermination. The precondition functions are constructed in a new and more elegant way. Healthiness laws are discussed briefly. Proof rules are introduced that enable calculational proofs of various safety and progress properties. The construction of the precondition functions is justified in an Appendix that provides the operational semantics.
A logic for Miranda, revisited
Authors: Thompson Simon
Published: February 2005

This paper expands upon work begun in [Tho89], in building a logic for the Miranda functional programming language. After summarising the work in that paper, a translation of Miranda definitions into logical formulas is presented, and illustrated by means of examples. This work expands upon [Tho89] in giving a complete treatment of sequences of equations, and by examining how to translate the local definitions introduced by where clauses.

The status of the logic is then examined, and it is argued that the logic extends a natural operational semantics of Miranda, given by the translations of definitions into conditional equations.

Finally it is shown how the logic can be implemented in the Isabelle proof tool.
Recursion induction for real-time processes
Authors: Davies Jim , Schneider Steve
Published: February 2005

The theory of timed Communicating Sequential Processes is a mathematical approach to the design and analysis of timed distributed systems. This paper extends the language of timed CSP to include a general treatment of recursion. A semantics for mutual recursion is introduced, together with a sufficient condition for the necessary fixpoint to be unique. The resulting language has the familiar unwinding property of process algebra, and exhibits a number of useful algebraic identities. A theory of recursion induction is formulated, and a simple example is presented to illustrate its use.
Proof movie — A proof with the Boyer-Moore prover
Authors: Weber-Wulff Debora
Published: February 2005

This paper uses the Boyer-Moore prover for developing a proof of correctness for the implementation of a very small compiler. The polished version of the proof is included as an appendix. The major intent of the paper is to describe the process of proving using an automatic theorem prover.
Axiomatic treatment of processes with shared variables revisited
Authors: Owe Olaf
Published: February 2005

The aim of this paper is to develop simple and practically useful formalisms for reasoning about processes with shared variables. Our approach is based on the axiomatic system described by Neelam Soundararajan. In contrast to that work, our formalism is first derived from a model; this guarantees soundness and completeness of the formal proof system, with respect to the model. As an additional advantage the rules become simpler than those of Soundararajan; in particular, the local assertions may freely refer to shared variables; and we remove the explicit use of the compatibility predicate.

Next we augment the formalism by allowing global invariants, which may refer to shared variables (including shared histories), but with a different semantics than in the local assertions. The augmented system makes reasoning simpler in the sense that reasoning about the past is replaced by reasoning about the present. Finally we suggest a sufficiently complete set of mythical (auxiliary) variables free from embedded program structure. We demonstrate our formalism on some examples.
An implementation of syntax directed functional programming on nested-stack machines
Authors: Fassbender Heinz , Vogler Heiko
Published: February 2005

This paper contributes to the field of functional programming languages. We investigate the call-by-name and call-by-need implementation of a restricted type of functional programming, calledsyntax directed functional programming; the target of this implementation is an abstract machine that is based on nested stacks. In fact, the technical kernel of this paper is a refinement of an automata theoretical result that, roughly speaking, investigates the well-known relationship “recursion = iteration + stack” in the framework of tree transducers. More precisely, in the underlying result the class of functions computed by total deterministic macro tree-to-string transducers with the call-by-name computation strategy is characterized by total deterministic checking-tree nested-stack transducers. Note that total deterministic macro tree-to-string transducers are term rewriting systems by means of which the reduction semantics of syntax directed functional programming languages can be described.
Equality of agent expressions is preserved under an extension of the universe of actions
Authors: Massart T. , Devillers R.
Published: February 2005

In a basic agent calculus, equality often links the agents which provide the same external behaviour in any context. Since the universe of agents and the universe of contexts depend on the used action set, equality depends a priori on this set of actions. We show here that if we select from the universe of agents, two agents which are equal, they are also equal if we extend the universe of actions (and consequently if we extend the universe of agents and contexts).
A demonstrably correct compiler
Authors: Stepney Susan , Whitley Dave , Cooper David , Grant Colin
Published: February 2005

As critical applications grow in size and complexity, high level languages, rather than better-trusted assembly languages, will be used in their development. This adds potential for extra errors to creep in, especially in the now necessary compiler. To avoid these new errors, it is necessary to have a formal specification of the high level language, and a formal development of its compiler. We outline what we believe is a practical route for achieving a demonstrably correct compiler, and describe a prototype compiler we have built by this route for a small, but non-trivial, language.
Theories for mechanical proofs of imperative programs
Authors: Hesselink Wim H.
Published: February 2005

For convenient application of a first-order theorem prover to verification of imperative programs, it is important to encapsulate the operational semantics in generic theories. The possibility to do so is illustrated by two theories for the Boyer-Moore theorem prover Nqthm.

The first theory is an Nqthm version of the classical while-theorem. Here the main interest is to show how one can use Nqthm's facilities to constrain and to functionally instantiate for the development and application of a generic theory. The theory is illustrated by a linear search program.

The second theory is a finitary approach to progress for shared-memory concurrent programs. It is illustrated by Peterson's algorithm for mutual exclusion of two processes. The proof of progress for Peterson's algorithm is new. The assertion of bounded fairness is slightly stronger than the conventional notion of weak fairness. This new concept may have other applications.
Verifying programs in the calculus of inductive constructions
Authors: Parent-Vigouroux Catherine
Published: February 2005

This paper deals with a particular approach to the verification of functional programs. A specification of a program can be represented by a logical formula [Con86, NPS90]. In a constructive framework, developing a program then corresponds to proving this formula. Given a specification and a program, we focus on reconstructing a proof of the specification whose algorithmic contents corresponds to the given program. The best we can hope is to generate proof obligations on atomic parts of the program corresponding to logical properties to be verified. First, this paper studies a weak extraction of a program from a proof that keeps track of intermediate specifications. From such a program, we prove the determinism of retrieving proof obligations. Then, heuristic methods are proposed for retrieving the proof from a natural program containing only partial annotations. Finally, the implementation of this method as a tactic of theCoqproof assistant is presented.
The semantics of the combination of atomized statements and parallel choice
Authors: Knijnenburg Peter M. W. , Kok Joost N.
Published: February 2005

In this paper we define a uniform language
ℒ
that is an extension of the language underlying the process algebra
PA
. One of the main extensions of this language over
PA
is given by so-called atomizing brackets. If we place these brackets around a statement then we treat this statement as an atomic action. Put differently, these brackets remove all interleaving points. We present a transition system for the language and derive its operational semantics. We show that there are several options for defining a transition system such that the resulting operational semantics is a conservative extension of the semantics for
PA
. We define a semantic domain and a denotational model for the language. Next we define a closure operator on the semantic domain and show how to use this closure operator to derive a fully abstract denotational semantics. Then the algebraic theory of the language is considered. We define a collection of axioms and a term rewrite system based on these axioms. Using this term rewrite system we are able to identify normal forms for the language. It is shown that these axioms capture the denotational equality. It follows that if two terms are provably equal then they have the same operational semantics. Finally, we show how to extend the axiomatization in order to axiomatize its operational equivalence.
Verification of schedulability for real-time programs
Authors: Liu Zhiming , Joseph Mathai , Janowski Tomasz
Published: February 2005

Assume that a real-time program
P
T
consisting of a number of parallel processes is executed on a system having a set
Pr
of processors which are shared between the processes by a real-time scheduler
S
T
. Assume that P
T
must meet some timing deadlines. We show that such an implementation of
P
T
can be represented as a transformationL(
P
T
) and that the deadlines of
P
T
will be met if they are satisfied by the timing properties of the transformed program. The condition for feasibility of a real-time program executed under a scheduler is formalized and rules are provided for verification. The scheduler
S
T
can be specified
generically
and applied to different programs, making it unnecessary to introduce low-level operations such as scheduling primitives into the programming language. Thus real-time program specification and Schedulability can be considered in the same framework and the timing properties of a program can be determined at the specification level. By separating the specification of the scheduler from that of the program, the feasibility of an implementation can be proved by considering a scheduling policy rather than its implementation details.
A method for showing progress
Authors: Leino K. Rustan M.
Published: February 2005

Charmed by the ease with which [vdS95] shows that its program makes progress, I state a theorem that allows for showing progress of a UNITY-like program in an easy way. I also give a proof of that theorem.
Response to “the formal specification of safety requirements for storing explosives”
Authors: Larsen Peter Gorm
Published: February 2005

This short communication is a response to [MuS93] investigating their ACS system specification. The main point in this paper is that executing specifications can be used as a feasible way of validating them. It is essential to have tool support which enables one to write a generally not executable specification, and then prototype (parts of) it directly in the specification language, without translating it into some other prototyping language.
How to write a long formula
Authors: Lamport Leslie
Published: February 2005

Standard mathematical notation works well for short formulas, but not for the longer ones often written by computer scientists. Notations are proposed to make one or two-page formulas easier to read and reason about.
Action transducers and timed automata
Authors: Lynch Nancy , Vaandrager Frits
Published: February 2005

The
timed automaton model
of [LyV92, LyV93] is a general model for timing-based systems. A notion of
timed action transducer
is here defined as an automata-theoretic way of representing operations on timed automata. It is shown that two timed trace inclusion relations are substitutive with respect to operations that can be described by timed action transducers. Examples are given of operations that can be described in this way, and a preliminary proposal is given for an appropriate language of operators for describing timing-based systems.
Automatic verification of a class of systolic circuits
Authors: Abdulla Parosh
Published: February 2005

Systolic circuits have attracted considerable attention as a means of implementing parallel algorithms in areas such as linear algebra, signal processing, pattern matching, etc. A systolic circuit is composed of a number of computation cells which are connected in a regular pattern. Each cell can perform computations, store data and communicate with other cells in the circuit. We define a language to describe implementations and specifications of a class of systolic circuits whose cells compute over a commutative ring, and present a decision method to check whether or not a circuit implementation fulfils a specification. The main advantage of our approach, compared with earlier work in the field, is that the verification is performed automatically, without user interaction. We give an example of how the method may be applied to verify a convolution circuit.
Type inference with non-structural subtyping
Authors: Palsberg Jens , Wand Mitchell , O'Keefe Patrick
Published: February 2005

We present an O(n
3
) time type inference algorithm for a type system with a largest type
Τ
, a smallest type ⊥, and the usual ordering between function types. The algorithm infers type annotations of least shape, and it works equally well for recursive types. For the problem of typability, our algorithm is simpler than the one of Kozen, Palsberg, and Schwartzbach for type inference
without
⊥. This may be surprising, especially because the system with ⊥ is strictly more powerful.
Equivalence of formal semantics definition methods
Authors: Caswell M. J. A.
Published: February 2005

There are numerous methods of formally defining the semantics of computer languages. Each method has been designed to fulfil a different purpose. For example, some have been designed to make reasoning about languages as easy as possible; others have been designed to be accessible to a large audience and some have been designed to ease implementation of languages. Given two semantics definitions of a language written using two separate semantics definition methods, we must be able to show that the two are in fact equivalent. If we cannot do this then we either have an error in one of the semantics definitions, or more seriously we have a problem with the semantics definition methods themselves.

Three methods of defining the semantics of computer languages have been considered, i.e. Denotational Semantics, Structural Operational Semantics and Action Semantics. An equivalence between these three is shown for a specific example language by first defining its semantics using each of the three definition methods. The proof of the equivalence is then constructed by selecting pairs of the semantics definitions and showing that they define the same language.
A strict functional language with cyclic recursive data
Authors: Nishimura Susumu
Published: February 2005

The paper proposes a strict functional language to program with cyclic recursive data structures. In the language, each recursive datum is represented by a system of equations. Cyclic structures are naturally expressed by this representation, and the language provides a general mechanism that transforms several such systems of equations into a single new system of equations. An operational semantics and a polymorphic type system for the language are given, and a type soundness proof is sketched. Finally, it is also shown that the language can be implemented in a data-parallel fashion.
Presupposition failure — A comedy of errors
Authors: van Eijck Jan
Published: February 2005

Presuppositions of utterances are the pieces of information you convey with an utterance no matter whether your utterance is true or not. We first study presupposition in a very simple framework of updating propositional information, with examples of how presuppositions of complex propositional updates can be calculated. Next we move on to presuppositions and quantification, in the context of a dynamic version of predicate logic, suitably modified to allow for presupposition failure. In both the propositional and the quantificational case, presupposition failure can be viewed as error abortion of procedures. Thus, a dynamic assertion logic which describes the preconditions for error abortion is the suitable tool for analysing presupposition.
Specification and refinement of networks of asynchronously communicating agents using the assumption/commitment paradigm
Authors: Stølen Ketil , Dederichs Frank , Weber Rainer
Published: February 2005

This paper presents an assumption/commitment specification technique and a refinement calculus for networks of agents communicating asynchronously via unbounded FIFO channels in the tradition of Kahn.

We define two types of assumption/commitment specifications, namely simple and general specifications.

It is shown that semantically, any deterministic agent can be uniquely characterized by a simple specification, and any nondeterministic agent can be uniquely characterized by a general specification.

We define two sets of refinement rules, one for simple specifications and one for general specifications. The rules are Hoare-logic inspired. In particular the feedback rules employ invariants in the style of a traditional while-rule.

Both sets of rules have been proved to be sound and also (semantic) relative complete.

Conversion rules allow the two logics to be combined. This means that general specifications and the rules for general specifications have to be introduced only at the point in a system development where they are really needed.
Architectural CCS
Authors: Krishnan Padmanabhan
Published: February 2005

In this article, we discuss the effect of architectures on behaviours and the notions of equivalence for CCS terms. Two types of architectures are considered viz, shared memory systems and distributed memory systems. Processes can be logically migrated in shared memory systems while in distributed memory systems, processes are bound to a location and require explicit migration. Communication in shared memory systems can follow the CCS principle. A complete equational characterisation of the bisimulation equivalence induced by the execution on multiprocessors requires an extended syntax; which captures the process of compiling and loading. To permit a realistic description of communication in distributed systems, asynchronous actions are required. Due to this the complete axiomatisation for the bisimulation equivalence is more sensitive to the causal structure of the processes. A practical interpretation to the complete axiomatisation of the bisimulation equivalence is also given.
Progress assumption in concurrent systems
Authors: Costa J. F. , Sernadas A.
Published: February 2005

A denotational semantics and a sound and complete inequational proof systems for processes with varying degrees of liveness is presented. New insights on
quiescence
are given concerning the Jonsson characterisation of input/output system. A theory of
transational behaviour
of the type
carry out until the end
is developed as an application of this concept of process with liveness requirements. The proposed model fully reflects the parallel composition of
transactional requirements
, giving the expected composite requirements.
A blocking model for reactive objects
Authors: Duke Roger , Bailes Cecily , Smith Graeme
Published: February 2005

Objects can be viewed as entities reacting concurrently with their environment through the sending and receiving of messages. In this paper a model for such reactive objects is constructed where messages may be blocked either by the object or by the environment. This model differentiates between output messages controlled by the object, and input messages controlled by the environment. The model is applied to define an object compatibility lattice structure enabling the construction of objects satisfying best possible compatibility requirements.
The NDB database specified in the RAISE specification language
Authors: George Chris
Published: February 2005

This paper answers a challenge designed to test the modularization features of specification languages. The RAISE Specification Language (RSL) is shown to have the power necessary to meet the challenge.

Basic features of RSL, particularly those useful for the problem, are introduced. Two solutions to the problem are exhibited. The first follows the structure of the challenge problem very closely and is model-based in style. The second shows how RSL may be written in an algebraic style.

An example of a proof of implementation is also given.
Modularising the specification of a small database system in extended ML
Authors: Kazmierczak Edmund
Published: February 2005

A case study in the modular specification and refinement of a small database system is presented in Extended ML. Two similar requirements specifications are given and a program development step from each these is presented. The structure resulting from the first program development step is similar to that given in [FiJ90] and is presented as an answer to the challenge problem given in that paper, while the second development step is presented as a possible alternative which is more suited to the Extended ML style of program development. In the context of these two development steps the module facilities of Extended ML, their role in specification and program development and their ability to meet the challenge of [FiJ90] are examined.
On sequential composition, action prefixes and process prefix
Authors: Baeten J. C. M. , Bergstra J. A.
Published: February 2005

We illustrate the difference between sequential composition in process algebra axiomatisations like ACP and action prefixing in process calculi like CCS. We define both early and late input in a general framework extending ACP, and consider various subalgebras, some very close to value passing CCS, another one close to CSP.
Role of lindane in membranes. Effects on membrane fluidity and activity of membrane-bound proteins
Authors: López-Aparicio P. , Recio M. N. , Prieto J. C. , Pérez-Albarsanz M. A.
Published: February 2005

The influence of lindane (gamma-hexachlorocyclohexane) on fluidity of plasma membranes from rat renal cortical tubules has been investigated. Preincubation with lindane increased membrane fluidity. This effect was accompanied by (i) a decrease in the transport of glucose with regard to the controls and (ii) an inhibition of the β-adrenergic stimulatory activity upon cyclic AMP accumulation. However, a significant decrease of the membrane fluidity was found when rats were injected with lindane for 12 days. The injection of lindane exerted the opposite effect on the membrane proteins, the glucose transporter and the β-adrenergic receptor, enhancing the glucose uptake and increasing the isoproterenol-stimulated cycle AMP accumulation. A possible explanation of the difference could involve a resistance to membrane disordering by lindane through a regulatory mechanism that would balance the activity of many lindane-sensitive proteins in insecticide-injected rats.
Dietary polyphenols decrease glucose uptake by human intestinal Caco‐2 cells
Authors: Johnston Kelly , Sharp Paul , Clifford Michael , Morgan Linda
Published: February 2005

The effect of different classes of dietary polyphenols on intestinal glucose uptake was investigated using polarised Caco‐2 intestinal cells. Glucose uptake into cells under sodium‐dependent conditions was inhibited by flavonoid glycosides and non‐glycosylated polyphenols whereas aglycones and phenolic acids were without effect. Under sodium‐free conditions, aglycones and non‐glycosylated polyphenols inhibited glucose uptake whereas glycosides and phenolic acids were ineffective. These data suggest that aglycones inhibit facilitated glucose uptake whereas glycosides inhibit the active transport of glucose. The non‐glycosylated dietary polyphenols appear to exert their effects via steric hindrance, and (−)‐epigallochatechingallate, (−)‐epichatechingallate and (−)‐epigallochatechin are effective against both transporters.
Inhibition of β‐oxidative respiration is a therapeutic window associated with the cancer chemo‐preventive activity of PPARγ agonists
Authors: Andela Valentine B. , Altuwaijri Saleh , Wood James , Rosier Randy N.
Published: February 2005

We demonstrate expression and coordinate induction of PPARγ and lipogenic enzymes (HMG‐CoA synthase, HMG‐CoA reductase and fatty acid synthase) in a murine lung alveolar carcinoma cell line (Line 1) treated with the PPARγ agonist troglitazone (TRO) [0–100 μM]. We postulate that TRO induces a shift in cellular energy metabolism towards fatty acid oxidation (β‐oxidative respiration). Accordingly, co‐treatment with TRO [30 μM] and increasing concentrations of trimetazidine (TMZ) [0.1–3 mM], an inhibitor of β‐oxidation, results in a dose dependent decrease cellular ATP levels and a dose dependent induction of apoptosis. These findings, suggest that inhibition of β‐oxidative respiration is a therapeutic window associated with the cancer chemo‐preventive activity of PPARγ agonists.
Expression profiling of the estrogen responsive genes in response to phytoestrogens using a customized DNA microarray
Authors: Ise Ryota , Han Dalho , Takahashi Yusuke , Terasaka Shunichi , Inoue Akio , Tanji Masao , Kiyama Ryoiti
Published: February 2005

Here, we examined phytoestrogens, isoflavones (genistein, daidzein, glycitein, biochanin A and ipriflavone), flavones (chrysin, luteolin and apigenin), flavonols (kaempferol and quercetin), and a coumestan, a flavanone and a chalcone (coumestrol, naringenin and phloretin, respectively) by means of a DNA microarray assay. A total of 172 estrogen responsive genes were monitored with a customized DNA microarray and their expression profiles for the above phytoestrogens were compared with that for 17β‐estradiol (E2) using correlation coefficients, or R values, after a correlation analysis by linear regression. While R values indicate the similarity of the response by the genes, we also examined the genes by cluster analysis and by their specificity to phytoestrogens (specific to genistein, daidzein or glycitein) or gene functions. Several genes were selected from p53‐related genes (CDKN1A, TP53I11 and CDC14), Akt2‐related genes (PRKCD, BRCA1, TRIB3 and APPL), mitogen‐activated protein kinase‐related genes (RSK and SH3BP5), Ras superfamily genes (RAP1GA1, RHOC and ARHGDIA) and AP‐1 family and related genes (RIP140, FOS, ATF3, JUN and FRA2). We further examined the extracts from two local crops of soy beans (Kuro‐daizu or Mochi‐daizu) by comparing the gene expression profiles with those of E2 or phytoestrogens as a first step in utilizing the expression profiles for various applications.
Why would cement porosity reduction be clinically irrelevant, while experimental data show the contrary
Authors: Janssen D. , Stolk J. , Verdonschot N.
Published: February 2005

Laboratory bench tests have shown that porosity reduction increases the fatigue life of bone cement specimens. Clinically, however, the effect porosity reduction is subject to debate. We hypothesized that the discrepancy between clinical and experimental findings is related to differences in the stress distribution, which is typically uniform in experimental test specimens, while stress concentrations exist in cement around hip implants. We simulated fatigue failure of cement in a finite element model of an experimental test specimen and of a transverse slice of a total hip arthroplasty with a sharp‐cornered stem. Four levels of porosity were introduced. In the fatigue test specimen model, the fatigue life clearly was dependent on the level of porosity, while in the transverse slice model, the level of porosity had virtually no effect on failure of the cement mantle. The results of the simulations confirmed our hypothesis. In simulations of laboratory tests, pores clearly acted as crack initiators, while in the simulation of a real total hip reconstruction, crack formation was governed by local stress singularities. This explains why the beneficial effect of cement porosity reduction on the lifetime of total hip reconstructions may be hard to detect clinically. © 2005 Orthopaedic Research Society. Published by Elsevier Ltd. All rights reserved.
Carbon and nitrogen isotope ratios in meteoritic organic matter: indicators of alteration processes on the parent asteroid
Authors: Sephton Mark A. , Verchovsky Alexander B. , Wright Ian P.
Published: February 2005

Macromolecular organic materials in chondrites display significant variations in carbon and nitrogen stable isotopes. In recent years, these variations have been interpreted as a record of aqueous and thermal processing on asteroids shortly after the birth of the Solar System. In this paper we review and summarize the key data and main interpretative approaches related to this study area. Armed with these methods we attempt to reinterpret the whole rock chondrite data set in the literature.
Diet of the quokka (Setonix brachyurus) (Macropodidae:Marsupialia) in the northern jarrah forest of Western Australia
Authors: Hayward M. W.
Published: February 2005

The diet of the quokka in the northern jarrah forest of Western Australia was investigated by microscopic examination of faecal pellets of known individuals and comparison with a reference collection of plant epidermal tissue. Twenty-nine plant species were identified from the 97 faecal pellet groups collected from 53 individuals, confirming that the quokka is a browsing herbivore that favours leaves and stems. Of those 29 species, 11 made up over 90% of the diet and five species accounted for 71%. Thomasia species were the most common in the diet and the most preferred; Dampiera hederacea was also preferred and these species, along with Bossiaea aquifolia, Mirbelia dilatata and Agonis linearifolia, were the five most important food items. The seasonal variation in the diet of the quokka, and that between sites, can be attributed to increases in nutrient content associated with fresh growth associated with season or vegetation seral stage after fire. The reduced dietary diversity at sites with younger seral stages (<10 years after fire) and the importance of certain species that are more common in these younger ages explains the cause of the species’ habitat preference for sites with a mosaic of young and old (>25 years after fire) age classes. The relatively short availability of sufficient, high-quality, succulent plants in the seral succession of swamps occupied by quokkas is likely to drive a regular pattern of local extinction and recolonisation.
Diving behaviour of two Ross seals off east Antarctica
Authors: Southwell Colin
Published: February 2005

The Ross seal (Ommatophoca rossii) is the least frequently sighted and least known of the Antarctic pinnipeds. Current knowledge of foraging and diving behaviour is based on observations of a single seal over <2 days. The current study provides some additional data on the diving behaviour of two Ross seals off east Antarctica over periods of 31 and 12 days during December–January 1999–2000 using satellite-linked dive recorders. Both seals remained over the continental shelf for these times, the female remaining some distance from the coast and the male moving close to the coast approximately half-way through his transmission period. Most dives by the female reached depths >150 m (maximum depth 372 m) and the modal duration was 10–11 min. The male’s dives were slightly shallower (most >100 m) and shorter (mode 6–7 min) when distant from the continental coast, and were truncated to a depth of 180 m when close to the coast, presumably by the sea floor. These dive patterns suggest that their prey species, thought to comprise mostly fish and squid, were relatively unavailable at depths <100 m.
Body condition assessment and prediction of fasting endurance in wild rabbits (Oryctolagus cuniculus)
Authors: Boos M. , Thouzeau C. , Delacour G. , Artois M. , Marchandeau S. , Jean-Claude P. , Robin J.-P.
Published: February 2005

In many species, reproductive success, resistance to food shortage and immune response to parasitism depend on body nutrient reserves. Thus, determining body fuels is important for studying the impact of the environment on animal fitness. As an alternative to the usual biochemical methods, we have defined models for estimating body composition in rabbits (Oryctolagus cuniculus). The accuracy of the indices obtained on a source group was tested on an independent group. The models were applicable regardless of age, sex or season. The intact body mass already accounted for 90% of the protein variability. The most accurate equation combining dry body mass and interscapular fat mass explained 99% of the protein variations. Intact body mass and the kidney fat index were poor estimators of lipid stores (r2 = 0.45) but 90% of the variation was explained by an equation combining the interscapular fat mass and the hind leg length. None of the predictive equations significantly over- or underestimated body reserves. The usefulness of the models was assessed by estimating fasting endurance during winter. Individual estimates, ranging from two to eight days, did not differ by more than 0.5 day from the fasting endurance obtained from actual mobilisable body nutrients. In such lean species (adiposity 2–4%), proteins may account for up to 40% of the available energy reserves and survival is likely to be linked to the continuous availability of food resources. These results stress the need to determine proteins and not only lipids to have a pertinent tool for the management of wild animal populations, particularly in lean species.
Prevalence of neutralising antibodies to Barmah Forest, Sindbis and Trubanaman viruses in animals and humans in the south-west of Western Australia
Authors: Johansen Cheryl A. , Mackenzie John S. , Smith David W. , Lindsay Michael D. A.
Published: February 2005

A study was undertaken in the south-west of Western Australia to investigate potential vertebrate hosts of Barmah Forest virus (BFV), Sindbis virus (SINV) and Trubanaman virus (TRUV) following isolation of these viruses from mosquitoes collected during routine surveillance for arboviruses. Over 3000 animal and human sera collected between 1979 and 1995 were tested for the presence of neutralising antibodies to each of the viruses. The overall prevalence of antibodies to BFV, SINV and TRUV was 0.4%, 0.3% and 1.6%, respectively. Antibodies to BFV were detected only in quokkas (3.2%), horses (1.2%) and humans (0.9%). No definitive evidence of infection with BFV was detected in samples collected prior to 1992, supporting previous suggestions that BFV was introduced into the region after this time. Antibodies to SINV were detected in western native cats (16.7%), emus (4.5%), rabbits (0.8%) and horses (0.7%), and evidence of TRUV infection was most common in western grey kangaroos (21.1%), feral pigs (3.6%), rabbits (2.4%), foxes (2.3%), quokkas (1.6%) and horses (1.6%).
Changes in milk composition during lactation in the eastern barred bandicoot (Perameles gunnii) (Marsupialia:Peramelidae)
Authors: Ikonomopoulou M. P. , Smolenski A. P. , Rose R. W.
Published: February 2005

Perameles gunnii is a small to medium-sized omnivorous marsupial. We measured milk components from Week 4 until weaning at Week 8; these showed marked quantitative and qualitative changes. The milk produced in the early stages of lactation was dilute, ~28% solid (w/w). At four weeks carbohydrate, protein and lipids were also at low levels: 2.0 g (100 mL)–1, 4.5 g (100 mL)–1 and 3.1 g (100 mL)–1 respectively. At the mid-phase of lactation solids reached 36%, carbohydrate 5.5 g (100 mL)–1, protein 10.0 g (100 mL)–1 and lipids 8.5 g (100 mL)–1. The energy content of the milk at 4 weeks of lactation was 2.25 kJ mL–1 while at pouch vacancy it reached 8.86 kJ mL–1. At 8 weeks the pouch young was almost weaned and all the constituents but carbohydrates had increased significantly. We compared the milk components of the eastern barred bandicoot with those of other marsupial species and with the Wombaroo milk formula used by zookeepers and carers to hand-raise orphaned bandicoots. We found the milk formula to be deficient in both protein and lipid.
A bifunctional DNA repair protein from
Ferroplasma acidarmanus
exhibits
O
6
-alkylguanine-DNA alkyltransferase and endonuclease V activities
Authors: Kanugula Sreenivas , Pauly Gary T. , Moschel Robert C. , Pegg Anthony E.
Published: February 2005

A recently discovered DNA repair protein of 303 aa from the archaeal organism
Ferroplasma acidarmanus
was studied. This protein (AGTendoV) consists of a fusion of the C-terminal active site domain of
O
6
-alkylguanine-DNA alkyltransferase (AGT) with an endonuclease V domain. The AGTendoV recombinant protein expressed in
Escherichia coli
and purified to homogeneity repaired
O
6
-methylguanine lesions in DNA via alkyl transfer action despite the complete absence of the N-terminal domain and some differences in key active site residues present in known AGTs. The AGTendoV recombinant protein also cleaved DNA substrates that contained the deaminated bases uracil, hypoxanthine, or xanthine in a similar manner to
E. coli
endonuclease V. Expression of AGTendoV in
E. coli
GWR109, a strain that lacks endogenous AGT activity, protected against both the killing and mutagenic activity of
N
-methyl-
N
′-nitro-
N
-nitrosoguanidine and was more effective in preventing mutations than human alkyltransferase, suggesting that the endonuclease V activity may also repair a promutagenic lesion produced by this alkylating agent. Expression of AGTendoV in a DNA repair-deficient
E. coli nfi
-
alkA
-
strain protected from spontaneous mutations arising in saturated cultures and restored the mutation frequency to that found in the
nfi
+
alkA
+
strain. These results demonstrate the physiological occurrence of two completely different but functional DNA repair activities in a single polypeptide chain.
ErbB-3 mediates phosphoinositide 3-kinase activity in gefitinib-sensitive non-small cell lung cancer cell lines
Authors: Engelman Jeffrey A. , Jänne Pasi A. , Mermel Craig , Pearlberg Joseph , Mukohara Toru , Fleet Christina , Cichowski Karen , Johnson Bruce E. , Cantley Lewis C.
Published: February 2005

Therapies that target the EGF receptor (EGFR), such as gefitinib (IRESSA), are effective in a subset of patients with advanced non-small cell lung cancer (NSCLC). The differences in intracellular signaling networks between gefitinib-sensitive and -resistant NSCLCs remain poorly understood. In this study, we observe that gefitinib reduces phospho-Akt levels only in NSCLC cell lines in which it inhibits growth. To elucidate the mechanism underlying this observation, we compared immunoprecipitates of phosphoinositide 3-kinase (PI3K) between gefitinib-sensitive and -resistant NSCLC cell lines. We observe that PI3K associates with ErbB-3 exclusively in gefitinib-sensitive NSCLC cell lines. Gefitinib dissociates this complex, thereby linking EGFR inhibition to decreased Akt activity. In contrast, gefitinib-resistant cells do not use ErbB-3 to activate the PI3K/Akt pathway. In fact, abundant ErbB-3 expression is detected only in gefitinib-sensitive NSCLC cell lines. Two gefitinib-sensitive NSCLC cell lines with endogenous distinct activating EGFR mutations (L858R and Del747-749), frequently observed in NSCLC patients who respond to gefitinib, also use ErbB-3 to couple to PI3K. Down-regulation of ErbB-3 by means of short hairpin RNA leads to decreased phospho-Akt levels in the gefitinib-sensitive NSCLC cell lines, Calu-3 (WT EGFR) and H3255 (L858R EGFR), but has no effect on Akt activation in the gefitinib-resistant cell lines, A549 and H522. We conclude that ErbB-3 is used to couple EGFR to the PI3K/Akt pathway in gefitinib-sensitive NSCLC cell lines harboring WT and mutant EGFRs.
Loss of mitogen-activated protein kinase kinase kinase 4 (MEKK4) results in enhanced apoptosis and defective neural tube development
Authors: Chi Hongbo , Sarkisian Matthew R. , Rakic Pasko , Flavell Richard A.
Published: February 2005

Neural tube defects (NTDs) are prevalent human birth defects. Mitogen-activated protein kinases (MAPKs), such as c-Jun N-terminal kinase (JNK), are implicated in facilitating neural tube closure, yet upstream regulators remain to be identified. Here, we show that MAP kinase kinase kinase 4 (MEKK4) is strongly expressed in the developing neuroepithelium. Mice deficient in MEKK4 develop highly penetrant NTDs that cannot be rescued by supplementation with folic acid or inositol. Unlike most mouse models of NTDs, MEKK4 mutant embryos display genetically co-segregated exencephaly and spina bifida, recapitulating the phenotypes observed in human patients. To identify downstream targets of MEKK4 during neural tube development, we examined the activity of MAP kinase kinase 4 (MKK4), a signaling intermediate between MAP kinase kinase kinase and JNK/p38. We found a significant reduction in MKK4 activity in MEKK4-deficient neuroepithelium at sites of neural tube closure. MAPK pathways are key regulators of cell apoptosis and proliferation. Analyses of the neuroepithelium in MEKK4-deficient embryos showed massively elevated apoptosis before and during neural tube closure, suggesting an antiapoptotic role for MEKK4 during development. In contrast, proliferation of MEKK4-deficient neuroepithelial cells appeared to be largely unaffected. MEKK4 therefore plays a critical role in regulating MKK4 activity and apoptotic cell death during neural tube development. Disruption of this signaling pathway may be clinically relevant to folate-resistant human NTDs.
Object-oriented biological system integration: a SARS coronavirus example
Authors: Shegogue Daniel , Zheng W. Jim
Published: February 2005

Motivation

The importance of studying biology at the system level has been well recognized, yet there is no well-defined process or consistent methodology to integrate and represent biological information at this level. To overcome this hurdle, a blending of disciplines such as computer science and biology is necessary.

Results

By applying an adapted, sequential software engineering process, a complex biological system (severe acquired respiratory syndrome-coronavirus viral infection) has been reverse-engineered and represented as an object-oriented software system. The scalability of this object-oriented software engineering approach indicates that we can apply this technology for the integration of large complex biological systems.

Availability

A navigable web-based version of the system is freely available at http://people.musc.edu/~zhengw/SARS/Software-Process.htm

Contact

zhengw@musc.edu

Supplementary information

Supplemental data: Table 1 and Figures 1–16.
Reducing DUI among US college students: results of an environmental prevention trial
Authors: Clapp John D. , Johnson Mark , Voas Robert B. , Lange James E. , Shillington Audrey , Russell Cristel
Published: February 2005

Aims  Driving under the influence (DUI) of alcohol is among the most common and serious alcohol‐related problems experienced by US college students. Community‐based prevention trials using environmental approaches to DUI prevention have been effective in reducing DUI. Such interventions remain untested in college settings. This study is the first to test the efficacy of an environmental prevention campaign to reduce DUI among college students.

Design  We used a quasi‐experimental non‐equivalent comparison group design to test the efficacy of the DUI prevention intervention. Students at the experimental university were exposed to a DUI prevention intervention that included a social marketing campaign, a media advocacy campaign and increased law enforcement (DUI checkpoints and roving DUI patrols).

Setting  Students from two large public universities located along the US/Mexico border participated in the seven‐semester study.

Participants  In total, 4832 college students took part.

Measures  Using telephone interviews of randomly selected students, we took pre‐ and postintervention measures of self‐reported DUI.

Findings  Self‐reported DUI (past year) decreased significantly from pre‐test to post‐test (odds ratio = 0.55) at the intervention school, whereas rates at the comparison campus remained stable. The campus–intervention interaction was statistically significant (P < 0.05), suggesting that the campaign led to the observed change in DUI.

Conclusions  Environmental DUI campaigns similar to those validated in community prevention trials can be effective in college settings. Further research, however, is needed to determine the robustness of the changes associated with such campaigns.