Intelligent Computer Mathematics
9th International Conference, CICM 2016, Bialystok, Poland, July 25-29, 2016, Proceedings
Page
%P
100 Result(s)
within
Michael Kohlhase
Mathematical Logic and Formal Languages
-
Chapter and Conference Paper
Learning Support Systems Based on Mathematical Knowledge Management
To cater to the increasingly diverse student bodies, higher education has to personalize education. In times of stagnant educational budgets and staffing problems, this can only be achieved via adaptive, inter...
-
Chapter and Conference Paper
Towards an Annotation Standard for STEM Documents
When publishing papers, researchers in mathematics and related disciplines typically focus on the presentation, i.e. type-setting, of their ideas and provide little semantic information. This impedes the devel...
-
Article
Open AccessExperiences from Exporting Major Proof Assistant Libraries
The interoperability of proof assistants and the integration of their libraries is a highly valued but elusive goal in the field of theorem proving. As a preparatory step, in previous work, we translated the l...
-
Chapter and Conference Paper
Logic-Independent Proof Search in Logical Frameworks
Logical frameworks like LF allow to specify the syntax and (natural deduction) inference rules for syntax/proof-checking a wide variety of logical systems. A crucial feature that is missing for prototy** log...
-
Chapter and Conference Paper
Discourse Phenomena in Mathematical Documents
Much of the wealth of industrialized societies is based on knowledge that is laid down and communicated in scientific/technical/engineering/mathematical documents: highly structured documents that contain diag...
-
Chapter and Conference Paper
Theories as Types
Theories are an essential structuring principle that enable modularity, encapsulation, and reuse in formal libraries and programs (called classes there). Similar effects can be achieved by dependent record typ...
-
Chapter and Conference Paper
Knowledge Amalgamation for Computational Science and Engineering
This paper addresses a knowledge gap that is commonly encountered in computational science and engineering: To set up a simulation, we need to combine domain knowledge (usually in terms of physical principles), m...
-
Chapter and Conference Paper
Automatically Finding Theory Morphisms for Knowledge Management
We present a method for finding morphisms between formal theories, both within as well as across libraries based on different logical foundations. As they induce new theorems in the target theory for any of th...
-
Chapter and Conference Paper
Translating the IMPS Theory Library to MMT/OMDoc
The IMPS system by Farmer, Guttman and Thayer was an influential automated reasoning system, pioneering mechanisations of features like theory morphisms, partial functions with subsorts, and the little theories a...
-
Chapter and Conference Paper
Mathematical Models as Research Data via Flexiformal Theory Graphs
Mathematical modeling and simulation (MMS) has now been established as an essential part of the scientific work in many disciplines. It is common to categorize the involved numerical data and to some extent th...
-
Chapter and Conference Paper
Knowledge-Based Interoperability for Mathematical Software Systems
There is a large ecosystem of mathematical software systems. Individually, these are optimized for particular domains and functionalities, and together they cover many needs of practical and theoretical mathem...
-
Chapter and Conference Paper
Classification of Alignments Between Concepts of Formal Mathematical Systems
Mathematical knowledge is publicly available in dozens of different formats and languages, ranging from informal (e.g. Wikipedia) to formal corpora (e.g., Mizar). Despite an enormous amount of overlap between ...
-
Chapter and Conference Paper
Visual Structure in Mathematical Expressions
Mathematics uses formulae to express knowledge about objects concisely and economically. Mathematical formulae are at the same time an indispensable tool for the initiated and a formidable barrier to novices. ...
-
Chapter and Conference Paper
Virtual Theories – A Uniform Interface to Mathematical Knowledge Bases
To support mathematical research, engineering, and education by computer systems, we need to deal with the differences between mathematical content collections and information systems available today. Unfortun...
-
Chapter and Conference Paper
Making PVS Accessible to Generic Services by Interpretation in a Universal Format
PVS is one of the most powerful proof assistant systems and its libraries of formalized mathematics are among the most comprehensive albeit under-appreciated ones. A characteristic feature of PVS is the use of...
-
Chapter and Conference Paper
Software Citations, Information Systems, and Beyond
Even though software plays an ever-increasing role in today’s research and engineering processes, the scholarly publication process has not quite caught up with this. In particular, referencing and citing soft...
-
Book and Conference Proceedings
-
Chapter and Conference Paper
Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach
OpenDreamKit – “Open Digital Research Environment Toolkit for the Advancement of Mathematics” – is an H2020 EU Research Infrastructure project that aims at supporting, over the period 2015–2019, the eco...
-
Chapter and Conference Paper
Math Literate Knowledge Management via Induced Material
Mathematicians integrate acquired knowledge into a mental model. For trained mathematicians, the mental model seems to include not just the bare facts, but various induced forms of knowledge, and the amount of...
-
Chapter and Conference Paper
A Flexiformal Model of Knowledge Dissemination and Aggregation in Mathematics
In the traditional knowledge dissemination process in mathematics and sciences, authors write semi-selfcontained articles which are then published in journals, conference proceedings, preprint archives, and/or...
