Open Research Index

On the Formalization of Network Topology Matrices in HOL

Kubra Aksoy, Adnan Rashid, Osman Hasan, Sofiene Tahar

arXivarxiv/2603.25682Mar 26, 2026cs.LOscore 0

Network topology matrices are algebraic representations of graphs that are widely used in modeling and analysis of various applications including electrical circuits, communication networks and transportation systems. In this paper, we propose to use Higher-Order-Logic (HOL) based interactive theorem proving to formalize network topology matrices. In particular, we formalize adjacency, degree, Laplacian and incidence matrices in the Isabelle/HOL proof assistant. Our formalization is based on modelling systems as networks using the notion of directed graphs (unweighted and weighted), where…

SourceJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/arxiv/2603.25682
curl -X POST /api/v1/records/arxiv/2603.25682/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2603.25682/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'