Let's COMPIT - Introduction

COMPIT

Let's COMPIT

A method for COMParing Indexing Techniques for automated deduction

What is Compit ?

If you use automated deduction for your application, you probably use some kind of indexing technique for terms. This technique may even be crucial to the efficiency of your program. But do you know how efficient it really is? Compared to others?

If you are an implementor and you need to know which indexing technique is likely to behave best for your application, or if you are a developer of new indexing techniques, you need to be able to compare techniques in order to get intuition about where to search for improvements, and in order to provide scientific evidence of the superiority of new techniques over other previous ones.

Are you sure your implementation works error free?
If you are an implementor, you need to debug your implementation. Why not use COMPIT for this and solve several problems in one step?
See our tutorial page for a use case.

Compit is a test-framework which allows you to compare indexing techniques for automated deduction. More on Compit you can find in the IJCAR paper "On the Evaluation of Indexing Techniques for Theorem Proving".
How to use Compit to compare your own indexing technique with the ones already included in the test-framework you can see on our tutorial page.

Indexing techniques already included in the testing framework

COMPIT tackles the following indexing problems: retrieval of generalization (forward matching) and unification. It is intended to cope with instances (backward matching) soon.

The following indexing techniques are already included in the framework:

Code Trees as implemented in the Vampire Prover
Context Trees, as decribed in this IJCAR paper
Discrimination Trees as implemented in the Waldmeister prover

Statistics on experiments currently available

Useful if you want to compare the efficiency of your indexing technique with others. The currently most up-to-date results of efficiency tests in the COMPIT framework are the ones given on the statistics page.

Downloads

From our download page, you can get the benchmark files that where used for the Compit testing framework.
Or learn how to make benchmarks for use with the test framework and how to test your own indexing technique implementation with the framework.

Robert Nieuwenhuis
Thomas Hillenbrand

revised and supplemented for the WWW by Doris Diedrich