CICM 2023: 16TH CONFERENCE ON INTELLIGENT COMPUTER MATHEMATICS

A
Agrawal, Ayush	LeanAIde - A statement autoformalisation tool for the Lean theorem prover
Al Wardani, Farah	Formal Reasoning using Distributed Assertions
Ansari, Mahsa	Doctoral Program Proposal Computing GCDs of Multivariate Polynomials over Algebraic Number Fields Presented with Multiple Extensions
Appel, Andrew	Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method
Aransay, Jesús	Evasiveness through Binary Decision Diagrams
Ayala-Rincón, Mauricio	Nominal AC-Matching (Best Paper)
B
Badyal, Arjun	Physics Engines for Verification of Robotic Systems
Bayer, Jonas	Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation
Benzmüller, Christoph	Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation
Berges, Marc	Learning Support Systems based on Mathematical Knowledge Management
Berry, David	Categorical Proofs are Natural Proofs
Betzendahl, Jonas	Learning Support Systems based on Mathematical Knowledge Management
Bindel, David	Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method
Blanqui, Frédéric	Progress on proof systems interoperability
Brown, Christopher	GeoGebra Discovery (system entry)
C
Caminati, Marco B.	Isabelle Formalisation of Original Representation Theorems
Chugh, Abhishek	Learning Support Systems based on Mathematical Knowledge Management Presentation of Active Documents in ALeA ALeA
Collins, Katie	CheckMate: an adaptable prototype platform for humans to interact with and evaluate LLMs
Corless, Robert	Teaching Linear Algebra in a mechanized mathematical environment
D
Davenport, James	Proving an Execution of an Algorithm Correct?
De Lon, Adrian	Scaling a natural proof assistant step by step Naproche Demo
de Paiva, Valeria	Extracting Mathematical Concepts with Large Language Models
Dubois, Catherine	Isomorphisms and Interoperability
F
Farmer, William	Little Theories: A Method for Organizing Mathematical Knowledge Illustrated Using Alonzo, a Practice-Oriented Version of Simple Type Theory (Invited Talk)
Fernandez, Maribel	Nominal AC-Matching (Best Paper)
Ferreira Silva, Gabriel	Nominal AC-Matching (Best Paper)
G
Gadgil, Siddhartha	LeanAIde - A statement autoformalisation tool for the Lean theorem prover
Gangwar, Neeraj	Highlighting Named Entities in Input for Auto-Formulation of Optimization Problems
Gao, Qiyue	Extracting Mathematical Concepts with Large Language Models
Gonus, Alexey	Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation
Goyal, Navin	LeanAIde - A statement autoformalisation tool for the Lean theorem prover
Groza, Adrian	Solving logical puzzles with ChatGPT
H
Hammer, Henry	ProofLang: the Language of arXiv Proofs
Heisinger, Simone	True Crafted Formula Families for Benchmarking Quantified Satisfiability Solvers
Hellström, Lars	A Catalogue of Mathematical Objects — micropublishing knowledge of examples
Hester, John	An Augmented MetiTarski Dataset for Real Quantifier Elimination using Machine Learning
Hitaj, Briland	CoProver: A Recommender System for Proof Construction An Augmented MetiTarski Dataset for Real Quantifier Elimination using Machine Learning
Horowitz, Lucy	MathGloss: Linked Undergraduate Math Concepts
Huch, Fabian	Formalization Quality in Isabelle
Hudeček, Michal	Levebee Digitising Advanced Interactions with Base Ten Blocks on a Grid
J
Jakubuv, Jan	VizAR: Visualization of Automated Reasoning Proofs
Jamnik, Mateja	How can we make trustworthy AI?
Jeannin, Jean-Baptiste	Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method
Jeffrey, David J.	Teaching Linear Algebra in a mechanized mathematical environment
K
Kaliszyk, Cezary	VizAR: Visualization of Automated Reasoning Proofs
Kaneko, Masataka	The learning constructs of inquiry-based mathematics learning represented in the log data of manipulating dynamic content
Kani, Nickvash	Highlighting Named Entities in Input for Auto-Formulation of Optimization Problems
Kellison, Ariel	Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method
Kharim, Aabid Seeyal Abdul	Formalizing Free Groups in Isabelle/HOL: The Nielsen- Schreier Theorem and the Conjugacy Problem
Kitamoto, Takuya	Framework for building an E-Learning system using existing teaching materials
Koepke, Peter	Naproche demonstration Experiences with Natural Language Proof Checking Formalizing Sets, Numbers, and some "Wiedijk Theorems" in Naproche
Kohlhase, Andrea	More Interactions in ALeA – Towards New Added-Value Services based on Semantic Markup
Kohlhase, Michael	Learning Support Systems based on Mathematical Knowledge Management Towards an Annotation Standard for STEM Documents: Datasets, Benchmarks, and Spotters Presentation of Active Documents in ALeA Aspects of Mathematical Knowledge More Interactions in ALeA – Towards New Added-Value Services based on Semantic Markup
Kovalev, Pavel	Extracting Mathematical Concepts with Large Language Models
Kovács, Zoltán	GeoGebra Discovery (system entry)
Kutsia, Temur	Nominal AC-Matching (Best Paper)
L
Lambán, Laureano	Evasiveness through Binary Decision Diagrams
Lohr, Dominic	Learning Support Systems based on Mathematical Knowledge Management
Loukanova, Roussanka	Type Theories for Computational Grammar of Natural Language (Invited Talk)
M
Marcol, Mateusz	Formalizing Sets, Numbers, and some "Wiedijk Theorems" in Naproche
Matsumoto, Ryutaro	VSCode Extension for the Web and Coding Assistance for the Mizar Language
Miller, Kyle	Informalizing formalized mathematics using the Lean theorem prover (Invited Talk)
Miyata, Haruka	VSCode Extension for the Web and Coding Assistance for the Mizar Language
Monagan, Michael	Doctoral Program Proposal Computing GCDs of Multivariate Polynomials over Algebraic Number Fields Presented with Multiple Extensions
Moss, Larry	Extracting Mathematical Concepts with Large Language Models
Müller, Dennis	Learning Support Systems based on Mathematical Knowledge Management Presentation of Active Documents in ALeA
N
Nagasaki, Masahiro	Classification and Dependency Visualization of the Articles of the Mizar Mathematical Library
Nakahara, Takahiro	The learning constructs of inquiry-based mathematics learning represented in the log data of manipulating dynamic content
Nakasho, Kazuhisa	VSCode Extension for the Web and Coding Assistance for the Mizar Language Classification and Dependency Visualization of the Articles of the Mizar Mathematical Library
Nantes-Sobrinho, Daniele	Nominal AC-Matching (Best Paper)
Narayanan, Ashvni	LeanAIde - A statement autoformalisation tool for the Lean theorem prover
Naumowicz, Adam	Extending Numeric Automation for Number Theory Formalizations in Mizar
Noda, Nanako	ProofLang: the Language of arXiv Proofs
Noda, Takeo	The learning constructs of inquiry-based mathematics learning represented in the log data of manipulating dynamic content
O
Owre, Sam	An Augmented MetiTarski Dataset for Real Quantifier Elimination using Machine Learning
Owre, Sam	CoProver: A Recommender System for Proof Construction
P
Panzer, Lukas	AnnoTize: A Flexible Annotation Tool for Documents with Mathematical Formulae
Passmore, Grant	An Augmented MetiTarski Dataset for Real Quantifier Elimination using Machine Learning
Paulson, Lawrence	Large-Scale Formal Proof for the Working Mathematician – Lessons Learnt from the ALEXANDRIA Project
Prathamesh, T.V.H.	Formalizing Free Groups in Isabelle/HOL: The Nielsen- Schreier Theorem and the Conjugacy Problem
Q
Quemener, Maena	CoProver: A Recommender System for Proof Construction
R
Rabe, Florian	Morphism Equality in Theory Graphs Extracting Theory Graphs from the Aldor Library Panel discussion on the Mathematical Software of the Future
Rajiv, Shweta	Formalizing Free Groups in Isabelle/HOL: The Nielsen- Schreier Theorem and the Conjugacy Problem
Recio, Tomas	GeoGebra Discovery (system entry)
Rubio, Julio	Evasiveness through Binary Decision Diagrams
S
Sacerdoti Coen, Claudio	An indexer and query language for libraries written in LambdaPi/Dedukti
Sardar, Muhammad Usama	Formal Specification and Verification of Attestation in Confidential Computing
Schaefer, Jan Frederik	Towards an Annotation Standard for STEM Documents: Datasets, Benchmarks, and Spotters AnnoTize: A Flexible Annotation Tool for Documents with Mathematical Formulae
Schaefer, Jan Frederik	AnnoTize
Schröder, Bernhard	Building small worlds in mathematical texts by formal and informal means
Schäfer, Patrick	Formalizing Sets, Numbers, and some "Wiedijk Theorems" in Naproche
Schütz, Marcel	Theory Morphisms in Computer Supported Education Foundational libraries in Naproche
Scott, Dana	Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation
Seidl, Martina	Never Trust Your Solver: Certification for SAT and QBF True Crafted Formula Families for Benchmarking Quantified Satisfiability Solvers
Shakoori, Azar	Teaching Linear Algebra in a mechanized mathematical environment
Shallit, Jeffrey	Proving Results About OEIS Sequences with Walnut
Shankar, Natarajan	An Augmented MetiTarski Dataset for Real Quantifier Elimination using Machine Learning Modularity in Mathematical Knowledge
Shankar, Natarajan	CoProver: A Recommender System for Proof Construction
Stathopoulos, Yiannos	Formalization Quality in Isabelle
Stone, Christopher	ProofLang: the Language of arXiv Proofs
Suzuki, Shotaro	Classification and Dependency Visualization of the Articles of the Mizar Mathematical Library Grouped Dependency Visualization Graph of Mizar Articles
T
Tadipatri, Anand Rao	LeanAIde - A statement autoformalisation tool for the Lean theorem prover
Tekriwal, Mohit	Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method
V
Vajda, Robert	GeoGebra Discovery (system entry)
Velez, M. Pilar	GeoGebra Discovery (system entry)
Vrečar, Luka	Towards computer-assisted semantic markup of mathematical documents
Vyas, Rishi	Formalizing Free Groups in Isabelle/HOL: The Nielsen- Schreier Theorem and the Conjugacy Problem
W
Watt, Stephen	Extracting Theory Graphs from the Aldor Library
Weber, Franziska	Morphism Equality in Theory Graphs
Wieser, Eric	Multiple-inheritance hazards in dependently-typed algebraic hierarchies
Y
Yeh, Eric	CoProver: A Recommender System for Proof Construction An Augmented MetiTarski Dataset for Real Quantifier Elimination using Machine Learning

Disclaimer | Powered by EasyChair Smart Program