Following the line of research started in 1996, we have carried on the program of developing uniform and analytic proof-methods for the major families of nonmonotonic logics [10,12,13]. The program aims to achieve a presentation of every nonmonotonic formalism in terms of simple deduction rules, alternative to the rather complex semi-procedural constructions, and without any commitment to specific search strategies or implementational details. On the other hand, it is part of our project to show how many known deduction procedures can be efficiently simulated in our calculi. In this way, a variety of deduction procedures can be studied (and compared) as proof-search strategies in our calculi. Our proof methods have the neat form of sequent calculi, whose main features are that they are analytic, they comprise an axiomatic rejection method (in the form of a sequent calculi by itself), and that they make use of provability assumptions.
In 1997 [13], we have extended our approach to circumscription, which is one of the most important nonmonotonic formalism and we have shown that our method can polinomially simulate derivations in one of the most efficient tableaux methods which is known so far. In previous work [10,12], we succesfully applied our methodology to default logic and the normal fragment of brave (or credulous) autoepistemic logic. To complete our framework, we plan to extend it to full autoepistemic logic. Moreover, we have developed an extension of resolution for the skeptical stable model semantics of logic programs [11]. This method enjoys three novel features: