Martin

I'm not sure if this is going to be useful - after all in set theory, everything is a set. To my knowledge, TLA+ does not define the inner structure...

I became curious and tried to define such an operator relative to a set of primitives ``` RECURSIVE DeepFlatten(_,_) DeepFlatten(S, Primitives) == FoldSet(LAMBDA x,y : LET rx == IF x...

I always avoided mutable state because the parser may backtrack. I haven't found a good way to get around this yet.

Cutting reduces the expressiveness of the parser, are the grammars all in the non-backtracking fragment?

Imagine a rule ( a ~!~b ) | c - if I see it correctly, then c will not be tried when b fails, since that branch has been cut...

I believe the cut is safe for whole `thf( ... ).`, I think binders can also be realized (the bound variable is first parsed as a string and only converted...

When it comes to quantifier reasoning, I think Haniel would be the contact on the veriT side - as far as I remember, he was working on improving the proof...

iProver proofs are certainly sometimes incomplete (there are outputs from the CASC competition 2018 that have an incomplete DAG as well). Konstantin is aware of the problem but I don't...

I just saw this report open - on my machine with the latest development version, I can not prove BuggyTheorem although I have not checked if I can reproduce the...