Titlebook: Intelligent Computer Mathematics; 18th Symposium, Calc James H. Davenport,William M. Farmer,Florian Rabe Conference proceedings 2011 Spring

botany

Using , in the Formalization of Theoretical Economicsematical proofs for certain axiomatized economical situations. Such proofs can—at least in principle—also be carried through in formal systems such as .. In this paper we describe experiments carried through using the . system to prove theorems about a particular form of games called pillage games.

灵敏

经典

Computer Certified Efficient Exact Reals in , can be shifted away from the user by providing a library of . analysis in which the computer handles the error estimates. We provide an implementation of the exact real numbers in the . proof assistant. This improves on the earlier .-implementation by O’Connor in two ways: we use dyadic rationals b

Ringworm

A Foundational View on Integration Problemsr, we use integration for the scenario where we have two systems that we integrate by moving problems and solutions between them. While this scenario is often approached from an engineering perspective, we take a foundational view. Based on the generic declarative language MMT, we develop a theoreti

STALL

Isometric

Large Formal Wikis: Issues and Solutionss handled by the general wiki system described in [10]. A smart re-verification scheme for the large formal libraries in the wiki is suggested for ./MML and ./CoRN, based on recently developed precise tracking of mathematical dependencies. We propose to use features of state-of-the-art filesystems t

DRAFT

Licensing the , Mathematical Librarye number of authors and maintainers. Yet the legal status of these efforts of the . community has never been clarified. In 2010, after many years of loose deliberations, the community decided to investigate the issue of licensing the content of the ., thereby clarifying and crystallizing the status

标准

projectile

Alcove