Installation requirements and usage instructions:
README.md
insertion.py
The insertion algorithm implemented uses a depth-first search approach in a chain
decomposition to identify the correct location of where a theory should be added in
the hierarchy. A new theory T is inserted to a chain above T1 and below T2 iff
T1 is entailed by T and T2 entails T. Entailment and consistency are checked using
the relationship package.
construct.py
Used to repeat the insertion algorithm for all theories in a directory ending in ".in"
and create a new hierarchy, represented as a chain decomposition in a given .csv file.
remove_duplicate_chains.py
Used to remove duplicate chains that are found in a hierarchy during construction.
Chains are duplicates of each other iff one chain contains all theories contained in another.