This is a tool for computing all maximal contractions of a finite set of propositional formulas with respect to a consistent set of literals, i.e. atomic formulas or negations of atomic formulas. It is also capable of computing all minimal inconsistent subsets of a given finite set of propositional formulas. This tool can be used for inconsistent detection, assisting science discovery et al.


    Last update: November 14, 2012