Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing

M. Fareed Arif, Carlos Mencía, Joao Marques-Silva

The enumeration of minimal unsatisfiable subsets (MUSes) finds a growing number of practical applications, that includes a wide range of diagnosis problems. As a concrete example,…