Skip to content
Switch branches/tags
Go to file
Cannot retrieve contributors at this time

Sequences for learning Path Semantics

Reading sequences for learning path semantics.

This is a collection of papers organized in a way to build up gradually understanding of path semantics.
Some papers are marked with stars (e.g. ★★★★★) to signify their significance.

Cheat Sheets

Reference material



Normal paths are formalized in 5 different ways:

The proof in Lean 3 assumes satisfied models of total normal paths using semiconjugates. This is currently the best available model of normal paths in dependent types.

Each of these pictures can be used to reason about normal paths. However, there exists no exhausting set of axioms (this is currently believed to be an undecidable problem). For some theories, like Boolean functions, normal paths are proven to be sound by exhaustive proof search.

In the broader theory of logic, one can study Path Semantical Logic.

Path Semantical Logic

It is recommended to skip this section, unless you are interested in logic or the foundation of Path Semantics.

Path Semantical Logic uses the core axiom to group propositions into levels. An equality at level N+1 propagates into equality at level N. For an experimental implementation, see the Pocket-Prover library.



Higher Order Operator Overloading

Higher Order Operator Overloading (HOOO) is a way to extend the semantics of normal expressions into expressions for higher order reasoning.

Discrete Path Semantics

Boolean Path Semantics

Permutative Path Semantics

Examples of Path Semantics

Concepts in Path Semantics



Probabilistic Path Semantics

Examples of Probabilistic Path Semantics

Avatar Extensions

Summary of Avatar Extensions

Foundation of Avatar Logic: Avatar Logic to Set Theory ★★★★★

Avatar Extensions is a technique of abstract generalization by exploiting symmetries inside "smaller" theories. For an experimental implementation of Avatar Logic, see Avalog. For visualization of Avatar Graphs, see Avatar-Graph.

Proof Techniques

Sized Type Theory

MX Grammar for Dependent Types

Slot Lambda Calculus

Dual Number Monotonic Density

Cocyclic Graphs

Directional Set Algebra

Closed Natural Numbers

Asymmetric Velocity Logic

Answered Modal Logic


Artificial Intelligence

Moved to its own sequences page

Esoteric Path Semantics

Non-Deterministic Path Semantics