insertion

insertion

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.