ACM Transactions on Computational Logic

In this article, we introduce a notion of backdoors to Reiter’s propositional default logic and study structural properties of it. Also we consider the problems of backdoor detection (parameterised by the solution size) as well as backdoor evaluation (...

Generalization techniques have many applications, including template construction, argument generalization, and indexing. Modern interactive provers can exploit advancement in generalization methods over expressive type theories to further develop proof ...