Sciweavers

AISC
2010
Springer
13 years 9 months ago
Some Considerations on the Usability of Interactive Provers
In spite of the remarkable achievements recently obtained in the field of mechanization of formal reasoning, the overall usability of interactive provers does not seem to be sensib...
Andrea Asperti, Claudio Sacerdoti Coen
AISC
2010
Springer
14 years 27 days ago
Proviola: A Tool for Proof Re-animation
Carst Tankink, Herman Geuvers, James McKinna, Free...
AISC
2010
Springer
14 years 1 months ago
On Building a Knowledge Base for Stability Theory
A lot of mathematical knowledge has been formalized and stored in repositories by now: Different mathematical theorems and theories have been taken into consideration and included ...
Agnieszka Rowinska-Schwarzweller, Christoph Schwar...
AISC
2010
Springer
14 years 1 months ago
On Duplication in Mathematical Repositories
Abstract. Building a repository of proof-checked mathematical knowledge is without any doubt a lot of work, and besides the actual formalization process there is also the task of m...
Adam Grabowski, Christoph Schwarzweller
AISC
2010
Springer
14 years 2 months ago
A Formal Quantifier Elimination for Algebraically Closed Fields
We prove formally that the first order theory of algebraically closed fields enjoy quantifier elimination, and hence is decidable. This proof is organized in two modular parts. We ...
Cyril Cohen, Assia Mahboubi
AISC
2010
Springer
14 years 2 months ago
How to Correctly Prune Tropical Trees
We present tropical games, a generalization of combinatorial min-max games based on tropical algebras. Our model breaks the traditional symmetry of rational zero-sum games where pl...
Jean-Vincent Loddo, Luca Saiu
AISC
2010
Springer
14 years 3 months ago
Structured Formal Development with Quotient Types in Isabelle/HOL
General purpose theorem provers provide sophisticated proof methods, but lack some of the advanced structuring mechanisms found in specification languages. This paper builds on pr...
Maksym Bortin, Christoph Lüth
AISC
2010
Springer
14 years 3 months ago
Dimensions of Formality: A Case Study for MKM in Software Engineering
Abstract. We study the formalization process of a collection of documents created for a Software Engineering project from an MKM perspective. We analyze how document and collection...
Andrea Kohlhase, Michael Kohlhase, Christoph Lange...
AISC
2010
Springer
14 years 3 months ago
An OpenMath Content Dictionary for Tensor Concepts
We introduce a new OpenMath content dictionary named “tensor1” containing symbols for the expression of tensor formulas. These symbols support the expression of non-Cartesian ...
Joseph B. Collins