A graph library for Isabelle
type: Item
instance of: scholarly article
title: A graph library for Isabelle
zbMATH Open document ID: 1308.05055
author: Lars Noschinski
published in: Mathematics in Computer Science
publication date: 2015-03-25T00:00:00Z
Mathematics Subject Classification ID: 05C20
Mathematics Subject Classification ID: 05C45
zbMATH DE Number: 6419296
zbMATH Keywords: graph theory
zbMATH Keywords: Isabelle
zbMATH Keywords: HOL
zbMATH Keywords: Euler
zbMATH Keywords: Kuratowski
describes a project that uses: Isabelle/HOL
describes a project that uses: Graph Theory
describes a project that uses: NASA PVS
describes a project that uses: CAVA LTL Modelchecker
describes a project that uses: ACL2
describes a project that uses: Isabelle
describes a project that uses: HOL
describes a project that uses: Locales
describes a project that uses: Flyspeck
describes a project that uses: AutoCorres
describes a project that uses: Tame Graphs
describes a project that uses: LEDA
describes a project that uses: Dijkstra Shortest Path
MaRDI profile type: Publication
full work available at URL: s11786-014-0183-z
OpenAlex ID: W2044116584
cites work: A framework for the verification of certifying computations
cites work: Locales: a module system for mathematical theories
cites work: Digraphs
cites work: Q3577833
cites work: Q4044590
cites work: Meta Reasoning in ACL2
cites work: Q4702188
cites work: Flyspeck I: Tame Graphs
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Q4862678
DOI: 10.1007/S11786-014-0183-Z
description: scientific article; zbMATH DE number 6419296