Gabriel Ebner

It would also be an intuitive user interface to support google maps-like panning and zooming with the mouse.

This is strange. On the elements of `congr`, the function `lt` is both irreflexive and transitive. It's not necessary to use a term order here at all. To be honest,...

Yeah, splitting is not really supported in the back-translation. Can you try `eliminateSplitting` on the resolution proof first? We might want to add that call to `ErasureReductionCNF` then.

> [...] the parser may backtrack. I haven't found a good way to get around this yet. Ah, that's easy: you just make a cut, which prevents backtracking. In parboiled2...

I'm not sure what you mean precisely. However in TPTP files there is a very nice point to cut, namely after each TPTP_input production, i.e. a dot-delimited top-level form: ```...

Ah, I see what you mean. Of course, just replacing sequential composition with cutting composition everywhere changes the language the grammar accepts. In the TPTP case I think we can...

Have you tried this change on `LinearExampleProof(3)`? I think this is very nice for the prime proof, however it's probably not that pretty in general. For the LatexExporter I have...

This visual phenomenon is called "wobbling", see [this bug report for more details](https://github.com/gapt/gapt/issues/545).

There is actually an even easier encoding by adding assumptions to the atoms in the deep formula. Assume again for simplicity that all nodes have negative polarity. We compute the...

I don't think you can tell z3 to write everything on a single line. Unfortunately the parsing library we use for the s-expression parser does not allow us to resume...