CICM-13: 13TH CONFERENCE ON INTELLIGENT COMPUTER MATHEMATICS

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

3
3D visualization	TGView3D: a System for 3-Dimensional Visualization of Theory Graphs
A
algebraic data types	Induction with Generalization in Superposition Reasoning
Artificial intelligence	Formally Correct Deduction Methods for Computational Logic
aspects	Towards a Heterogeneous Query Language for Mathematical Knowledge
automated reasoning	Induction with Generalization in Superposition Reasoning First Datasets and Experiments with Neural Conjecturing
automated theorem proving	Guiding Connection Tableau by Recurrent Neural Networks
B
Boilerplate	Leveraging Information Contained in Theory Presentations
C
Classification	AutoMSC: Automatic Assignment of Mathematicas Subject Classification Labels
Computational logic	Formally Correct Deduction Methods for Computational Logic
conference in intelligent computer mathematics	(Invited talk) The evolution of the language of mathematics How Natural is Formal Mathematics?
Conference on Intelligent Computer Mathematics	(Invited talk) Formal Proofs for the Future Integrating Formal Methods into LaTeX Workflows Formalizing Foundational Notions in Naproche-SAD (4 short talks) Why We Need Structured Proofs in Mathematics
conical space	Formal Adventures in Convex and Conical Spaces
connection tableau	Guiding Connection Tableau by Recurrent Neural Networks
content creation	FrameIT: Detangling Knowledge Management from Game Design in Serious Games
Continuous Time Markov Chains	A Framework for Formal Dynamic Dependability Analysis using HOL Theorem Proving (Project Paper)
convex function	Formal Adventures in Convex and Conical Spaces
convex hull	Formal Adventures in Convex and Conical Spaces
convex space	Formal Adventures in Convex and Conical Spaces
Coq	Formal Adventures in Convex and Conical Spaces
Coq Proof Assistant	The Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq
D
dataset	Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)
dependent type theory	Formal Adventures in Convex and Conical Spaces
Doctoral Program	Studying the learning process of student teachers regarding the subject of mathematical terminology in graph theory with the usage of an electronic dictionary High-Precision Semantics Extraction in STEM
Doctoral Programme	Undefinedness and Soft Typing in Formal Mathematics
Documentation	Maintaining a Library of Formal Mathematics
Dynamic Dependability Analysis	A Framework for Formal Dynamic Dependability Analysis using HOL Theorem Proving (Project Paper)
Dynamic Fault Trees	A Framework for Formal Dynamic Dependability Analysis using HOL Theorem Proving (Project Paper)
Dynamic Reliability Block Diagrams	A Framework for Formal Dynamic Dependability Analysis using HOL Theorem Proving (Project Paper)
E
Elimination theory	Formally Verifying Proofs for Algebraic Identities of Matrices
Energy-Utility Quantiles	Formal Verification for Safe and Secure Hardware Systems
F
first-order theorem proving	Induction with Generalization in Superposition Reasoning Interpreting Mathematical Texts in Naproche-SAD (and: From LaTeX to Lean with a controlled natural language)
Formal Analysis	A Framework for Formal Dynamic Dependability Analysis using HOL Theorem Proving (Project Paper)
Formal Library	Leveraging Information Contained in Theory Presentations
Formal Mathematics	Maintaining a Library of Formal Mathematics Interpreting Mathematical Texts in Naproche-SAD (and: From LaTeX to Lean with a controlled natural language)
formal proof	Metamath Zero: Designing a Theorem Prover Prover
formal specification	A Survey of Languages for Formalizing Mathematics
formal systems	Representing Structural Language Features in Formal Meta-Languages
Formal verification	Formal Verification for Safe and Secure Hardware Systems
formalization of mathematics	Adding an Abstraction Barrier to ZF Set Theory
formalized mathematics	A Survey of Languages for Formalizing Mathematics
G
Groebner bases	Formally Verifying Proofs for Algebraic Identities of Matrices
H
Higher-Order Logic	A Framework for Formal Dynamic Dependability Analysis using HOL Theorem Proving (Project Paper)
HOL Theorem Proving	A Framework for Formal Dynamic Dependability Analysis using HOL Theorem Proving (Project Paper)
HOL4	A Framework for Formal Dynamic Dependability Analysis using HOL Theorem Proving (Project Paper) Tree Neural Networks in HOL4
I
increasing/decreasing trails	Formalizing Graph Trail Properties in Isabelle/HOL
induction	Induction with Generalization in Superposition Reasoning
Intel SGX	Formal Verification for Safe and Secure Hardware Systems
Interactive Theorem Proving	The Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq
invited talk	(Invited talk) The evolution of the language of mathematics (Invited talk) Formal Proofs for the Future
Isabelle/HOL	Formalizing Graph Trail Properties in Isabelle/HOL Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)
K
knowledge discovery	A Contextual and Labeled Math-Dataset Derived from NIST's DLMF
knowledge management	Representing Structural Language Features in Formal Meta-Languages
L
labeled dataset	A Contextual and Labeled Math-Dataset Derived from NIST's DLMF
language features	Representing Structural Language Features in Formal Meta-Languages
lexicography	Studying the learning process of student teachers regarding the subject of mathematical terminology in graph theory with the usage of an electronic dictionary
Library development	Maintaining a Library of Formal Mathematics
Linguistic Linked Open Data	OntoMathEdu: a New Linguistically Grounded Educational Mathematical Ontology
Linked Open Data	OntoMathEdu: a New Linguistically Grounded Educational Mathematical Ontology
Linting	Maintaining a Library of Formal Mathematics
M
machine learning	AutoMSC: Automatic Assignment of Mathematicas Subject Classification Labels First Datasets and Experiments with Neural Conjecturing Guiding Connection Tableau by Recurrent Neural Networks Tree Neural Networks in HOL4 Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description) The Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq A Contextual and Labeled Math-Dataset Derived from NIST's DLMF
math language processing	A Contextual and Labeled Math-Dataset Derived from NIST's DLMF
mathcomp	Formal Adventures in Convex and Conical Spaces
mathematical knowledge management	OntoMathEdu: a New Linguistically Grounded Educational Mathematical Ontology FrameIT: Detangling Knowledge Management from Game Design in Serious Games
mathematical language	A Survey of Languages for Formalizing Mathematics
mathematical libraries	TGView3D: a System for 3-Dimensional Visualization of Theory Graphs
mathematics	Metamath Zero: Designing a Theorem Prover Prover
Mathematics education	OntoMathEdu: a New Linguistically Grounded Educational Mathematical Ontology Formalization of elementary number theory in Mizar
mathhub	TGView3D: a System for 3-Dimensional Visualization of Theory Graphs
MathIR	AutoMSC: Automatic Assignment of Mathematicas Subject Classification Labels
Matrix identities	Formally Verifying Proofs for Algebraic Identities of Matrices
Metamath Zero	Metamath Zero: Designing a Theorem Prover Prover
metamathematics	Metamath Zero: Designing a Theorem Prover Prover
Mizar formalization	Formalization of elementary number theory in Mizar
MKM system	FrameIT: Detangling Knowledge Management from Game Design in Serious Games
mmt	FrameIT: Detangling Knowledge Management from Game Design in Serious Games TGView3D: a System for 3-Dimensional Visualization of Theory Graphs
MSC	AutoMSC: Automatic Assignment of Mathematicas Subject Classification Labels
multi-class classification	AutoMSC: Automatic Assignment of Mathematicas Subject Classification Labels
N
natural formal mathematics	(Invited talk) The evolution of the language of mathematics
Natural Formal Mathematics Workshop	(Invited talk) Formal Proofs for the Future How Natural is Formal Mathematics? Integrating Formal Methods into LaTeX Workflows Formalizing Foundational Notions in Naproche-SAD (4 short talks) Why We Need Structured Proofs in Mathematics
Natural Language Parsing	Interpreting Mathematical Texts in Naproche-SAD (and: From LaTeX to Lean with a controlled natural language)
Natural Language Processing	OntoMathEdu: a New Linguistically Grounded Educational Mathematical Ontology
Neural Networks	First Datasets and Experiments with Neural Conjecturing
NLP	High-Precision Semantics Extraction in STEM
Number theory	Formalization of elementary number theory in Mizar
O
Ontology	OntoMathEdu: a New Linguistically Grounded Educational Mathematical Ontology Studying the learning process of student teachers regarding the subject of mathematical terminology in graph theory with the usage of an electronic dictionary
P
PaMpeR	Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)
Proof assistant	Formally Verifying Proofs for Algebraic Identities of Matrices Formally Correct Deduction Methods for Computational Logic
proof assistants	A Survey of Languages for Formalizing Mathematics
Proof certificates	Formally Verifying Proofs for Algebraic Identities of Matrices
proof method recommendation	Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)
Q
querying	Towards a Heterogeneous Query Language for Mathematical Knowledge
R
recommendation system	Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)
Recreational mathematics	Formalization of elementary number theory in Mizar
recurrent neural networks	Guiding Connection Tableau by Recurrent Neural Networks
S
Safe hardware systems	Formal Verification for Safe and Secure Hardware Systems
search	Towards a Heterogeneous Query Language for Mathematical Knowledge
semantics extraction	High-Precision Semantics Extraction in STEM
serious games	FrameIT: Detangling Knowledge Management from Game Design in Serious Games
set theory	Adding an Abstraction Barrier to ZF Set Theory
soft types	Undefinedness and Soft Typing in Formal Mathematics
superposition	Induction with Generalization in Superposition Reasoning
supervised learning	Tree Neural Networks in HOL4
System Overview	The Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq
T
Tactical Learning	The Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq
term extraction	Studying the learning process of student teachers regarding the subject of mathematical terminology in graph theory with the usage of an electronic dictionary
theorem proving	Adding an Abstraction Barrier to ZF Set Theory
theory graphs	FrameIT: Detangling Knowledge Management from Game Design in Serious Games TGView3D: a System for 3-Dimensional Visualization of Theory Graphs
Thermal-Constrained Scheduling	Formal Verification for Safe and Secure Hardware Systems
TNN	Tree Neural Networks in HOL4
tree neural networks	Tree Neural Networks in HOL4
Trusted execution environments	Formal Verification for Safe and Secure Hardware Systems
Type Theory	Interpreting Mathematical Texts in Naproche-SAD (and: From LaTeX to Lean with a controlled natural language)
U
undefinedness	Undefinedness and Soft Typing in Formal Mathematics
Universal Algebra	Leveraging Information Contained in Theory Presentations
User Interface	The Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq
V
verification	Metamath Zero: Designing a Theorem Prover Prover
verified theory formalization	Formalizing Graph Trail Properties in Isabelle/HOL
video game framework	FrameIT: Detangling Knowledge Management from Game Design in Serious Games
virtual reality	TGView3D: a System for 3-Dimensional Visualization of Theory Graphs
W
weighted graph	Formalizing Graph Trail Properties in Isabelle/HOL
Word problems	Formally Verifying Proofs for Algebraic Identities of Matrices
workshop talk	How Natural is Formal Mathematics? Integrating Formal Methods into LaTeX Workflows Formalizing Foundational Notions in Naproche-SAD (4 short talks) Why We Need Structured Proofs in Mathematics

Disclaimer | Powered by EasyChair Smart Program