TALK KEYWORD INDEX

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

A | |

active documents | |

adaptive learning | |

Adaptive Learning Assistant) | |

adaptive learning system | |

AI systems | |

Aldor | |

ALeA | |

Alexander dual | |

Algebraic Number Fields | |

Alonzo classical higher-order logic | |

annotation | |

Annotation Tool | |

annotations | |

AnnoTize | |

auto-informalization | |

automated classification | |

automated reasoning | |

Automated Theorem Provers | |

automatic sequence | |

automatic theorem-proving | |

B | |

base ten blocks | |

Benchmarking | |

Bias | |

Big Math | |

Binary Decision Diagrams | |

built-in knowledge | |

C | |

Category theory | |

Change frequency | |

ChatGPT | |

code formatter | |

Code smell | |

coding assistance | |

compound graph layout | |

computational biology | |

Computational Grammar | |

computer algebra | |

Computer algebra libraries | |

computer algebra system | |

concurrency | |

confidence | |

confidential computing | |

Controlled natural language | |

Coq Proof Assistant | |

correctness | |

cross-aspect | |

D | |

Dataset | |

Deep learning | |

Demonstration | |

digitisation | |

disambiguation | |

Dismantlability | |

dynamic geometry | |

E | |

E-Learning system | |

educational software | |

Encyclopedic Dictionary of Mathematics | |

Enhanced content accessibility | |

Evasiveness | |

Examples | |

Experiences | |

External assertions | |

F | |

Families of objects | |

finite automaton | |

First-Order Logic | |

Floating point errors | |

Formal means | |

Formal methods | |

Formal proof | |

formal specification and verification | |

formalisation | |

Formalization | |

Formalization of mathematics | |

Formalization quality | |

formalized mathematics | |

Formally Verified Numerical Methods | |

Formulation generation | |

Foundational libraries | |

free groups | |

G | |

Generalizability | |

GeoGebra | |

group theory | |

Grouped Dependency Visualization Graph | |

H | |

HELPING ALL KIDS STRUGGLING WITH MATHS | |

Heterogeneous formal reasoning | |

HTML5 | |

HTML5 document annotation | |

I | |

Informal means | |

Informal Proofs | |

Interaction | |

Interaction and Evaluation | |

interactions | |

interactive theorem proving | |

Interoperability | |

Interoperability of provers | |

interventions | |

Isabelle | |

Isabelle/HOL | |

Isomorphisms | |

Iterative convergence | |

J | |

Jacobi method | |

JavaScript | |

judgmental equality | |

K | |

KBKF | |

knowledge graph | |

L | |

LambdaPi/Dedukti | |

large language model | |

Large language models | |

LaTeX | |

Lean | |

Lean proof assistant | |

Lean theorem prover | |

learning analytics | |

Learning Assistant | |

Learning Support Services | |

Levebee | |

Libraries of proofs | |

Limitations | |

linear algebra | |

Linear programming word problems | |

Linter | |

Little Theories | |

log of manipulation | |

logical framework | |

Logical puzzles | |

M | |

Machine Learning | |

Machine Learning Datasets | |

Math concepts database | |

Math concepts organization | |

math knowledge management | |

Math word problems | |

Mathematical Knowledge | |

Mathematical Knowledge Management | |

Mathematical Objects | |

Mathematical Software of the Future | |

mathematical terminology | |

Mathematical texts | |

mathematics | |

MathGloss | |

mathlib | |

Mathmatics Subject Classification (MSC) | |

MathML annotations | |

maths | |

mechanization | |

MetiTarski Variable Ordering | |

Mizar | |

Mizar Mathematical Library (MML) | |

MMT | |

Modular gcd Algorithms | |

modularity | |

Module mechanism | |

morphism equality | |

multiple inheritance | |

N | |

Named entity-based augmentation | |

Naproche | |

Natural Language | |

Natural Language Processing | |

Natural Language Proof Checking | |

Natural Proof Checking | |

Nominal AC-Matching | |

Nominal Matching | |

number theory formalization | |

numeric computation | |

O | |

OMDoc | |

On-Line Encyclopedia of Integer Sequences | |

Online catalogue | |

Organizing Mathematical Knowledge | |

P | |

Physics Engine | |

Polynomial Greatest Common Divisors | |

Primitive Elements | |

productive failure | |

Proof | |

Proof assistant | |

Proof assistants | |

proof of algorithm | |

Proof Visualization | |

propositional equality | |

ProVerif | |

PVS | |

Q | |

QBF | |

QParity | |

Query language | |

R | |

React | |

recommendation system | |

remote attestation | |

representation theorems | |

Robotics | |

RusTeX | |

S | |

Semantic Markup | |

semantic service | |

semantic web | |

server side verification | |

Shallow embeddings | |

Simplicial complex | |

Simulation | |

Solver | |

Static analysis | |

STEM document annotation | |

STEM education | |

support systems | |

symbolic security analysis | |

system entry | |

T | |

teaching | |

Tetrapod model | |

theorem proving | |

Theory Graphs | |

theory isomorphism | |

theory morphism | |

theory morphisms | |

Theory Repositories | |

Translation of mathematical statements | |

Translation of natural language into formal code | |

trust | |

Type Theory | |

typeclasses | |

V | |

Verification | |

VSCode for the Web | |

W | |

web application | |

Wiedijk Theorems |