A new heuristic to filter nodes was added. Now if a literal is repeated (with the same sign) in a node the heuristic does not allow to choose that node for splitting.
A bug in Contraction constructor was detected and fixed
A bug in the method that checked sequents inclusion in a set modulus a substitution was detected and the method was re-implemented from scratch.
Experimentation still shows imperfections as some proofs still fail raising an exception.
ceilican
commented
8 years ago
A new heuristic to filter nodes was added. Now if a literal is repeated (with the same sign) in a node the heuristic does not allow to choose that node for splitting. A bug in Contraction constructor was detected and fixed A bug in the method that checked sequents inclusion in a set modulus a substitution was detected and the method was re-implemented from scratch. Experimentation still shows imperfections as some proofs still fail raising an exception.