Sciweavers

MKM
2009
Springer
13 years 11 months ago
A Logically Saturated Extension of
This paper presents a proof language based on the work of Sacerdoti Coen [1,2], Kirchner [3] and Autexier [4] on ¯λµ˜µ, a calculus introduced by Curien and Herbelin [5,6]. Jus...
Lionel Elie Mamane, Herman Geuvers, James McKinna
MKM
2009
Springer
13 years 11 months ago
Natural Deduction Environment for Matita
Abstract. Matita is a proof assistant characterised by a rich, user extensible, output facility based on a widget for the rendering of MathML Presentation, and by the automatic han...
Claudio Sacerdoti Coen, Enrico Tassi
MKM
2009
Springer
13 years 11 months ago
Algorithms for the Functional Decomposition of Laurent Polynomials
Abstract. Recent work has detailed the conditions under which univariate Laurent polynomials have functional decompositions. This paper presents algorithms to compute such univaria...
Stephen M. Watt
MKM
2009
Springer
13 years 11 months ago
Reasoning with Generic Cases in the Arithmetic of Abstract Matrices
Alan P. Sexton, Volker Sorge, Stephen M. Watt
MKM
2009
Springer
13 years 11 months ago
A Comparison of Equality in Computer Algebra and Correctness in Mathematical Pedagogy
Russell J. Bradford, James H. Davenport, Christoph...
MKM
2009
Springer
13 years 11 months ago
MathLang Translation to Isabelle Syntax
Converting mathematical documents from a human-friendly natural language to a form that can be readily processed by computers is often a tedious, manual task. Translating between v...
Robert Lamar, Fairouz Kamareddine, J. B. Wells
MKM
2009
Springer
13 years 11 months ago
A Review of Mathematical Knowledge Management
Mathematical Knowledge Management (MKM), as a field, has seen tremendous growth in the last few years. This period was one where many research threads were started and the field ...
Jacques Carette, William M. Farmer
MKM
2009
Springer
13 years 11 months ago
Finite Groups Representation Theory with Coq
Representation theory is a branch of algebra that allows the study of groups through linear applications, i.e. matrices. Thus problems in abstract groups can be reduced to problems...
Sidi Ould Biha
MKM
2009
Springer
13 years 11 months ago
From Tessellations to Table Interpretation
The extraction of the relations of nested table headers to content cells is automated with a view to constructing narrow domain ontologies of semistructured web data. A taxonomy of...
Ramana C. Jandhyala, Mukkai S. Krishnamoorthy, Geo...
MKM
2009
Springer
13 years 11 months ago
OpenMath in SCIEnce: SCSCP and POPCORN
In this short communication we want to give an overview of how OpenMath is used in the European project “SCIEnce” [12]. The main aim of this project is to allow unified commun...
Peter Horn, Dan Roozemond