6 Result(s)
-
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
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
Formal Management of CAD/CAM Processes
Systematic engineering design processes have many aspects in common with software engineering, with CAD/CAM objects replacing program code as the implementation stage of the development. They are, however, cur...
