MKM
2007
Springer
14 years 5 months ago
2007
Springer
Abstract. We explore mathematical knowledge in the field of electrical engineering and claim that electrical engineering is a suitable area of application for mathematical knowled...
MKM
2007
Springer
14 years 5 months ago
2007
Springer
Abstract. The disambiguation approach to the input of formulae enables the user to type correct formulae in a terse syntax close to the usual ambiguous mathematical notation. When ...
MKM
2007
Springer
14 years 5 months ago
2007
Springer
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...
MKM
2007
Springer
14 years 5 months ago
2007
Springer
MKM
2007
Springer
14 years 5 months ago
2007
Springer
Abstract. We have formalized material from an introductory real analysis textbook in the proof assistant Scunak. Scunak is a system based on set theory encoded in a dependent type ...
MKM
2007
Springer
14 years 5 months ago
2007
Springer
MKM
2007
Springer
14 years 5 months ago
2007
Springer
We address the problem of automatic synthesis of decision procedures. Our synthesis mechanism consists of several stages and submechanisms and is well-suited to the proof-planning ...
MKM
2007
Springer
14 years 5 months ago
2007
Springer
We present a new framework for the online development of formalized mathematics. This framework allows wiki-style collaboration while providing users with a rendered and browsable ...
MKM
2007
Springer
14 years 5 months ago
2007
Springer
An axiomatic theory represents mathematical knowledge declaratively as a set of axioms. An algorithmic theory represents mathematical knowledge procedurally as a set of algorithms....
MKM
2007
Springer
14 years 5 months ago
2007
Springer
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...