Titlebook: Intelligent Computer Mathematics; 13th International C Christoph Benzmüller,Bruce Miller Conference proceedings 2020 Springer Nature Switze

细微的差异

Representing Structural Language Features in Formal Meta-languages challenge when representing languages in meta-languages such as standard formats like . or logical frameworks like .. It is desirable to use shallow representations where a structural language feature is represented by the analogous feature of the meta-language, but the richness of structural langu

maverick

Formally Verifying Proofs for Algebraic Identities of Matricesexplicit algorithms relying on non-commutative Gröbner bases. We address not only verification, but also exploration and reasoning towards establishing new identities and even proving mathematical properties. Especially Gröbner-driven elimination theory navigates us to insightful conclusions. We pre

G-spot

granite

Maintaining a Library of Formal Mathematics entry for contributors and to lessen the burden of reviewing contributions, we have developed a number of tools for the library which check proof developments for subtle mistakes in the code and generate documentation suited for our varied audience.

镇痛剂

Conference proceedings 2020 Italy, in July 2020*..The 15 full papers, 1 invited paper and 2 abstracts of invited papers presented were carefully reviewed and selected from a total of 35 submissions. The papers focus on advances in automated theorem provers and formalization, computer algebra systems and their libraries, and a

琐事

未成熟

A Framework for Formal Dynamic Dependability Analysis Using HOL Theorem Provingly. In this paper, we describe recent developments towards this direction along with a roadmap on how to be able to develop a framework for formal reasoning support for DFTs, DRBDs and CTMCs in a higher-order-logic theorem prover.

带子

A Survey of Languages for Formalizing Mathematicsowledge, and language frameworks that allow building customized languages..We evaluate their advantages based on our experience in designing and applying languages and tools for formalizing mathematics. We reach the conclusion that no existing language is truly good enough yet and derive ideas for possible future improvements.

Accrue

Induction with Generalization in Superposition Reasoningners automating induction. We demonstrate the strength of our technique by showing that many interesting mathematical properties of natural numbers and lists can be proved automatically using this extension.

Malaise

Formalizing Graph Trail Properties in Isabelle/HOLry library of Isabelle/HOL with an algorithm computing the length of a longest strictly decreasing graph trail starting from a vertex for a given weight distribution, and prove that any decreasing trail is also an increasing one.