Martin

Sort with LPO leads to Exception "Comparison method violates its general contract!"

1

I tried to have a look at expansion proof deskolemization for my nTapeX proofs. For the nTape2 variant, I get some errors I was looking to fix but when I...

Notebooks seem to be well recieved in the scientific community (e.g. for data-analysis). One of them is [Jupyter](https://try.jupyter.org/) which also has [Scala integration](https://github.com/alexarchambault/jupyter-scala). It might be worthwhile to use it...

The skolem quantifier rules in LKsk infer the skolem context from the current labels: ``` \Gamma :- P (s l1 ... ln) , \Delta --------------------------------------------------- all:r \Gamma :- \all x...