Closed lex-lex closed 5 years ago
@lex-lex Right now the assumptions are a list of strings, unlike the formalization which includes also the original text. I will make the autoAssumptions similar to formalization. Please tell me if the manual assumptions should be changed as well.
Well, it can't hurt to have also an explanation for each manually added assumption (for documentation purposes), so changing this to { formula: ..., description: ... } instead of just a string seems adequate to me. What do you think?
I agree, but it will break the current tool since it is not backward compatible. I suggest we add it after finishing this feature.
Seems plausible, agreed! :-)
I finished and pushed this feature but I am using autoAssumptions and autoGoal right now. The reason is again that goal is currently a string and not an object. Does it make sense to have a manual goal? I dont think so. We can try to coordinate the change of assumptions and goals to objects and then I will get rid of the autoGoal completely. What do you think?
Nope, I would simply remove the manual goal and put the "autoGoal" in goal
.
There are some existing queries though with a manual goal. I can copy the goal into autoGoal in case it is empty and you can use autoGoal only?
Sounds good if that works from the back-end side.
ok, done (hopefully as I dont have time to test it). Please reopen if you think it doesnt work.
Following our discussion, the queries will also be constructed by annotating text. So I propose to:
content
(just as in theory) for the editor text.autoAssumption
goal
.assumptions
is still used for manually added assumption.The annotation of goals in
content
could be:There the content
[...]
is annotated as usual, i.e. with nested connectives and terms.