Installation requirements and usage instructions: README.md

This script is used to prove the relationship between two ontologies using theorem prover Prover9 and model builder Mace4.

The program starts by parsing and setting up the theories using the parse package, then goes to check consistency by searching for a model with axioms from each theory combined. If a model is not found, the program searches for a proof, for which if found, proves that the theories are inconsistent. If either process times out (i.e., Mace4 cannot find it in 10 models or Prover9 exceeds 30 seconds), the relationship is inconclusive.

The program then checks for entailment.

Used for all file related processes, including proof and model files that are generated as the relationship is checked between two theories. The user can opt-out for file generation.