search

spechub / Hets

The Heterogeneous Tool Set
http://hets.eu
GNU General Public License v2.0
57 stars 19 forks source link

User Feedback: The choice of reasoners and translations on rest.hets.eu is a nightmare #1959

Open fabianneuhaus opened 4 years ago

fabianneuhaus commented 4 years ago

This is not an issue per se, but rather user feedback + a proposal how to solve some major problems.

Imagine you are a new user of Hets and assume you want to prove some conjecture for a Common Logic ontology using the rest.hets.eu interface (or on your local Docker installation). The interfaces on rest.hets.eu forces you to make two choices (a) the reasoner and (b) a translation or rather a chain of translations. Nothing on the page tells you is that not every choice of translation works for every reasoner. Indeed what you don't know is that every reasoner accepts only one input language. And since there are many different translation-chains that produce different languages as output, chances that you choose the wrong chain of translations are high. Obviously Hets knows what input formats each reasoner expects, but instead of making this information available to you, it makes you guess or just try all possibilities until the right one is found. That's a very frustrating experience.

This frustration is not really limited to new users. For example, even after years of using Hets, I have yet not made Vampire work, because I haven't found the magic combinations of translations that would allow me to use it. (And I could not be bothered to do an exhaustive search.) Another example: E has two entries "EProver" and "eprover". For years I just thought that Eprover doesn't work at all, until Till told me that for some obscure reason "EProver" and "eprover" are associated with input format. First of all, how is a user expect to know that? And, secondly, even knowing that it is a continuous cause of frustration, since I regularly guess wrong. Why not at least call one "Eprover_TPTP" and the other "Eprover_SoftFOL"? What's the point of having both options anyway? As a user I just want to use one that works.

Currently, in the scenario described above Hets shows 20 different options for the choice of translation. Any user who looks at this is lost and overwhelmed. The brave might try one or two combinations, likely fail, and afterward conclude that Hets does not work. This is a shame, since the apparent complexity is just an artefact of a poor interface design. With some simple heuristics the user could be guided to a correct choice.

First of all, if a prover is chosen, the GUI should display only chains of translations that lead to the appropriate output format. Secondly, the GUI should automatically use the least expressive input format (e.g., CLFOL< CLSeq < CLFull). Lastly, if more than one chain of translations lead to the desired output format, it should by default show only the most direct options (= least number of intermediary theories). With these simple heuristics, there will be typically only one option left.

fabianneuhaus commented 4 years ago

PS: Another thing that is confusing: Names like CLSeq2CFOL:CASL2TPTP_FOF are not helpful at all. Some users might be able to guess that Hets uses chains of translations. But in this case one would expect that the output of the first translation matches the input of the second translation. There is nothing in the name "CFOL" that would allow the user to guess that it would work as input for a CASL2TPTP_FOL translation.

mcodescu commented 4 years ago

1922 already suggests that SoftFOL should be dropped, and then we no longer have duplicated provers. I would do that only after #1924 is solved, otherwise we don't have consistency checkers. I will work on #1924 as soon as we make more progress with fixing OWL and its provers.

But I couldn't get Vampire to run via rest.hets.eu for a very simple CASL theory either.

tillmo commented 4 years ago

These problems are long known. We need good heuristics for selecting translations and provers, see #417, and a better selection mechanism, see #336. We should announce this as a thesis topic.

fabianneuhaus commented 4 years ago

I don't think that this requires research, not even on a master level. The 3 dumb heuristics I listed above would solve the problem in the vast majority of cases. And these heuristics do not even need to be handled by Hets, this could just be done by the GUI, which hides the selection options for the normal users (maybe with an "advanced" option for people who want to do things manually).

mcodescu commented 4 years ago

Perhaps we should extend the default prover for a logic to a default prover for a sublogic. This would already be an improvement.

jvschroeder commented 4 years ago

It has been a while since I worked on HETS as a student assistant, but the following might be relevant: As mentioned in the user guide https://github.com/spechub/Hets/blob/5a71e7868023ec9dbfd579157fece803263b298f/doc/UserGuide.tex#L1587 the GUI allows for automatic selection of the comorphism for a prover. For this purpose I wrote some code (which can probably best be used through https://github.com/spechub/Hets/blob/6e348cf1439209682c1ba053d50f1a52fa291420/Proofs/AbstractState.hs#L459) that basically goes through the logic graph and finds the "shortest" comorphism path from the "current" (sub)logic to the desired provers' (sub)logic. For reference: The actual algorithm is in https://github.com/spechub/Hets/blob/master/Common/GraphAlgo.hs - I am not sure if any of this is relevant, but I thought there is no harm in mentioning it.