Search

In recent years, large corpora of formally expressed knowledge have become available in the fields of formal mathematics, software verification, and real-world ontologies. The Learning2Reason project aims to develop novel machine learning methods for computer-assisted reasoning on such corpora. Our global research goals are to provide good methods for selecting relevant knowledge from large formal knowledge bases, and to combine them with automated reasoning methods.

We have examined polycrystalline MgB2 by electron energy loss spectroscopy (EELS) and density of state calculations. In particular, we have studied two different crystal orientations, [110] and [001] with respect to the incident electron beam direction, and found significant changes in the near-edge fine-structure of the B K-edge. Density functional theory suggests that the pre-peak of the B K-edge core loss is composed of a mixture of pxy and pz hole states and we will show that these contributions can be distinguished only with an experimental energy resolution better than 0.5 eV. For conventional TEM/STEM instruments with an energy resolution of ~1.0 eV the pre-peak still contains valuable information about the local charge carrier concentration that can be probed by core-loss EELS. By considering the scattering momentum transfer for different crystal orientations, it is possible to analytically separate pxy and pz components from of the experimental spectra With careful experiments and analysis, EELS can be a unique tool measuring the superconducting properties of MgB2, doped with various elements for improved transport properties on a sub-nanometer scale., Comment: 26 Pages, 5 figures, 1 table. Submited to PRB

We recently started the Formalin project to create a formal version of the C99 standard for the C programming language. We are writing three matching formalizations for the interactive theorem provers HOL4, Isabelle/HOL and Coq, that all closely follow the existing C99 standard text. The project runs from 2011 to 2015, and involves a full time PhD student, a half time researcher and several scientific advisors. The project differs from existing work in that our aim is to formalize the full C99 standard. This means that we treat the C preprocessor, the C standard library, floating point arithmetic, and 'dirty' C features like signal handling and volatile variables. Importantly, this means we also treat embedded C programs without explicit input/output.

Floating point operations are fast, but require continuous effort on the part of the user in order to ensure that the results are correct. This burden can be shifted away from the user by providing a library of exact analysis in which the computer handles the error estimates. We provide an implementation of the exact real numbers in the Coq proof assistant. This improves on the earlier Coq-implementation by O'Connor in two ways: we use dyadic rationals built from the machine integers and we optimize computation of power series by using approximate division. Moreover, we use type classes for clean mathematical interfaces. This appears to be the first time that type classes are used in heavy computation. We obtain over a 100 times speed up of the basic operations and indications for improving the Coq system.

We present several steps towards large formal mathematical wikis. The Coq proof assistant together with the CoRN repository are added to the pool of systems handled by the general wiki system described in \cite{DBLP:conf/aisc/UrbanARG10}. A smart re-verification scheme for the large formal libraries in the wiki is suggested for Mizar/MML and Coq/CoRN, based on recently developed precise tracking of mathematical dependencies. We propose to use features of state-of-the-art filesystems to allow real-time cloning and sandboxing of the entire libraries, allowing also to extend the wiki to a true multi-user collaborative area. A number of related issues are discussed.

Cylindrical algebraic decompositions (CADs) are a key tool in real algebraic geometry, used primarily for eliminating quantifiers over the reals and studying semi-algebraic sets. In this paper we introduce cylindrical algebraic sub-decompositions (sub-CADs), which are subsets of CADs containing all the information needed to specify a solution for a given problem. We define two new types of sub-CAD: variety sub-CADs which are those cells in a CAD lying on a designated variety; and layered sub-CADs which have only those cells of dimension higher than a specified value. We present algorithms to produce these and describe how the two approaches may be combined with each other and the recent theory of truth-table invariant CAD. We give a complexity analysis showing that these techniques can offer substantial theoretical savings, which is supported by experimentation using an implementation in Maple., 26 pages