Combining Proofs for Description Logic and Concrete Domain Reasoning

The 7th International Joint Conference on Rules and Reasoning 2023

Submission number 4819


This page provides supplementary material for the submission. Here you can find the following:

Getting Z3

As part of our experiments, we compare the performance of our tool with Z3 solver.
Before running the experiment, follow these steps to get Z3:

  1. Clone the Z3 repository (https://github.com/Z3Prover/z3)
  2. In the root directory of Z3, run the following:
    1. python scripts/mk_make.py --java
    2. cd build
    3. make
  3. After it is done, in the build directory, you should be able to find either:
    • libz3.so and libz3java.so,
    • or libz3.dylib and libz3java.dylib
    Which you need to copy to experiment/z3Lib.

Running the Experiment

Requirement: Java 8 (or Higher).
To run the experiment, first make sure that the user account you will use to run the experiment has no Java process running.
In experiment/, run 

 ./watcher.sh [your-user-name]
to start the experiment.

Using the Tool

If you want to try the tool without running the full experiment, you can run it as in the following example:

java -cp cd.jar de.tu_dresden.lat.App -o src/test/resources/scalable/cd1/diet/instances/diet1a.owl -c src/test/resources/scalable/cd1/diet/instances/diet1a.txt -a "<http://www.semanticweb.org/alisa/ontologies/2023/concrete-domain/diet#MyDayDiet> <= <http://www.semanticweb.org/alisa/ontologies/2023/concrete-domain/diet#Well-balanced>" -r Elk -cd linearConstraints

You can also add the following additional options: To enable Z3 tests for CD reasoning, you need to set "concrete-domain-reasoner.enableZ3Checks" to true (java -Dconcrete-domain-reasoner.enableZ3Checks=true -cp cd.jar de.tu_dresden.lat.App ...)