The paper will give an introduction to the principle of the giant magneto resistive — GMR — effect and the silicon system integration of GMR sensors. The two main applications of a GMR are as a magnetic field strength sensor and as an angular field direction sensor. They will be discussed under consideration of automotive requirements.

In recent years, formal verification of hardware and software components has increasingly attracted interest from both academia and industry. The widespread use of automated reasoning techniques requires tools that are easy to use and support standardised protocols and data exchange formats. In [1] the first author presented the MathWeb Software Bus, a first step towards re-usable reasoning services. The MathWeb-SB had several drawbacks which limited its usability. For example, it had no service brokering capabilities and the user had to know exactly which reasoning system to use to solve a problem and how to access it.

The paper will give an introduction to the principle of the giant magneto resistive - GMR - effect and the silicon system integration of GMR sensors. The two main applications of a GMR as a magnetic field strength sensor and as an angular field direction sensor will be discussed under consideration of automotive requirements. The typical applications of a magnetic field strength GMR sensor in incremental position and speed sensing and those of GMR angular field sensors in position sensing will be summarized. Finally advantages of GMR in those applications will be discussed and conclusions on the use of GMR in automotive sensing will be drawn.

Proof planning is an application of AI planning to theorem proving that employs plan operators that encapsulate mathematical proof techniques. Many proofs require the instantiation of variables; that is, mathematical objects with certain properties have to be constructed. This is particularly difficult for automated theorem provers if the instantiations have to satisfy requirements specific for a mathematical theory, for example, for finite sets or for real numbers, because in this case unification is insufficient for finding a proper instantiation. Often, constraint solving can be employed for this task. We describe a framework for the integration of constraint solving into proof planning that combines proof planners and stand-alone constraint solvers. Proof planning has some peculiar requirements that are not met by any off-the-shelf constraint-solving system. Therefore, we extended an existing propagation-based constraint solver in a generic way. This approach generalizes previous work on tackling the problem. It provides a more principled way and employs existing AI technology.

Many applications have shown that the combination of specialized reasoning systems, such as deduction and computation systems, can lead to synergetic effects. Often, a clever combination of different reasoning systems can solve problems that are beyond the problem solving horizon of single, stand-alone systems. Current platforms for the integration of reasoning systems typically lack abstraction, robustness, and automatic coordination of reasoners. We are currently developing a new framework for reasoning agents to solve these problems. Our framework builds on the FIPA specifications for multi-agent systems, formal service descriptions, and a central brokering mechanism. In this paper we present the architecture of our framework and our progress with the integration of automated theorem provers.

This paper describes two communication for- malisms for Automated Theorem Proving (ATP) tools. First, a problem and solution language has been designed. The language will be used for writ- ing problems to be input to ATP systems, and for writing solutions output by ATP systems. Second, a hierarchy of result statuses, which adequately ex- press the range of results output by ATP systems, has been established. These formalisms will sup- port application and research in ATP, and will fa- cilitate direct communication between ATP tools when they are used as embedded components in larger systems.

Automated reasoning systems have reached a high degree of maturity in the last decade. Many reasoning tasks can be delegated to an automated theorem prover (ATP) by encoding them into its interface logic, simply calling the system and waiting for a proof, which will arrive in less than a second in most cases. Despite this seemingly ideal situation, ATPs are seldom actually used by people other than their own developers. The reasons for this seem to be that it is difficult for practitioners of other fields to find information about theorem prover software, to decide which system is best suited for the problem at hand, installing it, and coping with the often idiosyncratic concrete input syntax. Of course, not only potential outside users face these problems, so that, more often than not, existing reasoning procedures are re-implemented instead of re-used.

Reasoning systems have reached a high degree of maturity in the last decade. However, even the most successful systems are usually not general purpose problem solvers but are typically specialised on problems in a certain domain. The MathWeb Software Bus (MathWeb-SB) is a system for combining reasoning specialists via a common software bus. We describe the integration of the Clam system, a reasoning specialist for proofs by induction, into the MathWeb-SB. Due to this integration, Clam now offers its theorem proving expertise to other systems in the MathWeb-SB. On the other hand, Clam can use the services of any reasoning specialist already integrated. We focus on the latter and describe first experiments on proving theorems by induction using the computational power of the Maple system within Clam.

The Ωmega proof development system [2] is the core of several related and well integrated research projects of the Ωmega research group.

1 Abstract Today's interactive mathematics textbooks use a collection of predefined documents, typically organized as a network of pages. This makes a reuse and a sound re-combination of the encoded knowledge impossible and inhibits a radical adaption of course presentation and content to the user's needs. In order to avoid these drawbacks we have designed a web-based framework for dynamically producing interactive documents for learning mathematics called ID. The system design relies on the separation of knowledge representation from system functionalities. Salient features of our system are the individual generation of interactive documents based on general domain knowledge, user-specific preferences and the user's knowledge as well as the integration of external problem solving systems. The paper describes the distributed web-based architecture of our system and the principles of its components.

A somatic cell hybrid panel was constructed consisting of seven hybrids with translocation breakpoints spanning the region 17q23-->q25. Hybrid clones carrying the longarm derivative of chromosome 17 in the absence of the normal chromosome 17 and of the derivative 17 were initially identified by PCR typing for a proximal and distal 17q marker. The translocation breakpoints of the hybrids were then mapped in more detail by PCR analysis for a number of microsatellite markers from chromosome 17q as well as for five gene loci (CACNLG, GH1, SOX9, TIMP2, TK1) previously mapped to the region 17q23-->q25. In addition, the locus for GDIA1 was mapped by FISH to 17q25.3 and fine mapped with the help of the hybrid panel. These seven new hybrids complement the existing somatic cell hybrid panel for the long arm of chromosome 17q.

A human autosomal XY sex reversal locus, SRA1, associated with the skeletal malformation syndrome campomelic dysplasia (CMPD1), has been placed at distal 17q. The SOX9 gene, a positional candidate from the chromosomal location and expression pattern reported for mouse Sox9, was isolated and characterized. SOX9 encodes a putative transcription factor structurally related to the testis-determining factor SRY and is expressed in many adult tissues, and in fetal testis and skeletal tissue. Inactivating mutations on one SOX9 allele identified in nontranslocation CMPD1-SRA1 cases point to haploinsufficiency for SOX9 as the cause for both campomelic dysplasia and autosomal XY sex reversal. The 17q breakpoints in three CMPD1 translocation cases map 50 kb or more from SOX9.

Cells of an euploid strain of the Chinese hamster synchronized in the G1 phase were microirradiated in the nucleus with a laser UV microbeam (λ = 257 nm) and pulse-labelled with [3H]thymidine. In autoradiographs of cells fixed immediately after the pulse unscheduled DNA synthesis (UDS) was found restricted to the microirradiated part of the nucleus. The rate of UDS varied with the UV energy applied and the post-irradiation incubation time. In other experiments chromosome preparations were established after an additional chase and a subsequent growth period. In 28 mitotic cells autoradiographic label was found concentrated on a few chromosomes which lay adjacent to each other in one part of the metaphase plate. The distribution of label on the chromosomes could clearly be distinguished from patterns which originate from semi-conservative DNA synthesis within S phase. The label on chromosomes of microirradiated cells thus represents UDS. Our findings support the following ideas on the arrangement of interphase chromosomes: (1) Decondensed interphase chromosomes may occupy rather compact territories. (2) Chromosomes do not necessarily exhibit a close and permanent association with their respective homologues.

In the last few decades a large variety of mathematical reasoning tools, such as computer algebra systems, automated and interactive theorem provers, decision procedures, etc. have been developed and reached considerable strength. It has become clear that no single system is capable of providing all types of mathemat- ical services, and that systems have to be combined for ambitious mathematical applications. Unfortunately, many mathematical reasoning systems use proprietary input and output formats, and the output in these system-specific formats is of- ten incomprehensible to other components and human users. Transformation tools and data-exchange formats are necessary in order to combine systems and to grant common access to mathematical content. This paper describes the integration of several proof transformation tools in a Java agent architecture, their description in a mathematical service description language, and their combination via a brokering mechanism. The applicability of the approach is demonstrated with an example from group theory.

This paper describes two communication formalisms for Automated Theorem Proving (ATP) tools. First, a problem and solution language has been designed. The language will be used for writing problems to be input to ATP systems, and for writing solutions output by ATP systems. Second, a hierarchy of result statuses, which adequately express the range of results output by ATP systems, has been established. These formalisms will support application and research in ATP, and will facilitate direct communication between ATP tools when they are used as embedded components in larger systems.