Posts

Showing posts from August, 2021

recent work in math knowledge rep 2021Q3

  2021-Q3 survey of recent work in math knowledge rep Background definitions and motives FAIR Data : ( wikipedia )  data which meet principles of findability , accessibility , interoperability , and reusability . go-fair  principles in more depth Some surveys  (Deep) FAIR Mathematics - (KWARC) 2020-02-25 by Katja Berčič, Michael Kohlhase, Florian Rabe  " Big Math and the One-Brain Barrier : The Tetrapod Model of Mathematical Knowledge" by Jacques Carette, William M. Farmer, Michael Kohlhase, Florian Rabe  Expanded group from McMaster + KWARC shared working notes and tables as of 2020-Feb in: " The Space of Mathematical Software Systems -- A Survey of Paradigmatic Systems" A Survey of Languages for Formalizing Mathematics - (KWARC) 2020  by Cezary Kaliszyk and Florian Rabe Some proceedings Accepted Papers at ITP2021 -- 12th International Conference on Interactive Theorem Proving ITP2021  Proceedings   as a single PDF  CADE 2021 Proceedings (open access at Spring

AxioMagic under Spark on cloud (AWS, Azure, ...)

AxioMagic under Spark on ${ cloud  } AxioMagic relies on functional composition over immutable inputs, thus matching modern evaluation frameworks like Apache Spark, which defines a structured approach to managing data contexts of functional evaluation over data frames.  Spark embodies a refinement of both  ETL and MapReduce methodology.  State machines like Spark require computation and storage resources which may come from any cluster, but today are commonly provided from cloud environments, yielding high volume functional computation at predictable usage-based costs.  We especially value Spark for open scientific dataset analysis, where it is common to work with large data files in interchange formats. Essential features of Spark distributed evaluation Spark assembles batch pipelines to pump datasets of structured records through functional tasks (which may  invoke side-effects, with all necessary stipulations).  This pipeline serves to evaluate a given distributed functional algorit