On Extracting Arguments in Favor of One Given Conclusion

An any-time approach to extract the deductive arguments in favor of a given conclusion from a set of formulas is proposed. Since the number of such arguments can be exponential in the worst-case, the approach focuses first on a series of arguments with mutually independent supports before it considers additional arguments. It is developed in the standard clausal Boolean framework and it is based on a refutation-like method that benefits from recent progress in the practical extraction of minimal unsatisfiable subsets of Boolean clauses.