CICM 2023: 16TH CONFERENCE ON INTELLIGENT COMPUTER MATHEMATICS

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

A
active documents	Presentation of Active Documents in ALeA
adaptive learning	Presentation of Active Documents in ALeA
Adaptive Learning Assistant)	ALeA
adaptive learning system	Theory Morphisms in Computer Supported Education
AI systems	How can we make trustworthy AI?
Aldor	Extracting Theory Graphs from the Aldor Library
ALeA	Presentation of Active Documents in ALeA ALeA
Alexander dual	Evasiveness through Binary Decision Diagrams
Algebraic Number Fields	Doctoral Program Proposal Computing GCDs of Multivariate Polynomials over Algebraic Number Fields Presented with Multiple Extensions
Alonzo classical higher-order logic	Little Theories: A Method for Organizing Mathematical Knowledge Illustrated Using Alonzo, a Practice-Oriented Version of Simple Type Theory (Invited Talk)
annotation	Extracting Mathematical Concepts with Large Language Models
Annotation Tool	AnnoTize: A Flexible Annotation Tool for Documents with Mathematical Formulae
annotations	Towards an Annotation Standard for STEM Documents: Datasets, Benchmarks, and Spotters AnnoTize
AnnoTize	AnnoTize
auto-informalization	Informalizing formalized mathematics using the Lean theorem prover (Invited Talk)
automated classification	Classification and Dependency Visualization of the Articles of the Mizar Mathematical Library
automated reasoning	GeoGebra Discovery (system entry)
Automated Theorem Provers	VizAR: Visualization of Automated Reasoning Proofs
automatic sequence	Proving Results About OEIS Sequences with Walnut
automatic theorem-proving	Proving Results About OEIS Sequences with Walnut
B
base ten blocks	Digitising Advanced Interactions with Base Ten Blocks on a Grid
Benchmarking	True Crafted Formula Families for Benchmarking Quantified Satisfiability Solvers
Bias	An Augmented MetiTarski Dataset for Real Quantifier Elimination using Machine Learning
Big Math	Aspects of Mathematical Knowledge
Binary Decision Diagrams	Evasiveness through Binary Decision Diagrams
built-in knowledge	Extending Numeric Automation for Number Theory Formalizations in Mizar
C
Category theory	Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation Categorical Proofs are Natural Proofs
Change frequency	Formalization Quality in Isabelle
ChatGPT	Classification and Dependency Visualization of the Articles of the Mizar Mathematical Library VSCode Extension for the Web and Coding Assistance for the Mizar Language Solving logical puzzles with ChatGPT
code formatter	VSCode Extension for the Web and Coding Assistance for the Mizar Language
Code smell	Formalization Quality in Isabelle
coding assistance	VSCode Extension for the Web and Coding Assistance for the Mizar Language
compound graph layout	Classification and Dependency Visualization of the Articles of the Mizar Mathematical Library
computational biology	Isabelle Formalisation of Original Representation Theorems
Computational Grammar	Type Theories for Computational Grammar of Natural Language (Invited Talk)
computer algebra	Proving an Execution of an Algorithm Correct?
Computer algebra libraries	Extracting Theory Graphs from the Aldor Library
computer algebra system	Framework for building an E-Learning system using existing teaching materials
concurrency	Isabelle Formalisation of Original Representation Theorems
confidence	How can we make trustworthy AI?
confidential computing	Formal Specification and Verification of Attestation in Confidential Computing
Controlled natural language	Scaling a natural proof assistant step by step
Coq Proof Assistant	Categorical Proofs are Natural Proofs
correctness	Proving an Execution of an Algorithm Correct?
cross-aspect	Panel discussion on the Mathematical Software of the Future
D
Dataset	ProofLang: the Language of arXiv Proofs
Deep learning	Formalization Quality in Isabelle
Demonstration	Naproche Demo Levebee Grouped Dependency Visualization Graph of Mizar Articles ALeA Naproche demonstration AnnoTize
digitisation	Digitising Advanced Interactions with Base Ten Blocks on a Grid
disambiguation	Towards computer-assisted semantic markup of mathematical documents
Dismantlability	Evasiveness through Binary Decision Diagrams
dynamic geometry	The learning constructs of inquiry-based mathematics learning represented in the log data of manipulating dynamic content
E
E-Learning system	Framework for building an E-Learning system using existing teaching materials
educational software	Learning Support Systems based on Mathematical Knowledge Management Presentation of Active Documents in ALeA
Encyclopedic Dictionary of Mathematics	Classification and Dependency Visualization of the Articles of the Mizar Mathematical Library
Enhanced content accessibility	AnnoTize: A Flexible Annotation Tool for Documents with Mathematical Formulae
Evasiveness	Evasiveness through Binary Decision Diagrams
Examples	A Catalogue of Mathematical Objects — micropublishing knowledge of examples
Experiences	Experiences with Natural Language Proof Checking
External assertions	Formal Reasoning using Distributed Assertions
F
Families of objects	Isomorphisms and Interoperability
finite automaton	Proving Results About OEIS Sequences with Walnut
First-Order Logic	Proving Results About OEIS Sequences with Walnut VizAR: Visualization of Automated Reasoning Proofs
Floating point errors	Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method
Formal means	Building small worlds in mathematical texts by formal and informal means
Formal methods	Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation Nominal AC-Matching (Best Paper)
Formal proof	Progress on proof systems interoperability Isomorphisms and Interoperability
formal specification and verification	Formal Specification and Verification of Attestation in Confidential Computing
formalisation	Isabelle Formalisation of Original Representation Theorems
Formalization	Formalizing Sets, Numbers, and some "Wiedijk Theorems" in Naproche Categorical Proofs are Natural Proofs
Formalization of mathematics	Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation
Formalization quality	Formalization Quality in Isabelle
formalized mathematics	Informalizing formalized mathematics using the Lean theorem prover (Invited Talk)
Formally Verified Numerical Methods	Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method
Formulation generation	Highlighting Named Entities in Input for Auto-Formulation of Optimization Problems
Foundational libraries	Foundational libraries in Naproche
free groups	Formalizing Free Groups in Isabelle/HOL: The Nielsen- Schreier Theorem and the Conjugacy Problem
G
Generalizability	An Augmented MetiTarski Dataset for Real Quantifier Elimination using Machine Learning
GeoGebra	GeoGebra Discovery (system entry)
group theory	Formalizing Free Groups in Isabelle/HOL: The Nielsen- Schreier Theorem and the Conjugacy Problem
Grouped Dependency Visualization Graph	Grouped Dependency Visualization Graph of Mizar Articles
H
HELPING ALL KIDS STRUGGLING WITH MATHS	Levebee
Heterogeneous formal reasoning	Formal Reasoning using Distributed Assertions
HTML5	Framework for building an E-Learning system using existing teaching materials
HTML5 document annotation	AnnoTize: A Flexible Annotation Tool for Documents with Mathematical Formulae
I
Informal means	Building small worlds in mathematical texts by formal and informal means
Informal Proofs	ProofLang: the Language of arXiv Proofs
Interaction	More Interactions in ALeA – Towards New Added-Value Services based on Semantic Markup
Interaction and Evaluation	CheckMate: an adaptable prototype platform for humans to interact with and evaluate LLMs
interactions	Digitising Advanced Interactions with Base Ten Blocks on a Grid
interactive theorem proving	CoProver: A Recommender System for Proof Construction
Interoperability	Progress on proof systems interoperability Formal Reasoning using Distributed Assertions Panel discussion on the Mathematical Software of the Future
Interoperability of provers	Isomorphisms and Interoperability
interventions	Digitising Advanced Interactions with Base Ten Blocks on a Grid
Isabelle	Formalization Quality in Isabelle
Isabelle/HOL	Formalizing Free Groups in Isabelle/HOL: The Nielsen- Schreier Theorem and the Conjugacy Problem
Isomorphisms	Isomorphisms and Interoperability
Iterative convergence	Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method
J
Jacobi method	Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method
JavaScript	Framework for building an E-Learning system using existing teaching materials
judgmental equality	Multiple-inheritance hazards in dependently-typed algebraic hierarchies
K
KBKF	True Crafted Formula Families for Benchmarking Quantified Satisfiability Solvers
knowledge graph	Extracting Mathematical Concepts with Large Language Models
L
LambdaPi/Dedukti	An indexer and query language for libraries written in LambdaPi/Dedukti
large language model	Extracting Mathematical Concepts with Large Language Models
Large language models	CheckMate: an adaptable prototype platform for humans to interact with and evaluate LLMs
LaTeX	Towards computer-assisted semantic markup of mathematical documents
Lean	Multiple-inheritance hazards in dependently-typed algebraic hierarchies
Lean proof assistant	Informalizing formalized mathematics using the Lean theorem prover (Invited Talk)
Lean theorem prover	LeanAIde - A statement autoformalisation tool for the Lean theorem prover
learning analytics	The learning constructs of inquiry-based mathematics learning represented in the log data of manipulating dynamic content
Learning Assistant	More Interactions in ALeA – Towards New Added-Value Services based on Semantic Markup
Learning Support Services	More Interactions in ALeA – Towards New Added-Value Services based on Semantic Markup
Levebee	Levebee
Libraries of proofs	An indexer and query language for libraries written in LambdaPi/Dedukti
Limitations	Solving logical puzzles with ChatGPT
linear algebra	Teaching Linear Algebra in a mechanized mathematical environment
Linear programming word problems	Highlighting Named Entities in Input for Auto-Formulation of Optimization Problems
Linter	Formalization Quality in Isabelle
Little Theories	Little Theories: A Method for Organizing Mathematical Knowledge Illustrated Using Alonzo, a Practice-Oriented Version of Simple Type Theory (Invited Talk)
log of manipulation	The learning constructs of inquiry-based mathematics learning represented in the log data of manipulating dynamic content
logical framework	Morphism Equality in Theory Graphs Progress on proof systems interoperability
Logical puzzles	Solving logical puzzles with ChatGPT
M
Machine Learning	CoProver: A Recommender System for Proof Construction Formalization Quality in Isabelle CheckMate: an adaptable prototype platform for humans to interact with and evaluate LLMs
Machine Learning Datasets	An Augmented MetiTarski Dataset for Real Quantifier Elimination using Machine Learning
Math concepts database	MathGloss: Linked Undergraduate Math Concepts
Math concepts organization	MathGloss: Linked Undergraduate Math Concepts
math knowledge management	Towards an Annotation Standard for STEM Documents: Datasets, Benchmarks, and Spotters
Math word problems	Highlighting Named Entities in Input for Auto-Formulation of Optimization Problems
Mathematical Knowledge	Aspects of Mathematical Knowledge Modularity in Mathematical Knowledge
Mathematical Knowledge Management	Extracting Theory Graphs from the Aldor Library Learning Support Systems based on Mathematical Knowledge Management
Mathematical Objects	A Catalogue of Mathematical Objects — micropublishing knowledge of examples
Mathematical Software of the Future	Panel discussion on the Mathematical Software of the Future
mathematical terminology	Extracting Mathematical Concepts with Large Language Models
Mathematical texts	Building small worlds in mathematical texts by formal and informal means
mathematics	Towards computer-assisted semantic markup of mathematical documents
MathGloss	MathGloss: Linked Undergraduate Math Concepts
mathlib	Multiple-inheritance hazards in dependently-typed algebraic hierarchies
Mathmatics Subject Classification (MSC)	Classification and Dependency Visualization of the Articles of the Mizar Mathematical Library
MathML annotations	AnnoTize: A Flexible Annotation Tool for Documents with Mathematical Formulae
maths	Digitising Advanced Interactions with Base Ten Blocks on a Grid
mechanization	Teaching Linear Algebra in a mechanized mathematical environment
MetiTarski Variable Ordering	An Augmented MetiTarski Dataset for Real Quantifier Elimination using Machine Learning
Mizar	Extending Numeric Automation for Number Theory Formalizations in Mizar Classification and Dependency Visualization of the Articles of the Mizar Mathematical Library VSCode Extension for the Web and Coding Assistance for the Mizar Language Grouped Dependency Visualization Graph of Mizar Articles
Mizar Mathematical Library (MML)	Classification and Dependency Visualization of the Articles of the Mizar Mathematical Library
MMT	Morphism Equality in Theory Graphs Presentation of Active Documents in ALeA
Modular gcd Algorithms	Doctoral Program Proposal Computing GCDs of Multivariate Polynomials over Algebraic Number Fields Presented with Multiple Extensions
modularity	Modularity in Mathematical Knowledge Panel discussion on the Mathematical Software of the Future
Module mechanism	Modularity in Mathematical Knowledge
morphism equality	Morphism Equality in Theory Graphs
multiple inheritance	Multiple-inheritance hazards in dependently-typed algebraic hierarchies
N
Named entity-based augmentation	Highlighting Named Entities in Input for Auto-Formulation of Optimization Problems
Naproche	Formalizing Sets, Numbers, and some "Wiedijk Theorems" in Naproche Experiences with Natural Language Proof Checking Foundational libraries in Naproche Scaling a natural proof assistant step by step Naproche Demo Naproche demonstration
Natural Language	Type Theories for Computational Grammar of Natural Language (Invited Talk)
Natural Language Processing	ProofLang: the Language of arXiv Proofs
Natural Language Proof Checking	Experiences with Natural Language Proof Checking
Natural Proof Checking	Foundational libraries in Naproche Naproche Demo Naproche demonstration
Nominal AC-Matching	Nominal AC-Matching (Best Paper)
Nominal Matching	Nominal AC-Matching (Best Paper)
number theory formalization	Extending Numeric Automation for Number Theory Formalizations in Mizar
numeric computation	Extending Numeric Automation for Number Theory Formalizations in Mizar
O
OMDoc	Extracting Theory Graphs from the Aldor Library
On-Line Encyclopedia of Integer Sequences	Proving Results About OEIS Sequences with Walnut
Online catalogue	A Catalogue of Mathematical Objects — micropublishing knowledge of examples
Organizing Mathematical Knowledge	Little Theories: A Method for Organizing Mathematical Knowledge Illustrated Using Alonzo, a Practice-Oriented Version of Simple Type Theory (Invited Talk)
P
Physics Engine	Physics Engines for Verification of Robotic Systems
Polynomial Greatest Common Divisors	Doctoral Program Proposal Computing GCDs of Multivariate Polynomials over Algebraic Number Fields Presented with Multiple Extensions
Primitive Elements	Doctoral Program Proposal Computing GCDs of Multivariate Polynomials over Algebraic Number Fields Presented with Multiple Extensions
productive failure	The learning constructs of inquiry-based mathematics learning represented in the log data of manipulating dynamic content
Proof	Physics Engines for Verification of Robotic Systems
Proof assistant	Scaling a natural proof assistant step by step
Proof assistants	Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation
proof of algorithm	Proving an Execution of an Algorithm Correct?
Proof Visualization	VizAR: Visualization of Automated Reasoning Proofs
propositional equality	Morphism Equality in Theory Graphs
ProVerif	Formal Specification and Verification of Attestation in Confidential Computing
PVS	Nominal AC-Matching (Best Paper)
Q
QBF	True Crafted Formula Families for Benchmarking Quantified Satisfiability Solvers
QParity	True Crafted Formula Families for Benchmarking Quantified Satisfiability Solvers
Query language	An indexer and query language for libraries written in LambdaPi/Dedukti
R
React	Presentation of Active Documents in ALeA
recommendation system	CoProver: A Recommender System for Proof Construction
remote attestation	Formal Specification and Verification of Attestation in Confidential Computing
representation theorems	Isabelle Formalisation of Original Representation Theorems
Robotics	Physics Engines for Verification of Robotic Systems
RusTeX	Presentation of Active Documents in ALeA
S
Semantic Markup	Towards computer-assisted semantic markup of mathematical documents More Interactions in ALeA – Towards New Added-Value Services based on Semantic Markup
semantic service	Theory Morphisms in Computer Supported Education
semantic web	Towards an Annotation Standard for STEM Documents: Datasets, Benchmarks, and Spotters
server side verification	VSCode Extension for the Web and Coding Assistance for the Mizar Language
Shallow embeddings	Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation
Simplicial complex	Evasiveness through Binary Decision Diagrams
Simulation	Physics Engines for Verification of Robotic Systems
Solver	True Crafted Formula Families for Benchmarking Quantified Satisfiability Solvers
Static analysis	Formalization Quality in Isabelle
STEM document annotation	AnnoTize: A Flexible Annotation Tool for Documents with Mathematical Formulae
STEM education	Theory Morphisms in Computer Supported Education
support systems	Learning Support Systems based on Mathematical Knowledge Management
symbolic security analysis	Formal Specification and Verification of Attestation in Confidential Computing
system entry	GeoGebra Discovery (system entry)
T
teaching	Teaching Linear Algebra in a mechanized mathematical environment
Tetrapod model	Aspects of Mathematical Knowledge
theorem proving	Isabelle Formalisation of Original Representation Theorems
Theory Graphs	Extracting Theory Graphs from the Aldor Library Morphism Equality in Theory Graphs
theory isomorphism	Morphism Equality in Theory Graphs
theory morphism	Theory Morphisms in Computer Supported Education
theory morphisms	Morphism Equality in Theory Graphs
Theory Repositories	Extracting Theory Graphs from the Aldor Library
Translation of mathematical statements	LeanAIde - A statement autoformalisation tool for the Lean theorem prover
Translation of natural language into formal code	LeanAIde - A statement autoformalisation tool for the Lean theorem prover
trust	How can we make trustworthy AI?
Type Theory	Type Theories for Computational Grammar of Natural Language (Invited Talk)
typeclasses	Multiple-inheritance hazards in dependently-typed algebraic hierarchies
V
Verification	Physics Engines for Verification of Robotic Systems
VSCode for the Web	VSCode Extension for the Web and Coding Assistance for the Mizar Language
W
web application	Framework for building an E-Learning system using existing teaching materials
Wiedijk Theorems	Formalizing Sets, Numbers, and some "Wiedijk Theorems" in Naproche

Disclaimer | Powered by EasyChair Smart Program