Skip to content

Lean4 Formalization of Jürg Kohlas' Information Algebra Book (and Shafer and Shenoy 1991)

Notifications You must be signed in to change notification settings

extradosages/information-algebra

Repository files navigation

A Formalization of Jürg Kohlas' Information Algebra

Overview

This repository represents a formalization of Jürg Kohlas' Information Algebra text in Lean4.

The work has also kind of bled out into Shafer and Shenoy's Local Computation in Hypertrees which is rich and from which Kohlas' text draws a lot of its concrete foundations.

It is an opportunity to learn about both formalization in Lean4 and about the contents of the texts.

Progress

This is a work-in-progress; right now I'm still on Chapter 2 in both Kohlas and Shafer and Shenoy.

About

Lean4 Formalization of Jürg Kohlas' Information Algebra Book (and Shafer and Shenoy 1991)

Resources

Stars

Watchers

Forks

Languages