We made two big changes to the code of OOPS, we added/changed two classes; ConfigurableProver and ConfigurableModel. These allow for changing the axiom system instead of using only the S5 model. Also we have chosen for a more dynamic approach for creating the axiom schemes instead of building new classes for every axiom scheme we only have two classes for creating the models.

All of the axioms are defined in the ConfigurableProver class. Where each axiom scheme is buildup with a set of rules and relation constrains. This makes it easier to add new axiom schemes.

In the ConfigurableModel class the relations ( reflexive, transitive, …,  etc. ) can be added to a model separately from each other. This makes it easier to make new axiom system, where only the corresponding relations have to be selected.

The current relations modeled in OOPS are transitive, reflexive, symmetric and serial.

Each relation can be added to an axiom system separately making it easier to add the relations to an axiom scheme.

The serial relation has been added to the old OOPS version because it is required by the D axiom system. The other relations (transitive, reflexive and symmetric) where already modeled and only had to be separated to make it possible for a more dynamic approach for creating axiom systems.

A serial relation means that every world in the model needs to have outgoing arrows for every agent. The model checks for every world if it has an outgoing arrow, if it doesn’t a new arrow is added to the world pointing to itself. By doing this for every world in the model the model becomes serial.