Debugging with Theorem prover

[Bart Bogaerts]

Often, typos in your theory will result in an inconsistent theory (trivially false).

A minimal set of contradicting sentences could be found (given a structure) by UNSAT core extraction, but the theorem prover might also discover this symbolically.

This way, we avoid the work of one-by-one commenting all sentences..

[Broes De Cat]

This would preferably be implemented in lua only, when we support selecting sentences from a theory.

[Ingmar Dasseville]

@jjansen thesisidee?