Modal provability foundations for logical failure, with illustration in argumentation networks

Dov Gabbay

ABSTRACT

Any proof theory for a logic must contain the notion of finite failure
when it is clear the proof cannot go on for lack of applicable
rules. One can bring this notion into the object level by adding a
procedural failure connective to the language enabling it to say in
the object level what to do next (for example negation as failure
added to horn clause logic).  The question is, given such a database,
how can we characterise its logical content? Answer: as fixed points
in the modal logic of of provability based on the original logic. We
work this out for the logic of argumentation networks.