Sciweavers

MKM
2007
Springer
13 years 9 months ago
Towards Mathematical Knowledge Management for Electrical Engineering
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...
Agnieszka Rowinska-Schwarzweller, Christoph Schwar...
MKM
2007
Springer
13 years 9 months ago
Spurious Disambiguation Error Detection
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 ...
Claudio Sacerdoti Coen, Stefano Zacchiroli
MKM
2007
Springer
13 years 9 months ago
Methods of Relevance Ranking and Hit-content Generation in Math Search
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...
Abdou Youssef
MKM
2007
Springer
13 years 9 months ago
Formal Representation of Mathematics in a Dependently Typed Set Theory
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 ...
Feryal Fulya Horozal, Chad E. Brown
MKM
2007
Springer
13 years 9 months ago
Automatic Synthesis of Decision Procedures: A Case Study of Ground and Linear Arithmetic
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 ...
Predrag Janicic, Alan Bundy
MKM
2007
Springer
13 years 9 months ago
Cooperative Repositories for Formal Proofs
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 ...
Pierre Corbineau, Cezary Kaliszyk
MKM
2007
Springer
13 years 9 months ago
Biform Theories in Chiron
An axiomatic theory represents mathematical knowledge declaratively as a set of axioms. An algorithmic theory represents mathematical knowledge procedurally as a set of algorithms....
William M. Farmer
MKM
2007
Springer
13 years 9 months ago
Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
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...
Andrea Asperti, Enrico Tassi