yusuke1997/dblp-id-title huggingface dataset:
IsarMathLib - a Formalized Mathematics Library for Isabelle/ZF
Some Traditional Mathematical Knowledge Management
Verified Optimization (work in progress)
An Interactive Algebra Course with Formalised Proofs and Definitions
Automated Generation of Exam Sheets for Automated Deduction
Intelligent Computer Mathematics - 16th International Conference, CICM 2023, Cambridge, UK, September 5-8, 2023, Proceedings
Software for Evaluating Relevance of Steps in Algebraic Transformations
Maintaining a Library of Formal Mathematics
Math Handwriting Recognition in Windows 7 and Its Benefits
Math-Literate Computers
Workflows for the Management of Change in Science, Technologies, Engineering and Mathematics
CICM'21 Systems Entries
Reusing Learning Objects via Theory Morphisms
A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity
Restoring Natural Language as a Computerised Mathematics Input Method
Incorporating a Database of Graphs into a Proof Assistant
A New Export of the Mizar Mathematical Library
Solving Hard Mizar Problems with Instantiation and Strategy Invention
Spreadsheets: from data interfaces to knowledge interfaces
Making the Census of Cubic Vertex Transitive Graphs Searchable and FAIR
LeoPARD - A Generic Platform for the Implementation of Higher-Order Reasoners
Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories
Variadic Equational Matching
Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach
Towards Collaborative Content Management and Version Control for Structured Mathematical Knowledge
Collaborative Assistant to Handle MathML Expressions
Computational Logic and Continuous Mathematics, Pure and Applied
Experiments with Automated Reasoning in the Class
C-CoRN, the Constructive Coq Repository at Nijmegen
A Database of Glyphs for OCR of Mathematical Documents
Global, Regional, and Local Contexts
Creating a Database of Definitions From Large Mathematical Corpora
Roles of Math Search in Mathematics
Improving Stateful Premise Selection with Transformers
Semantic Matching for Mathematical Services
Authoring LeActiveMath Calculus Content
Beginners' Quest to Formalize Mathematics: A Feasibility Study in Isabelle
Mathematical Practice, Crowdsourcing, and Social Machines
Automated Determination of Isoptics with Dynamic Geometry
A Path to Faithful Formalizations of Mathematics
Generating Formally Verified Quantum Fourier Transform Algorithms
Never Trust Your Solver: Certification for SAT and QBF
CICM'22 System Entries
Formalizing Graph Trail Properties in Isabelle/HOL
The Scala-REPL + MMT as a lightweight mathematical user interface
From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfalls
Inspection and Selection of Representations
Spreadsheet Interaction with Frames: Exploring a Mathematical Practice
Algorithms for the Functional Decomposition of Laurent Polynomials
Extending GeoGebra/realgeom with QEPCAD B to obtain proofs on geometric inequalities
Formalizing the Solow Model in $\mathbb {N}$aproche
Computing the Border Array in Isabelle/HOL (short paper)
A Logically Saturated Extension of lambdaµµ
A First Class Boolean Sort in First-Order Theorem Proving and TPTP
Cooperative Repositories for Formal Proofs
VizAR: Visualization of Automated Reasoning Proofs (System Description)
MathUI Preface
Querying Geometric Figures Using a Controlled Language, Ontological Graphs and Dependency Lattices
Towards a Heterogeneous Query Language for Mathematical Knowledge
Interpreting Mathematical Texts in Naproche-SAD
A Web Environment for Geometry
Re examining the MKM Value Proposition: From Math Web Search to Math Web Re Search
The LaTeXML Daemon: Editable Math on the Collaborative Web
Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library
Lurch: a word processor built on OpenMath that can check mathematical reasoning
Towards the Formal Reliability Analysis of Oil and Gas Pipelines
CoProver: A Recommender System for Proof Construction
Synthesizing Proof Planning Methods and Omega-Ants Agents from Mathematical Knowledge
A Language with Type-Dependent Equality
Informalising Formal Mathematics: Searching the Mizar Library with Latent Semantics
Arithmetic in Metamath, Case Study: Bertrand's Postulate
From Untyped to Polymorphically Typed Objects in Mathematical Web Services
Automatically Generalizing Theorems Using Typeclasses (short paper)
Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof Assistants and Computer Algebra System Framework
FrameIT: Detangling Knowledge Management from Game Design in Serious Games
Towards Machine-Actionable Modules of a Digital Mathematics Library - The Example of DML-CZ
Project Abstract: Logic Atlas and Integrator (LATIN)
Computational Origami of a Morley's Triangle
Visualization of Tangent Developables on a Volumetric Display
Morphism Equality in Theory Graphs
Auto-hyperlinking the Stacks Project
Formal Adventures in Convex and Conical Spaces
ProofLang: The Language of arXiv Proofs
A Survey of Languages for Formalizing Mathematics
A Formal Description of an Algorithm Suitable for Parsing the Language of Mathematics
Injecting Formal Mathematics Into LaTeX
True Crafted Formula Families for Benchmarking Quantified Satisfiability Solvers
Knowledge Amalgamation for Computational Science and Engineering
Interactive Simplifier Tracing and Debugging in Isabelle
Automatically Proving Equivalence by Type-Safe Reflection
High Stakes Automatic Assessments: Developing an Online Linear Algebra Examination
Theorem Proving and Proof Verification in the System SAD
An Augmented MetiTarski Dataset for Real Quantifier Elimination Using Machine Learning
OntoMath Edu : Towards an Educational Mathematical Ontology
Goal-Oriented Conjecturing for Isabelle/HOL
Learning to Reason Assisted by Automated Reasoning
The Layers of Logiweb
Formal Mathematics on Display: A Wiki for Flyspeck
Formalization Quality in Isabelle
A Proposal for an OpenMath JSON Encoding
OuterCount: A First-Level Solution-Counter for Quantified Boolean Formulas
A Verified Algorithm Enumerating Event Structures
A Dynamic Symbolic Geometry Environment Based on the GröbnerCover Algorithm for the Computation of Geometric Loci and Envelopes
The Rooster and the Butterflies
Assisted Proof Document Authoring
Accessing the Mizar Library with a Weakly Strict Mizar Parser
Certification of Bounds of Non-linear Functions: The Templates Method
Revisions as an Essential Tool to Maintain Mathematical Repositories
Reaping the Benefits of Modularization in Flexiformal Mathematics by GF-based AST Transformations
Learning to Solve Geometric Construction Problems from Images
Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study
Mathematical Language Processing Project
The full angle method on the OpenGeoProver
Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic
Modeling Interactivity for Mathematics Learning by Demonstration
The Coq Library as a Theory Graph
Gröbner Bases of Modules and Faugère's F 4 Algorithm in Isabelle/HOL
Mathematical Models as Research Data via Flexiformal Theory Graphs
Using Theorema in the Formalization of Theoretical Economics
Efficient Formal Verification of Bounds of Linear Programs
Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings
Towards automatic generation of domain-specific mathematical input support
MathChat: Computational Mathematics via a Social Machine
Quantifiers and n-ary binders: an OpenMath standard enhancement proposal
swMATH - A New Information Service for Mathematical Software
A Coq Formalization of Digital Filters
Generating OpenMath Content Dictionaries from Wikidata (short paper)
Intelligent Computer Mathematics - 9th International Conference, CICM 2016, Bialystok, Poland, July 25-29, 2016, Proceedings
An Approach to Mathematical Search Through Query Formulation and Data Normalization
Gauss-Lintel, an Algorithm Suite for Exploring Chord Diagrams
Formalization of Dubé's Degree Bounds for Gröbner Bases in Isabelle/HOL
Verifying and Invalidating Textbook Proofs Using Scunak
Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description
MathLang Translation to Isabelle Syntax
Automatic Mathematical Information Retrieval to Perform Translations up to Computer Algebra Systems
Extending Flexible Boolean Semantics for the Language of Mathematics
Reasoning Support for Undefinedness and Soft Typing in Formal Mathematics - Extended Abstract
Searching for Mathematical Formulas Based on Graph Representation Learning
TGView3D: A System for 3-Dimensional Visualization of Theory Graphs
Testing Mizar User Interactivity in a University-level Introductory Course on Foundations of Mathematics
alsoMATH - A Database for Mathematical Algorithms and Software
Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings
A Foundational View on Integration Problems
Exploring a Quantum Theory with Graph Rewriting and Computer Algebra
Invariant Properties of Third-Order Non-hyperbolic Linear Partial Differential Operators
Joint Proceedings of the MathUI, OpenMath and ThEdu Workshops and Work in Progress track at CICM co-located with Conferences on Intelligent Computer Mathematics (CICM 2014), Coimbra, Portugal, July 7-11, 2014
A Dynamic Poincaré Principle
Indexing and Searching Mathematics in Digital Libraries - Architecture, Design and Scalability Issues
Towards an Interaction-based Integration of MKM Services into End-User Applications
Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant
System Description: sTeX2.0 - A LaTeX-based Ecosystem for Semantic/Active Mathematical Documents (short paper)
Proceedings of the Mathematical Knowledge Management Symposium, MKM Symposium 2003, Edinburgh, UK, November 25-29, 2003
Evaluation and Domain Adaptation of Similarity Models for Short Mathematical Texts
A Mathematical Structure for Modeling Inventions
mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library
The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq
InkChat: a collaboration tool for mathematics
Learning Support Systems Based on Mathematical Knowledge Management
Proof Mining with Dependent Types
E-books and Graphics with
Towards Mathematical AI via a Model of the Content and Process of Mathematical Question and Answer Dialogues
Improving Mizar Texts with Properties and Requirements
Automated Symbolic and Numerical Testing of DLMF Formulae Using Computer Algebra Systems
Formalization of Complex Vectors in Higher-Order Logic
Natural Typesetting of Naproche Formalizations in LaTeX (short paper)
Students' Comparison of Their Trigonometric Answers with the Answers of a Computer Algebra System
Graded Quantitative Narrowing
Flexary Operators for Formalized Mathematics
Extension Proposal: Records in Pragmatic OpenMath
Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings
Mining the Archive of Formal Proofs
PDF/A-3u as an Archival Format for Accessible Mathematics
Story Based Content Structuring in MATh
A Framework for Interactive Proof
Mathematical Knowledge Management, 4th International Conference, MKM 2005, Bremen, Germany, July 15-17, 2005, Revised Selected Papers
A Formalization of the C99 Standard in HOL, Isabelle and Coq
SAT-Enhanced Mizar Proof Checking
Interactive Learning and Mathematical Calculus
Translating Mizar for First Order Theorem Provers
Alternative Aggregates in Mizar
Leveraging the Information Contained in Theory Presentations
Integrating Semantic Mathematical Documents and Dynamic Notebooks
A Web Platform for Hosting the Mizar Mathematical Library (short paper)
Transforming Optimization Problems into Disciplined Convex Programming Form
Combining Source, Content, Presentation, Narration, and Relational Representation
Unifying Math Ontologies: A Tale of Two Standards
Textbook Proofs Meet Formal Logic - The Problem of Underspecification and Granularity
Using General Large Language Models to Classify Mathematical Documents
A Knowledge Repository for Indefinite Integration Based on Transformation Rules
ML4PG in Computer Algebra Verification
Adaptive Access to a Proof Planner
NNexus Glasses: a drop-in showcase for wikification
Translating Mathematical Vernacular into Knowledge Repositories
Diagram Combinators in MMT
Intelligent Computer Mathematics - 12th International Conference, CICM 2019, Prague, Czech Republic, July 8-12, 2019, Proceedings
Certified Proofs in Programs Involving Exceptions
Intelligent Computer Mathematics - International Conference, CICM 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings
Develop a Mathematical E-Dictionary and Test it - Extended Abstract
Towards Mathematical Knowledge Management for Electrical Engineering
Explorations into the Use of Word Embedding in Math Search and Math Semantics
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems
Boosting Math Problem Solving in Small LLMs via Ensembles
Interaction with Formal Mathematical Documents in Isabelle/PIDE
Aligator.jl - A Julia Package for Loop Invariant Generation
Performance Evaluation and Optimization of Math-Similarity Search
Toward an Object-Oriented Structure for Mathematical Text
System Description: MathHub.info
Pattern Matching for Mathematical Expressions with OpenMath (short paper)
Exploring proof autoformalization with Mistral on Herald
A Tough Nut for Mathematical Knowledge Management
Advantages and Dangers on Utilizing GeoGebra Automated Reasoning Tools
A Theoretical Analysis of Hierarchical Proofs
Joint Proceedings of the MathUI, OpenMath, PLMMS and ThEdu Workshops and Work in Progress at CICM, Bath, UK
Towards Mechanized Mathematical Assistants, 14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 27-30, 2007, Proceedings
Formalization of Prime Representing Polynomial in Mizar (short paper)
Hammering Higher Order Set Theory
Teaching Linear Algebra in a Mechanized Mathematical Environment
Formal verification of the correctness of chosen algorithms in Mizar
Problems and Solutions for Markup for Mathematical Examples and Exercises
SC 2 : Satisfiability Checking Meets Symbolic Computation - (Project Paper)
Evolving MathHub for Tetrapodal Math
Mining State-Based Models from Proof Corpora
Parsing Texts and Checking Proofs in LATEX
Partial Proof Terms in the Study of Idealized Proof Search
Formalizing Physics: Automation, Presentation and Foundation Issues
Using MathML to Represent Units of Measurement for Improved Ontology Alignment
Classification of Alignments Between Concepts of Formal Mathematical Systems
Detecting Unknots via Equational Reasoning, I: Exploration
Formalizing Finite Ramsey Theory in Lean 4
The Formalization of Vickrey Auctions: A Comparison of Two Approaches in Isabelle and Theorema
Towards Formal Fault Tree Analysis Using Theorem Proving
Mathematics and the World Wide Web
Representation for Interactive Exercises
Scalar actions in Lean's mathlib (short paper)
Tree Neural Networks in HOL4
Unified Decomposition-Aggregation (UDA) Rules: Dynamic, Schematic, Novel Axioms
Math Literate Knowledge Management via Induced Material
Three Years of DLMF: Web, Math and Search
MDML: The Mathdoc Digital Mathematics Library
The eval Symbol for Axiomatising Variadic Functions
Towards Robust Hyperlinks for Web-Based Scholarly Communication
Search Interfaces for Mathematicians
The MMT API: A Generic MKM System
Reasoning with Concept Diagrams About Antipatterns in Ontologies
Towards an Implementation in LambdaProlog of the Two Level Minimalist Foundation (short paper)
Lurch: a word processor that can grade students' proofs
Adding an Abstraction Barrier to ZF Set Theory
The Mathematical Semantic Web
Enhancing ENIGMA Given Clause Guidance
Understanding Branch Cuts of Expressions
Vector Graphics through Category Theory
Extending E Prover with Similarity Based Clause Selection Strategies
Combined Decision Techniques for the Existential Theory of the Reals
A Universal Machine for Biform Theory Graphs
On Diagrammatic Representation of Mathematical Knowledge
Towards Math Terms Disambiguation Using Machine Learning
A System for Computing and Reasoning in Algebraic Topology
A Formalization of the Change of Variables Formula for Integrals in mathlib
A Review of Mathematical Knowledge Management
Towards a Universal Interface for Real-Time Mathematical Communication
Matching Concepts across HOL Libraries
System Description STEX3 - A LATEX-Based Ecosystem for Semantic/Active Mathematical Documents
Comparing Machine Learning Models to Choose the Variable Ordering for Cylindrical Algebraic Decomposition
Escaping the Trap of Too Precise Topic Queries
MathTools: An Open API for Convenient MathML Handling
Automated Symmetric Constructions in Discrete Geometry
An Exploration in the Space of Mathematical Knowledge
Developing Visualisations For Spreadsheet Formulae: Towards Increasing the Accessibility of Science, Technology, Engineering and Maths Subjects
Work in Progress: Reachability Analysis for Time-triggered Hybrid Systems, The Platoon Benchmark (short paper)
Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition
A Tale of Two Set Theories
An Expert System for the Flexible Processing of XML-Based Mathematical Knowledge in a PROLOG-Environment
Intelligent Computer Mathematics, 16th Symposium, Calculemus 2009, 8th International Conference, MKM 2009, Held as Part of CICM 2009, Grand Bend, Canada, July 6-12, 2009. Proceedings
Capturing Hiproofs in HOL Light
Stochastic Modelling of Scientific Terms Distribution in Publications
Visual Structure in Mathematical Expressions
Growing Mathlib: maintenance of a large scale mathematical library
GCD - A Case Study on Lucas-Interpretation
Tools for MML Environment Analysis
Leveraging Information Contained in Theory Presentations
Constructing Examples of Fuzzy Implications within the Mizar Mathematical Library
Short Introduction by Example to Coq and Formalising ZF ⊆ ZF ε in Coq
Computer Certified Efficient Exact Reals in Coq
Licensing the Mizar Mathematical Library
Towards Formula Translation using Recursive Neural Networks
10 Years Later: The Mathematics Subject Classification and Linked Open Data
Mizar Course in Logic and Set Theory
Graded Rings in Lean's Dependent Type Theory
TIP: Tons of Inductive Problems
Literate sources for content dictionaries
Structure Formation in Large Theories
Growing the Digital Repository of Mathematical Formulae with Generic Sources
Progress of Self-Archiving Within the DML Corpus, with a View Toward Community Dynamics
Supporting Maintenance of Formal Mathematics with Similarity Search
Interactive mathematical videos
Efficient Ambiguous Parsing of Mathematical Formulae
A Unifying Framework for Managing Conflict-laden Content
Chaining Extensionality Lemmas in Lean's Mathlib
Structural Similarity Search for Mathematics Retrieval
First Neural Conjecturing Datasets and Experiments
Formalising the Kruskal-Katona Theorem in Lean
Mathematical Knowledge Management, 5th International Conference, MKM 2006, Wokingham, UK, August 11-12, 2006, Proceedings
Spurious Disambiguation Error Detection
MathScheme: Project Description
A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method
Mechanical Explanation in "Systems that Explain Themselves"
Combining Refinement and Signal-Temporal Logic for Biological Systems
Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita
A Graph-Based Approach Towards Discerning Inherent Structures in a Digital Library of Formal Mathematics
Context Aware Calculation and Deduction
Narrative Structure of Mathematical Texts
Transformations of MML Database's Elements
Compensating the Computational Bias of Spreadsheets with MKM Techniques
Automated Improving of Proof Legibility in the Mizar System
Confidence Measures in Recognizing Handwritten Mathematical Symbols
Towards Semantic Markup of Mathematical Documents via User Interaction
Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings
Integrating Dynamic Geometry Software, Deduction Systems, and Theorem Repositories
Logic as a Path to Enlightenment (Work in Progress Report)
Understanding Scientific Documents with Synthetic Analysis on Mathematical Expressions and Natural Language
Dynamic User Interfaces via Incremental Knowledge Management
Classifying Differential Equations on the Web
Comparing Mathematical Provers
Formal Mathematics for the Masses (short paper)
System Description: A Semantics-Aware LaTeX-to-Office Converter
Problem Formulation for Truth-Table Invariant Cylindrical Algebraic Decomposition by Incremental Triangular Decomposition
Formal Dependability Modeling and Analysis: A Survey
Towards the Structure of Mathematical Proof
The Global Digital Mathematics Library and the International Mathematical Knowledge Trust
Extending Numeric Automation for Number Theory Formalizations in Mizar
A Web-Based Toolkit for Mathematical Word Processing Applications with Semantics
Nominal AC-Matching
Reasoning with Generic Cases in the Arithmetic of Abstract Matrices
A Mathematical Approach to Ontology Authoring and Documentation
Managing Informal Mathematical Knowledge: Techniques from Informal Logic
AutoMSC: Automatic Assignment of Mathematics Subject Classification Labels
The Categorial Type of OpenMath Objects
Semantic Enrichment of Mathematics via 'tooltips'
Rough Concept Analysis - Theory Development in the Mizar System
Enumeration of AG-Groupoids
ENIGMA: Efficient Learning-Based Inference Guiding Machine
Managing Digital Mathematical Discourse
Engineering Mathematical Knowledge
A Comparison of Equality in Computer Algebra and Correctness in Mathematical Pedagogy
Sequential decision problems, dependently-typed solutions
Formally Verifying Proofs for Algebraic Identities of Matrices
MMTTeX: Connecting Content and Narration-Oriented Document Formats
Another Look at Formal Mathematical Properties
What Might "Understand a Function" Mean?
OpenMathMap: Interaction
Formalization of Gambler's Ruin Problem (short paper)
Indexing and Retrieval in a Heterogeneous Formal Library
Mathematical Libraries as Proof Assistant Environments
CICM 2015 - Informal Work in Progress Proceedings, Washington, DC, USA, July 13-17, 2015
Simple Dataset for Proof Method Recommendation in Isabelle/HOL
Edition with Arabic mathematical notation
Textbook Mathematics in the Naproche-SAD System
Joint Proceedings of the CME-EI, FMM, CAAT, FVPS, M3SRD, OpenMath Workshops, Doctoral Program and Work in Progress at the Conference on Intelligent Computer Mathematics 2018 co-located with the 11th Conference on Intelligent Computer Mathematics (CICM 2018), Hagenberg, Austria, August 13-17, 2018
Conservative Retractions of Propositional Logic Theories by Means of Boolean Derivatives: Theoretical Foundations
A Plugin to Export Coq Libraries to XML
An Integrated Web Platform for the Mizar Mathematical Library
Which One Is Better: Presentation-Based or Content-Based Math Search?
Author Profile Pages in zbMATH - Improving Accuracy through User Interaction
A Lean-based Language for Teaching Proof in High School
Using the Isabelle Ontology Framework - Linking the Formal with the Informal
Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL
A Framework for Formal Reasoning about Geometrical Optics
Formula Collection Mobile Apps Realized by Teachers
The DeLiVerMATH Project - Text Analysis in Mathematics
Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings
Intuitive and Formal Representations: The Case of Matrices
Gröbner Bases - Theory Refinement in the Mizar System
Hall's Theorem for Enumerable Families of Finite Sets
Automated Reasoning Service for HOL Light
Mathematical Knowledge Management, Second International Conference, MKM 2003, Bertinoro, Italy, February 16-18, 2003, Proceedings