CICM 2022: 15TH CONFERENCE ON INTELLIGENT COMPUTER MATHEMATICS

A
Abraham, Erika	Experiments with Automated Reasoning in the Class SMT solving for Arithmetic Theories
Ayala-Rincón, Mauricio	Hall's Theorem for Enumerable Families of Finite Sets (Online Talk)
B
Berčič, Katja	Making the Census of Cubic Vertex Transitive Graphs searchable and FAIR (Online Talk)
Bhayat, Ahmed	Lemmaless Induction in Trace Logic (Online Talk)
Bordg, Anthony	A Parallel Corpus for Natural Language Machine Translation to Isabelle
Bundy, Alan	Decomposition Rules: Dynamic, Schematic, Novel Axioms (Online Talk)
C
Chugh, Abhishek	Sophize Mathematics Library (Online talk)
D
de Lima, Thaynara Arielly	Hall's Theorem for Enumerable Families of Finite Sets (Online Talk)
De Lon, Adrian	Setting up Set-theoretical Foundations in Naproche
Deniz, Elif	Formalization of Partial Differential Equations in HOL On the Formalization of the Heat Conduction Problem in HOL
Dramnesc, Isabela	Experiments with Automated Reasoning in the Class
Dunne, Ciaran	Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories
E
Einarsdóttir, Sólrún Halla	LOL: A library of lemmas for data-driven conjecturing (Online talk)
Eisenhofer, Clemens	Lemmaless Induction in Trace Logic (Online Talk)
F
Fernandez, Maribel	Hierarchical Higher-Order Port-graph Rewriting as a Modelling Tool
Fernandez Mir, Ramon	Verified Convex Optimization for Hybrid Systems
Ferreira Silva, Gabriel	Formalising Nominal AC-Unification (Online talk)
Fleuriot, Jacques	Re-imagining the Isabelle Archive of Formal Proofs (Online Talk)
Fuenmayor, David	Formalising Basic Topology for Computational Logic in Simple Type Theory (Online Talk)
Furushima, Hideharu	An Integrated Web Platform for the Mizar Mathematical Library (Online Talk)
G
Georgiou, Pamina	Lemmaless Induction in Trace Logic (Online Talk)
Ginev, Deyan	Welcome to ar5iv! Wrestling with the Open Problems of Scholarly Writing (Online Talk)
Gouëzel, Sébastien	Formalizing the change of variables formula for integrals in mathlib (Online Talk)
H
Hamel, Emma	An evaluation of NLP methods to extract mathematical token descriptors (Online Talk)
Hasan, Osman	On the Formalization of the Heat Conduction Problem in HOL
Hemaspaandra, Edith	Formal Methods for NFA Equivalence: QBFs, Witness Extraction, and Encoding Verification (Online Talk)
Huch, Fabian	Formal Entity Graphs as Complex Networks: Assessing Centrality Metrics of the Archive of Formal Proofs Re-imagining the Isabelle Archive of Formal Proofs (Online Talk)
Hůla, Jan	Targeted Configuration of SMT Solver (Online Talk)
J
Jakubův, Jan	Targeted Configuration of SMT Solver (Online Talk)
Janota, Mikoláš	Targeted Configuration of SMT Solver (Online Talk)
Jebelean, Tudor	Experiments with Automated Reasoning in the Class
Jeffrey, David	Working with Families of Inverse Functions
Johansson, Moa	LOL: A library of lemmas for data-driven conjecturing (Online talk)
K
Kani, Nickvash	An evaluation of NLP methods to extract mathematical token descriptors (Online Talk)
Kauers, Manuel	OuterCount: A First-Level Solution-Counter for Quantified Boolean Formulas (Online Talk)
Kieffer, Steve	PISE (Proofscape Integrated Study Environment) (Online talk)
Koepke, Peter	Setting up Set-theoretical Foundations in Naproche Web-Naproche
Kohlhase, Michael	OEIS Semantified -- A Tetrapodal Data Set System Description sTeX3 – A LaTeX-based Ecosystem for Semantic/Active Mathematical Documents Injecting Formal Mathematics Into LaTeX
Koprivec, Filip	Making the Census of Cubic Vertex Transitive Graphs searchable and FAIR (Online Talk)
Kosaian, Katherine	Formalizing Algorithms for Real Quantifier Elimination (Online Talk)
Kovacs, Laura	Lemmaless Induction in Trace Logic (Online Talk)
Kubej, Lukáš	Targeted Configuration of SMT Solver (Online Talk)
Kusper, Gabor	Experiments with Automated Reasoning in the Class
L
Lorenzen, Anton	Web-Naproche
M
MacKenzie, Carlin	Re-imagining the Isabelle Archive of Formal Proofs (Online Talk)
Mehta, Bhavik	Formalising the Kruskal-Katona theorem in Lean (Online talk)
Monnet, Sebastian	Formalising the Krull Topology in Lean (Online talk)
Möhle, Sibylle	OuterCount: A First-Level Solution-Counter for Quantified Boolean Formulas (Online Talk)
Müller, Dennis	System Description sTeX3 – A LaTeX-based Ecosystem for Semantic/Active Mathematical Documents Injecting Formal Mathematics Into LaTeX
N
Nakasho, Kazuhisa	An Integrated Web Platform for the Mizar Mathematical Library (Online Talk)
Narváez, David	Formal Methods for NFA Equivalence: QBFs, Witness Extraction, and Encoding Verification (Online Talk)
Nuamah, Kwabena	Decomposition Rules: Dynamic, Schematic, Novel Axioms (Online Talk)
P
Paulson, Lawrence	A Parallel Corpus for Natural Language Machine Translation to Isabelle Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis
R
Rabe, Florian	Case Studies on Realms (Online talk)
Rashid, Adnan	On the Formalization of the Heat Conduction Problem in HOL
Reger, Giles	Lemmaless Induction in Trace Logic (Online Talk)
S
Sardar, Muhammad Usama	Understanding Trust Assumptions for Attestation in Confidential Computing (Online talk)
Schütz, Marcel	Setting up Set-theoretical Foundations in Naproche
Seidl, Martina	OuterCount: A First-Level Solution-Counter for Quantified Boolean Formulas (Online Talk)
Serrano, Fabian	Formalising Basic Topology for Computational Logic in Simple Type Theory (Online Talk) Hall's Theorem for Enumerable Families of Finite Sets (Online Talk)
Shigenaka, Seigo	An Integrated Web Platform for the Mizar Mathematical Library (Online Talk)
Shminke, Boris	Python client for Isabelle server (System Entry)
Shukla, Ankit	OuterCount: A First-Level Solution-Counter for Quantified Boolean Formulas (Online Talk)
Smallbone, Nicholas	LOL: A library of lemmas for data-driven conjecturing (Online talk)
Stathopoulos, Yiannos	A Parallel Corpus for Natural Language Machine Translation to Isabelle
Stratulat, Sorin	Experiments with Automated Reasoning in the Class
T
Tahar, Sofiène	On the Formalization of the Heat Conduction Problem in HOL
V
Vaughan, James	Re-imagining the Isabelle Archive of Formal Proofs (Online Talk)
W
Wagner, Michael	OEIS Semantified -- A Tetrapodal Data Set
Wasaki, Katsumi	An Integrated Web Platform for the Mizar Mathematical Library (Online Talk)
Watt, Stephen	Working with Families of Inverse Functions
Weber, Franziska	Case Studies on Realms (Online talk)
Wells, Joe	Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories
Wieser, Eric	Graded rings in Lean's Dependent type theory (Online Talk)
Windsteiger, Wolfgang	Learning to Reason Assisted by Automated Reasoning (Online Talk)
Y
Yamamichi, Daichi	An Integrated Web Platform for the Mizar Mathematical Library (Online Talk)
Z
Zhang, Jujian	Graded rings in Lean's Dependent type theory (Online Talk)
Zheng, Hongbo	An evaluation of NLP methods to extract mathematical token descriptors (Online Talk)

Disclaimer | Powered by EasyChair Smart Program