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...
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...
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...
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 ...
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...
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...
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...
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 ...