### Abstract

In this work we formalise the isomorphism between simplicial complexes of dimension $n$ and monotone Boolean functions in $n$ variables, mainly following the definitions and results as introduced by N. A. Scoville. We also take advantage of the AFP representation of ROBDD (Reduced Ordered Binary Decision Diagrams) to compute the ROBDD representation of a given simplicial complex (by means of the isomorphism to Boolean functions). Some examples of simplicial complexes and associated Boolean functions are also presented.

### License

BSD License

### Topics

- Mathematics/Topology

### Session Simplicial_complexes_and_boolean_functions

- Boolean_functions
- Simplicial_complex
- Bij_betw_simplicial_complex_bool_func
- MkIfex
- Evasive
- ListLexorder
- BDD
- Binary_operations

### Depends on

- Matrices, Jordan Normal Forms, and Spectral Radius Theory
- Algorithms for Reduced Ordered Binary Decision Diagrams
- The Imperative Refinement Framework

## Cite

×

Simplicial_complexes_and_boolean_functions-AFP

    @article{Simplicial_complexes_and_boolean_functions-AFP,
      author  = {Jesús Aransay and Alejandro del Campo and Julius Michaelis},
      title   = {Simplicial Complexes and Boolean functions},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Simplicial_complexes_and_boolean_functions.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Dec 13, 2021 : Isabelle2021