Call hets/prove multiple times with different provers

ontohub / ontohub

A web-based repository for distributed ontologies.

GNU Affero General Public License v3.0

32 stars 8 forks source link

Call hets/prove multiple times with different provers #1132

Open eugenk opened 9 years ago

eugenk commented 9 years ago

Run multiple provers simultaneously with a short timeout to get most out of them.

Sascha Böhme and Tobias Nipkow analyzed the behavior of the automated theorem provers SPASS, eProver and Vampire in their paper "Sledgehammer: Judgement Day". The found out:

Running all 3 ATPs together for 5s yields the same success rate (44%) as running the most effective one for 120s. Therefore Sledgehammer now calls all 3 ATPs concurrently.

Do the same thing.

tillmo commented 9 years ago

If enough servers are availabe, we can also run more than 3 ATP instances concurrently. We could also try several instances of the same ATP with different flags and/or different axiom sets.

eugenk commented 9 years ago

Parallel execution is basically implemented with #1411. The only thing left to do is creating several Hets instances and sidekiq workers. Also some load balancing accross those workers would be nice.