On Induction Principles for Diamond-Free Partial Orders

Autor:	Ievgen Ivanov
Rok vydání:	2021
Předmět:	TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Software Generalization Computer science business.industry Proof assistant Calculus engineering Diamond engineering.material Formal methods business
Zdroj:	Information and Communication Technologies in Education, Research, and Industrial Applications ISBN: 9783030775919 ICTERI (Revised Selected Papers)
DOI:	10.1007/978-3-030-77592-6_8
Popis:	We propose a formulation of an induction principle for diamond-free partial orders, which can be considered as a generalization of one of the variants of the real induction principle. This principle may be useful for specification and verification of non-discrete systems using interactive proof assistant software. As an example, a formalization in Isabelle proof assistant is presented.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::c7ea2c40aecc4c39329d692e2c88fc73 https://doi.org/10.1007/978-3-030-77592-6_8 Zobrazit plný text záznamu