TALK KEYWORD INDEX

This page contains an index consisting of author-provided keywords.

3 | |

3D visualization | |

A | |

algebraic data types | |

Artificial intelligence | |

aspects | |

automated reasoning | |

automated theorem proving | |

B | |

Boilerplate | |

C | |

Classification | |

Computational logic | |

conference in intelligent computer mathematics | |

Conference on Intelligent Computer Mathematics | |

conical space | |

connection tableau | |

content creation | |

Continuous Time Markov Chains | |

convex function | |

convex hull | |

convex space | |

Coq | |

Coq Proof Assistant | |

D | |

dataset | |

dependent type theory | |

Doctoral Program | |

Doctoral Programme | |

Documentation | |

Dynamic Dependability Analysis | |

Dynamic Fault Trees | |

Dynamic Reliability Block Diagrams | |

E | |

Elimination theory | |

Energy-Utility Quantiles | |

F | |

first-order theorem proving | |

Formal Analysis | |

Formal Library | |

Formal Mathematics | |

formal proof | |

formal specification | |

formal systems | |

Formal verification | |

formalization of mathematics | |

formalized mathematics | |

G | |

Groebner bases | |

H | |

Higher-Order Logic | |

HOL Theorem Proving | |

HOL4 | |

I | |

increasing/decreasing trails | |

induction | |

Intel SGX | |

Interactive Theorem Proving | |

invited talk | |

Isabelle/HOL | |

K | |

knowledge discovery | |

knowledge management | |

L | |

labeled dataset | |

language features | |

lexicography | |

Library development | |

Linguistic Linked Open Data | |

Linked Open Data | |

Linting | |

M | |

machine learning | |

math language processing | |

mathcomp | |

mathematical knowledge management | |

mathematical language | |

mathematical libraries | |

mathematics | |

Mathematics education | |

mathhub | |

MathIR | |

Matrix identities | |

Metamath Zero | |

metamathematics | |

Mizar formalization | |

MKM system | |

mmt | |

MSC | |

multi-class classification | |

N | |

natural formal mathematics | |

Natural Formal Mathematics Workshop | |

Natural Language Parsing | |

Natural Language Processing | |

Neural Networks | |

NLP | |

Number theory | |

O | |

Ontology | |

P | |

PaMpeR | |

Proof assistant | |

proof assistants | |

Proof certificates | |

proof method recommendation | |

Q | |

querying | |

R | |

recommendation system | |

Recreational mathematics | |

recurrent neural networks | |

S | |

Safe hardware systems | |

search | |

semantics extraction | |

serious games | |

set theory | |

soft types | |

superposition | |

supervised learning | |

System Overview | |

T | |

Tactical Learning | |

term extraction | |

theorem proving | |

theory graphs | |

Thermal-Constrained Scheduling | |

TNN | |

tree neural networks | |

Trusted execution environments | |

Type Theory | |

U | |

undefinedness | |

Universal Algebra | |

User Interface | |

V | |

verification | |

verified theory formalization | |

video game framework | |

virtual reality | |

W | |

weighted graph | |

Word problems | |

workshop talk |