Titlebook: Intelligent Computer Mathematics; 16th International C Catherine Dubois,Manfred Kerber Conference proceedings 2023 The Editor(s) (if applic

External-Otitis

书目名称Intelligent Computer Mathematics影响因子(影响力)




书目名称Intelligent Computer Mathematics影响因子(影响力)学科排名




书目名称Intelligent Computer Mathematics网络公开度




书目名称Intelligent Computer Mathematics网络公开度学科排名




书目名称Intelligent Computer Mathematics被引频次




书目名称Intelligent Computer Mathematics被引频次学科排名




书目名称Intelligent Computer Mathematics年度引用




书目名称Intelligent Computer Mathematics年度引用学科排名




书目名称Intelligent Computer Mathematics读者反馈




书目名称Intelligent Computer Mathematics读者反馈学科排名

小卷发

Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigationogical-investigations, we contribute to building an Isabelle category theory library, with a focus on ease of use in the formalization beyond category theory itself. This work paves the way for future formalizations based on category theory and demonstrates the power of automated reasoning in investigating meta-logical questions.

Overstate

Isabelle Formalisation of Original Representation Theoremsfication via Isabelle/HOL definitions and theorems, and exposes the technical challenges found in the process. The introduced formalisation completes the verification of Isabelle-verified event structure enumeration algorithms into a fully verified framework to link event structures to full graphs.

同来核对

Highlighting Named Entities in Input for Auto-formulation of Optimization Problemsnts an approach that converts linear programming word problems into mathematical formulations. We leverage the named entities in a problem description and augment the input to highlight these entities. Our approach achieves the highest accuracy among all submissions to the NL4Opt competition, securing first place in the generation track.

byline

Nominal AC-Matching of nominal atoms, permutations and abstractions. Furthermore, by adding a parameter for “protected variables” that cannot be instantiated during the execution, it enables nominal matching. Such a general treatment of protected variables also gives rise to a verified nominal AC-equality checker as a byproduct.

Pigeon

Morphism Equality in Theory Graphsin several elementary formalizations that critically require stating and proving certain non-trivial morphism equalities. The key difficulty of this approach is that important properties of theory graphs now become undecidable and require heuristic methods.

disciplined

Conference proceedings 2023 UK, in September 2023..The 14 full papers, 2 project/survey papers, 6 short papers, and 1 tool paper presented were carefully reviewed and selected from a total of 37 submissions. The papers focus on advances in formalization, automatic theorem proving and learning, search and classification, teach

Fibroid

放牧

Teaching Linear Algebra in a Mechanized Mathematical Environment Jupyter Notebooks, and some choices of topics that are especially suited to teaching with these tools. The discussion is informed by our experience over the past thirty or more years teaching at various levels, especially at the University of Western Ontario.

QUAIL

Conference proceedings 2023rom a total of 37 submissions. The papers focus on advances in formalization, automatic theorem proving and learning, search and classification, teaching and geometric reasoning, and logic and systems, among other topics..