Search

Capturing and understanding mathematics from print form is an important task in translating written mathematical knowledge into electronic form. While the problem of syntactically recognising mathematical formulas from scanned images has received attention, very little work has been done on semantic validation and correction of recognised formulas. We present a first step towards such an integrated system by combining the Infty system with a semantic analyser for matrix expressions. We applied the combined system in experiments on the semantic analysis of matrix images scanned from textbooks. While the first results are encouraging, they also demonstrate many ambiguities one has to deal with when analysing matrix expressions in different contexts. We give a detailed overview of the problems we encountered that motivate further research into semantic validation of mathematical formula recognition. [ABSTRACT FROM AUTHOR]

Mathematical notation is a structured, open, and ambiguous language. In order to support mathematical notation in MKM applications one must necessarily take into account presentational as well as semantic aspects. The former are required to create a familiar, comfortable, and usable interface to interact with. The latter are necessary in order to process the information meaningfully. In this paper we investigate a framework for dealing with mathematical notation in a meaningful, extensible way, and we show an effective instantiation of its architecture to the field of interactive theorem proving. The framework builds upon well-known concepts and widely-used technologies and it can be easily adopted by other MKM applications. [ABSTRACT FROM AUTHOR]

Within the LeActiveMath project, a collection of OMDoc files and supporting material has been realized. This content covers the derivative side of calculus and is being used by students in the LeActiveMath learning environment. LeAM-calculus is the first collection trying to make use of most of the features of the learning environment including advanced usages of OpenMath and OMDoc. It has been written in OQMath, a readable xml-syntax. This paper describes the tools to produce it, how they were used and combined, the resulting content and the experience gained. It argues that the declaration of new OpenMath symbols is a requirement and explains challenges of authoring semantic mathematical content. Finally, it presents the management activities to support the authoring process. [ABSTRACT FROM AUTHOR]

In this paper, we address the problem of automatic keywords assignment to scientific publications. The idea to use textual traces learned from training data in a supervised manner to identify appropriate keywords is considered. We introduce the transparent concept of identification cloud as a means to represent the semantics of scientific terms. This concept is mathematically defined by models of scientific terms stochastic distributions over publication texts. Characteristics of models as well as procedures for both non-parametric and parametric estimation of probability distributions are presented. [ABSTRACT FROM AUTHOR]

In this paper we investigate how to extract proof procedural information contained in declarative representations of mathematical knowledge, such as axioms, definitions, lemmas and theorems (collectively called assertions) and how to effectively include it into automated proof search techniques. In the context of the proof planner Multi and the agent-based reasoning system Ω-Ants, we present techniques to automatically synthesize proof planning methods and Ω-Ants-agents from assertions such that they can be actively used by these systems. This in turn enables a user to effectively use these systems without having to know the peculiarities of coding methods and agents. [ABSTRACT FROM AUTHOR]

Math-aware fine-grain search is expected to be widely available. A key question is what roles it can play in mathematics. It will be argued that, besides finding information, math search can help advance and manage mathematical knowledge. This paper will present the short-term goals and state of the art of math-aware fine-grain search. Afterwards, it will focus on how math search can help advance and manage mathematical knowledge, and discuss what needs to be done to fulfill those roles, emphasizing two key components. The first is similarity search, and how it applies to (1) discovering and drawing upon connections between different fields, and (2) proof development. The second is math metadata, which math search will surely encourage and benefit from, and which will be pivotal to mathematical knowledge management. [ABSTRACT FROM AUTHOR]

"The Strong Law of Small Numbers" is the provocative title of an unpublished paper by Richard Kenneth Guy, a mathematician at the University of Calgary. For many years Guy has edited the "Research Problems" department of The American Mathematical Monthly. He is the author of numerous technical papers and is coauthor with John Horton Conway and Elwyn R. Berlekamp of Winning Ways, a two-volume work about new mathematical recreations. The material that follows is taken almost entirely from Guy's paper. [ABSTRACT FROM AUTHOR]

This paper presents the research that is being undertaken by the Transport Infrastructure and Systems Group of CESUR — IST, under the author's leadership. There are three main research streams: Modelling and innovation in urban mobility management; Organization and technology as instruments for efficiency gains in large scale transport systems; and, Quality and safety of transport infrastructure. Most of this research is developed through PhD dissertations. This paper briefly provides the main motivation, methodology and expected results of the different research studies, as well as the labs and international networks that underpin this research effort. [ABSTRACT FROM AUTHOR]

The research and development portfolio of the metal forming group of Instituto Superior Técnico is driven by fundamental topics in the field of computer simulation and by the needs of manufacturing industries. The group was formed in the late 70's and conducts activities in bulk forming, sheet forming, tube forming and powder forming. The purpose of this paper is to provide a brief overview of the activities of the metal forming group. The paper is organized around a number of examples that are representative of the activities of the group in the fields of numerical and experimental simulation of forming processes and of technology development and transfer into industrial companies. In what concerns numerical and experimental simulation the paper includes three-dimensional numerical modelling of the closed-die forging of spiders by means of the finite element flow formulation and modelling of the backward extrusion process by means of state-of-the-art meshless approaches. Collaboration with the industry is illustrated by means of selected joint partnerships with the Portuguese Mint House and with an industrial company producing intercoolers for automotives. [ABSTRACT FROM AUTHOR]

Multimedia information has been conquering a central role in our society in recent years. For multimedia services and applications to be possible, multimedia information has to be efficiently and effectively represented. This paper addresses three challenges in this area: coding, description and adaptation. In order for multimedia information to be used, it is essential that it is coded not only in an efficient way but also in an error resilient way due to the growing importance of error prone channels such as mobile networks; moreover it must allow random access, provide interactive capabilities, low complexity implementation, etc. Also the huge amount of multimedia information available requires efficient management in terms of identification, filtering and retrieval. Information that cannot be found is the same as information that does not exist. This capability asks for powerful ways to describe multimedia information, this means to create data about the data which allows to identify, filter and retrieve the data, making the data more useful for the simple fact that it can be effectively found when there is a need. Finally, the increasing heterogeneity of the multimedia consumption conditions in terms of networks, terminal, environments and users, is asking for content to be adequately adapted and customized in order the users get the best possible multimedia experience for the conditions in place. This paper describes research work developed at the Image Group of Instituto de Telecomunicações at Instituto Superior Técnico in the areas of the three main challenges above identified: coding, description and adaptation. [ABSTRACT FROM AUTHOR]

Biotechnology methods provided a huge breakthrough in the knowledge of reproduction and development processes in mammals and opened new windows of opportunity for innovative enterprises in reproductive technologies in livestock and, in the pharmaceutical and biotechnological industries. In this paper we review our recent methodological and scientific developments and their integration in private commercially oriented enterprises. The first part of the paper contains examples on reproductive technologies (semen cryopreservation in the national equine breed, the Lusitano, and embryo transfer in dairy cattle) and the second part includes developmental biology studies on gene expression and genetic manipulation of the laboratory mouse and their prospects in the biotechnology industry [ABSTRACT FROM AUTHOR]

To be effective and useful, math search systems must not only maximize precision and recall, but also present the query hits in a form that makes it easy for the user to identify quickly the truly relevant hits. To meet that requirement, the search system must sort the hits according to domain-appropriate relevance criteria, and provide with each hit a query-relevant summary of the hit target. The standard relevance measures in text search, which rely mostly on keyword frequencies and document sizes, turned out to be inadequate in math search. Therefore, alternative relevance measures must be defined, which give more weight to certain types of information than to others and take into account cross-reference statistics. In this paper, new, multidimensional relevance metrics are defined for math search, methods for computing and implementing them are discussed, and comparative performance evaluation results are presented. Query-relevant hit-summary generation is another factor that enables users to quickly determine the relevance of the presented hits. Although the hit title accompanied by a few leading sentences from the target document is simple to produce, this often fails to convey to the user the document's relevant excerpts. This shifts the burden onto the user to pursue many of the hits, and read significant portions of their target documents, to finally locate the wanted documents. Clearly, this task is too time-consuming and should be largely automated. This paper presents query-relevant hit-summary generation methods, outlines implementation strategies, and presents performance evaluation results. [ABSTRACT FROM AUTHOR]

Logiweb is an open source, distributed system for publication of machine checked mathematics. It covers all aspects of electronic publishing: high typographical quality, archival, handling of references to previously published results, and publication of refereed volumes. The present paper is itself produced using Logiweb; and the paper is formally correct in the sense that it has been verified by Logiweb. The paper describes the implementation layers of the Logiweb system as seen by the user: the programming layer, the metalogic layer, the tactic layer, and the object proof layer. [ABSTRACT FROM AUTHOR]

From the very beginning of the development of the Mizar system experiments with using Mizar as a tool for teaching mathematics have been conducted. Numerous organized courses were based on different versions of the system: starting from the first implementation of its processor, through Mizar-MSE, Mizar-4 and PC-Mizar up till its present version. Now Mizar with its mathematical library gives us quite new didactic possibilities. The purpose of this paper is to present a certain course on logic and set theory offered by our Institute for freshman students. The course employs Mizar as the main tool of instruction. In the paper we discuss the organization of this course and describe some examples of students' tasks. Finally, some conclusions and remarks are given. [ABSTRACT FROM AUTHOR]

In previous papers we described the implementation of a system which combines mathematical object generation, transformation and filtering, conjecture generation, proving and disproving for mathematical discovery in non-associative algebra. While the system has generated novel, fully verified theorems, their construction involved a lot of ad hoc communication between disparate systems. In this paper we carefully reconstruct a specification of a sub-process of the original system in a framework for trustable communication between mathematics systems put forth by us. It employs the concept of biform theories that enables the combined formalisation of the axiomatic and algorithmic theories behind the generation process. This allows us to gain a much better understanding of the original system, and exposes clear generalisation opportunities. [ABSTRACT FROM AUTHOR]

Many processes in mathematical computing try to use knowledge of the most desired forms of mathematical expressions. This occurs, for example, in symbolic computation systems, when expressions are simplified, or mathematical document recognition, when formula layout is analyzed. The decision about which forms are the most desired, however, has typically been left to the guess-work or prejudices of a small number of system designers. This paper observes that, on a domain by domain basis, certain expressions are actually used much more frequently than others. On the hypothesis that actual usage is the best measure of desirability, this papers begins to quantify empirically the use of common expressions in the mathematical literature. We analyze all 20,000 mathematical documents from the mathematical arXiv server from 2000-2004, the period corresponding to the new mathematical subject classification. We report on the process by which these documents are analyzed, through conversion to MathML, and present first empirical results on the most common aspects of mathematical expressions by subject classification. We use the notion of a weighted dictionary to record the relative frequency of subexpressions, and explore how this information may be used for further processes, including deriving common patterns of expressions and probability measures for symbol sequences. [ABSTRACT FROM AUTHOR]

OpenMath is a widely recognised approach to the semantic markup of mathematics that is often used for communication between OpenMath compliant systems. The Aldor language has a sophisticated category-based type system that was specifically developed for the purpose of modelling mathematical structures, while the system itself supports the creation of small-footprint applications suitable for deployment as web services. In this paper we present our first results of how one may perform translations from generic OpenMath objects into values in specific Aldor domains, describing how the Aldor interface domain ExpressionTree is used to achieve this. We outline our Aldor implementation of an OpenMath translator, and describe an efficient extension of this to the Parser category. In addition, the Aldor service creation and invocation mechanism are explained. Thus we are in a position to develop and deploy mathematical web services whose descriptions may be directly derived from Aldor's rich type language. [ABSTRACT FROM AUTHOR]

Much work in MKM depends on the application of formal logic to mathematics. However, much mathematical knowledge is informal. Luckily, formal logic only represents one tradition in logic, specifically the modeling of inference in terms of logical form. Many inferences cannot be captured in this manner. The study of such inferences is still within the domain of logic, and is sometimes called informal logic. This paper explores some of the benefits informal logic may have for the management of informal mathematical knowledge. [ABSTRACT FROM AUTHOR]

For the transfer of mathematical knowledge from paper to electronic form, the reliable automatic analysis and understanding of mathematical texts is crucial. A robust system for this task needs to combine low level character recognition with higher level structural analysis of mathematical formulas. We present progress towards this goal by extending a database-driven optical character recognition system for mathematics with two high level analysis features. One extends and enhances the traditional approach of projection profile cutting. The second aims at integrating the recognition process with graph grammar rewriting by giving support to the interactive construction and validation of grammar rules. Both approaches can be successfully employed to enhance the capabilities of our system to recognise and reconstruct compound mathematical expressions. [ABSTRACT FROM AUTHOR]

Cut-elimination is the most prominent form of proof transformation in logic. The elimination of cuts in formal proofs corresponds to the removal of intermediate statements (lemmas) in mathematical proofs. The cut-elimination method CERES (cut-elimination by resolution) works by constructing a set of clauses from a proof with cuts. Any resolution refutation of this set then serves as a skeleton of an LK-proof with only atomic cuts. In this paper we present an extension of CERES to a calculus LKDe which is stronger than the Gentzen calculus LK (it contains rules for introduction of definitions and equality rules). This extension makes it much easier to formalize mathematical proofs and increases the performance of the cut-elimination method. The system CERES already proved efficient in handling very large proofs. [ABSTRACT FROM AUTHOR]

The Borsuk-Ulam theorem is one of the most useful tools offered by elementary algebraic topology to the outside world. Here are four reasons why this is such a great theorem: There are (1) several different equivalent versions, (2) many different proofs, (3) a host of extensions and generalizations, and (4) numerous interesting applications. As for (1), Borsuk's original paper [Bor33] already gives three variants. Below we state six different but equivalent versions, all of them very useful, and several more are given in the exercises. [ABSTRACT FROM AUTHOR]

A (q,m,k) cover of V(k,q), the vector space of k-tuples over GF(q), is a subset of the non-zero vectors of V(k,q) which has rank k and has non-empty intersection with every subspace of V(k,q) of rank k−m. A (q,m,k) cover may also be viewed as a matroid. As such it is essentially the image in V(k,q) of a restriction M of PG(k−1,q) under some representation, where M has rank k and critical exponent greater than m. An earlier paper answered several questions of Mullin and Stanton concerning (2,m,k) covers. This paper answers the corresponding questions for (q,m,k) covers when q>2. In particular, the least number η(q,m,k) of elements in a (q,m,k) cover is determined and those matroids having exactly η(q,m,k) elements are characterized. [ABSTRACT FROM AUTHOR]

This paper discusses a combination of factors that fuelled the BSE crisis in Portugal and highlights the relevant changes that the BSE epidemic compelled in the beef chain and products of bovine origin. An emphasis is made on the dilemma of communicating out of a food safety crisis. [ABSTRACT FROM AUTHOR]

In this paper, an overview on the development and application of state of the art integrated water modelling tools to study water pollution, either from urban or agricultural origin, from source to final destination, and also of the research carried out at IST in the framework of integrated water management is described. The modelling tools are used for computing the urban load in a sub-catchment of Lisbon metropolitan area for assessing the trophic levels of Tagus estuary and its relation with urban and agricultural loads. The strategy for modelling development at IST is also described, showing that modelling can be an important contribution for the integration of water management. Results have shown that modelling of the functioning of wastewater treatment plants is a mechanism for managing the urban wastewater loads and that the trophic level in the Tagus estuary is controlled by light penetration and not by nutrients. As a consequence, a reduction of the nutrient loads from urban origin or a 50% of the agricultural nutrient load would have no benefits in terms of trophic activity. [ABSTRACT FROM AUTHOR]

Most of the industrial production processes were developed in the 50s at the time of cheap and abundant raw materials, energy and water resources. The intensive use of water of good quality and the search for new processes/products aiming maximal profits led to scarcity and degradation of natural resources. Reducing material waste is one of the greatest challenges facing industry today. Because water is one of the industry's major waste products, the ability to reduce waste water would be a giant step in the direction of overall waste reduction. Water conservation and water use were considered justifiable only if they represented economic savings either in material recovering or in the avoidance of treatment costs. However, today's industrial facilities are constantly striving to operate more efficiently, and the most successful plans are relentless in their search for the following: higher product yields; beneficial use of by-products; improved energy efficiency; safer and more reliable operations; improved public image; reduced environmental impacts. This paper provides a systematic approach with four outstanding examples from diverse industries: Corrugated board; Dairy; Coke and Cork. The authors have combined the use of proven and accepted technologies and practices with some new emergent technologies developing a new systematic approach for minimizing net water usage at industrial facilities, presented it in a straight forward manner. [ABSTRACT FROM AUTHOR]

The present Portuguese forests resulted from reforestation in the context of socio-economic changes in rural areas, which have been occurring since middle of the 20th century. Hence, some of its vulnerabilities are related to the lack of tradition in the management of forests in a country where agriculture was the dominant activity until recently. In addition to the vulnerabilities resulting from inadequate management forests are facing today, as well as in the future, changes in the environment (climate) and in potentially harmful biotic invasions - e.g. pests and diseases - must be taken into account. Simultaneously, global markets change as well as the impact of agricultural and rural development policies on forestry. In spite of these constraints, it is a relevant sector for the national economy that claims for research results to support policies and management planning concerning its sustainability. This paper describes the national forest sector in its economic, social and environmental facets. Based on current research, we discuss some of the impacts of climate change scenarios and the new forest management paradigms on the forests of the future in the Portuguese continental territory.. [ABSTRACT FROM AUTHOR]

Industrial ecology is a broad framework for thinking and acting in the realm of sustainability. The name suggests, metaphorically, the blending of ecological systems and industrial economies. The ecological side offers possibilities to learn from observing resilient, robust, long-lived ecological communities as examples of sustainable systems. The industrial side suggests that society can move towards sustainable economies by embedding the principles learned from ecological systems to the design of firms and larger social institutions. Industrial Ecology promotes a holistic view of engineering systems where the system under analysis must be viewed in a global context. This framework is quite challenging and requires the development of a set of tools to bridge different scales, from site or product specific analysis to the whole economy diagnostic and from the economic to the socio-environmental dimension, thus resulting in a multi-disciplinary set of analytical tools. Providing an adequate framework for this "Industrial Ecology Toolbox" and putting it at the service of the promotion of sustainable development is the major objective of the R&D reported in this paper. R&D at IST-UTL on the development and application of different tools aimed at providing a coherent framework for this "Industrial ecology toolbox" is revised and its contribution to the promotion of sustainable development policies and practices in the socioeconomic arena is demonstrated with specific case-studies. The tools analyzed range from macroeconomic techniques to specific environmental analysis tools, and it was shown how other tools could be developed and used to promote the interaction between economic and environmental analysis within macro and micro-scales, thus enabling the design of more sustainable systems of different complexity levels. [ABSTRACT FROM AUTHOR]

Energy is central to achieving sustainable social and economic development. As a matter of fact, it is not possible to achieve economic growth to satisfy current basic needs of Humanity without an intensive use of energy. On the other side, one of the main challenges for the use of energy in the negative effects of greenhouse gases on the global climates. Europe needs a greater security of supply and to achieve this goal it is necessary to competitive markets and efficient regulations. It also necessary to diversify energy mix and renewable energy sources could contribute to this objective. This paper presents the work performed by the Research Group on Energy and Sustainable Development of the Instituto Superior Técnico of the Technical University of Lisbon on new and renewable energy sources for sustainable development. [ABSTRACT FROM AUTHOR]

Fifty year have passed since Solow's [21] paper on economic growth theory has been published. With a non-specialized reader in mind, we present the main ensuing phases of the theory and the way our own research relates to it. The history of growth theory is conventionally divided into two phases: until early 1970's, the research is labeled exogenous growth theory, and, starting in late 1980's until the present, the new growth or endogenous growth theory is being developed. We present the main models of both theories, the stylized facts of growth and a broad view on their compliance of theory with them. At last, we report some avenues that we have been exploring, as well as their motivation and results. This research addresses the topics: existence of multiple BGP's, indeterminacy, non-monotonous transitions and an exploration on the integration of spatial and growth theories using PDE's. [ABSTRACT FROM AUTHOR]

In recent years there has been growing evidence of a renewal of the Chinese interest in Africa, not for ideological reasons, as in the past, but rather due to economic motivations. In this new framework, African Portuguese speaking countries (Angola, Mozambique, Guinea-Bissau and Cape Verde) are interesting case studies. This paper argues that the PRC foreign policy to Africa has substituted the ideological approach by an economic one, exporting to the third world its development model. In the particular case of African Portuguese speaking countries, China strategy takes advantage of a common denominator between those countries and a Chinese territory that was formerly under Portuguese administration: Macau.. [ABSTRACT FROM AUTHOR]

This paper analyses different public policies in the regulation area that may be applied to competition as a reality that criss-crosses the whole of Portuguese economy. It also approaches, from the same optic but with a different focalization, the issue of concentration in the media sector, as an economic and sociological reality of growing, unambiguous importance in our present world. It is concluded that the State should proceed with effective regulation policies that may handle market failures without, however, generating State failures. [ABSTRACT FROM AUTHOR]

Experimental investigations over many years reveal that blood flow exhibits non-Newtonian characteristics such as shear-thinning, viscoelasticity and thixotropic behaviour. The complex rheology of blood is influenced by numerous factors including plasma viscosity, rate of shear, hematocrit, level of erythrocytes aggregation and deformability. Hemodynamic analysis of blood flow in vascular beds and prosthetic devices requires the rheological behaviour of blood to be characterized through appropriate constitutive equations relating the stress to deformation and rate of deformation. The objective of this paper is to present a short overview of some macroscopic constitutive models that can mathematically characterize the rheology of blood and describe its known phenomenological properties. Some numerical simulations obtained in geometrically reconstructed real vessels will be also presented to illustrate the hemodynamic behaviour using Newtonian and non-Newtonian inelastic models under a given set of physiological flow conditions. [ABSTRACT FROM AUTHOR]

In this paper we illustrate the interplay between Mathematics and Finance, pointing out the relevance of stochastic calculus and mathematical modelling in some important aspects of modern finance. We present two types of mathematical models: the binomial asset pricing model and continuous-time models. We point out some sensitive points of research. [ABSTRACT FROM AUTHOR]

We explore mathematical knowledge in the field of electrical engineering and claim that electrical engineering is a suitable area of application for mathematical knowledge management: We show that mathematical knowledge arising in electrical engineering can be successfully handled by existing MKM systems, namely by the Mizar system. To this end we consider in this paper network theory and in particular stability of networks. As an example for mathematical knowledge in electrical engineering we present a Mizar formalization of Schur's theorem. Schur's theorem provides a recursive, easy method to check for BIBO-stability of networks. [ABSTRACT FROM AUTHOR]

Even though only a tiny fraction of mathematical knowledge is available digitally (e.g in theorem prover or computer algebra libraries, in documents with content-markup), our current retrieval methods are already inadequate. With further increase in digitalization of mathematics the situation will get worse without significant advances. When searching a formula, we often want to find not only structurally identical occurrences, but also all (logically) equivalent ones. Furthermore, we want to retrieve whole mathematical theories (i.e. objects with prescribed properties), and we want to find them irrespective of the nomenclature chosen in the respective formalization. In this paper, we propose a normalization-based approach to mathematical formula and theory retrieval modulo an equivalence theory and concept renaming, and apply the proposed algorithm to end-user querying and knowledge sharing. We test the implementation by applying it to a first-order translation of the Mizar library. [ABSTRACT FROM AUTHOR]

The interest of the field of Mathematical Knowledge Management is predicated on the assumption that by investing into markup or formalization of mathematical knowledge, we can reap benefits in managing (creating, classifying, reusing, verifying, and finding) mathematical theories, statements, and objects. This global value proposition has been used to motivate the pursuit of technologies that can add machine support to these knowledge management tasks. But this (rather naive) technology-centered motivation takes a view merely from the global (macro) perspective, and almost totally disregards the user's point of view and motivations for using it, the local (micro) perspective. In this paper we go a first step into a more principled analysis of the MKM value proposition by focusing on motivations for mathematical search engines from the micro perspective. We will use a table-based method called the "Added-Value Analysis" (AVA) developed by one of the authors. Even though we apply the AVA only to mathematical search engines, the method quickly leads to value considerations that are relevant for the whole field of MKM. [ABSTRACT FROM AUTHOR]

There are many styles for the narrative structure of a mathematical document. Each mathematician has its own conventions and traditions about labeling portions of texts (e.g., chapter, section, theorem or proof ) and identifying statements according to their logical importance (e.g., theorem is more important than lemma). Such narrative/structuring labels guide the reader's navigation of the text and form the key components in the reasoning structure of the theory reflected in the text. We present in this paper a method to computerise the narrative structure of a text which includes the relationships between labeled text entities. These labels and relations are input by the user on top of their natural language text. This narrative structure is then automatically analysed to check its consistency. This automatic analysis consists of two phases: (1) checking the correct usage of labels and relations (i.e., that a "proof" justifies a "theorem" but cannot justify an "axiom") and (2) checking that the logical precedences in the document are self-consistent. The development of this method was driven by the experience of computerising a number of mathematical documents (covering different authoring styles). We illustrate how such computerised narrative structure could be used for further manipulations, i.e. to build a skeleton of a formal document in a formal system like Mizar, Coq or Isabelle. [ABSTRACT FROM AUTHOR]

One major goal of Mathematical Knowledge Management is building extensive repositories, in which the mathematical knowledge has been verified. It appears, however, that maintaining such a repository is as hard as building it - especially for an open collection with a large number of contributors. In this paper we argue that even careful reviewing of contributions cannot cope with the task of keeping a mathematical repository efficient and clearly arranged in the long term. We discuss reasons for revisions of mathematical repositories accomplished by the "core implementors" and illustrate our experiences with revisions of MML, the Mizar Mathematical Library. [ABSTRACT FROM AUTHOR]

This paper introduces Proof General Kit, a framework for software components tailored to interactive proof development. The goal of the framework is to enable flexible environments for managing formal proofs across their life-cycle: creation, maintenance and exploitation. The framework connects together different kinds of component, exchanging messages using a common communication infrastructure and protocol called PGIP. The main channel connects provers to displays. Provers are the back-end interactive proof engines and displays are components for interacting with the user, allowing browsing or editing of proofs. At the core of the framework is a broker middleware component which manages proof-in-progress and mediates between components. [ABSTRACT FROM AUTHOR]

In this paper we address the problem of reconstructing a higher order, checkable proof object starting from a proof trace left by a first order automatic proof searching procedure, in a restricted equational framework. The automatic procedure is based on superposition rules for the unit equality case. Proof transformation techniques aimed to improve the readability of the final proof are discussed. [ABSTRACT FROM AUTHOR]

We address the problem of automatic synthesis of decision procedures. Our synthesis mechanism consists of several stages and sub-mechanisms and is well-suited to the proof-planning paradigm. The system (adeptus), that we present in this paper, synthesised a decision procedure for ground arithmetic completely automatically and it used some specific method generators in generating a decision procedure for linear arithmetic, in only a few seconds of cpu time. We believe that this approach can lead to automated assistance in constructing decision procedures and to more reliable implementations of decision procedures. [ABSTRACT FROM AUTHOR]

This paper looks at the feasibility of applying the quantifier elimination program QEPCAD-B to obtain quantifier-free conditions for the approximate factorization of a simple hyperbolic linear partial differential operator (LPDO) of order 2 over some given bounded rectangular domain in the plane. A condition for approximate factorization of such an operator to within some given tolerance over some given bounded rectangular domain is first stated as a quantified formula of elementary real algebra. Then QEPCAD-B is applied to try to eliminate the quantifiers from the formula. While QEPCAD-B required too much space and time to finish its task, it was able to find a partial solution to the problem. That is, it was able to find a nontrivial quantifier-free sufficient condition for the original quantified formula. [ABSTRACT FROM AUTHOR]

An axiomatic theory represents mathematical knowledge declaratively as a set of axioms. An algorithmic theory represents mathematical knowledge procedurally as a set of algorithms. A biform theory is simultaneously an axiomatic theory and an algorithmic theory. It represents mathematical knowledge both declaratively and procedurally. Since the algorithms of algorithmic theories manipulate the syntax of expressions, biform theories—as well as algorithmic theories—are difficult to formalize in a traditional logic without the means to reason about syntax. Chiron is a derivative of von-Neumann-Bernays-Gödel (nbg) set theory that is intended to be a practical, general-purpose logic for mechanizing mathematics. It includes elements of type theory, a scheme for handling undefinedness, and a facility for reasoning about the syntax of expressions. It is an exceptionally well-suited logic for formalizing biform theories. This paper defines the notion of a biform theory, gives an overview of Chiron, and illustrates how biform theories can be formalized in Chiron. [ABSTRACT FROM AUTHOR]

This paper reports on ongoing work on the project of representing the Kenzo system [15] in type theory [11]. [ABSTRACT FROM AUTHOR]

In this paper, an approach to integrate an already-written Common Lisp program for algebraic manipulation with ACL2 proofs of properties of that program is presented. We report on a particular property called "cancellation theorem", which has been proved in ACL2, and could be applied to several problems in the field of Computational Algebraic Topology. [ABSTRACT FROM AUTHOR]

A variety of problems in mathematical calculus can be solved by recursively applying a finite number of rules. Often, a generic solving strategy can be extracted and an interactive exercise system that emulates a tutor can be implemented. In this paper we show how software developed by us can be used to realize this interactivity. In particular, an implementation of a generic exercise for computing the derivative of elementary functions is presented. [ABSTRACT FROM AUTHOR]

We describe a case-study of the application of web- technology () to create web-based didactic material out of a repository of formal mathematics (), using the structure of an existing course (). The paper discusses the difficulties related to associating notation to a formula, the embedding of formal notions into a document (the "view"), and the rendering of proofs. [ABSTRACT FROM AUTHOR]

Due to their rapidly increasing amount, maintaining mathematical documents more and more becomes an engineering task. In this paper, we combine the projects : Multimedia in Safe and Secure Systems - see www.mmiss.de and .: The Consistent Document Engineering Toolkit - see www.unibw.de/inf2/ CDET That way, we achieve major benefits for mathematical knowledge management: (1) Semantic annotations relate mathematical constructs. This reaches beyond mathematics and thus fosters integration of mathematical content into a broader context. (2) Fine-grained version control enables change management and configuration management. (3) Semi-formal consistency management identifies violations of user-defined consistency requirements and proposes how they can be best resolved. [ABSTRACT FROM AUTHOR]

The -calculus, introduced by Curien and Herbelin, is a calculus isomorphic to (a variant of) the classical sequent calculus LK of Gentzen. As a proof format it has very remarkable properties that we plan to study in future works. In this paper we embed it with a rendering semantics that provides explanations in pseudo-natural language of its proof terms, in the spirit of the work of Yann Coscoy [3] for the λ-calculus. The rendering semantics unveils the richness of the calculus that allows to preserve several proof structures that are identified when encoded in the λ-calculus. [ABSTRACT FROM AUTHOR]

Computerizing mathematical texts to allow software access to some or all of the texts' semantic content is a long and tedious process that currently requires much expertise. We believe it is useful to support computerization that adds some structural and semantic information, but does not require jumping directly from the word-processing level (e.g., ) to full formalization (e.g., , , etc.). Although some existing mathematical languages are aimed at this middle ground (e.g., , , ), we believe they miss features needed to capture some important aspects of mathematical texts, especially the portion written with natural language. For this reason, we have been developing , a language for representing mathematical texts that has weak type checking and support for the special mathematical use of natural language. is currently aimed at only capturing the essential grammatical and binding structure of mathematical text without requiring full formalization. The development of is directly driven by experience encoding real mathematical texts. Based on this experience, this paper presents the changes that yield our latest version of . We have restructured and simplified the core of the language, replaced our old notion of "context" by a new system of blocks and local scoping, and made other changes. Furthermore, we have enhanced our support for the mathematical use of nouns and adjectives with object-oriented features so that nouns now correspond to classes, and adjectives to mixins. [ABSTRACT FROM AUTHOR]