Known Bugs

Saturate is a prototype that we use to try out some of our theoretical ideas. Many things should be improved, above all, speed. Certainly, Saturate contains bugs that we haven't found yet. There is no correctness guarantee whatsover that we can provide with this system and no liability can be assumed in any regard.

The following list describes bugs that are related to certain implementation issues.

Reflexive closure declarations should be made only for strict total orderings. This is not checked. For other transitive relations it may result in cross incompleteness of the prover.

Certain Prolog-operators, in particular [_ |_ ], ``not'' and ``:'' should not appear as function symbols in clauses. Otherwise many things could go wrong. This is not checked.

Imprint | Data Protection