, G. Amati 1 , LC. Aiello 2 and D. Gabbay 3 F. Pirri 2 , 1Fondazione Ugo Bordoni, via Baldassarre Castiglione 59, 00142 Rome, Italy and 2Dipartimento di Informatica e Sistemistica, Universita di Roma 'La Sapienza', via Salaria 113, 00198 Rome, Italy 3Department of Computing, Imperial College of Science, Technology and Medicine, 180 Queen's Gate, LondonSW1 2BZ, UK
We present a general proof theoretical methodology for default systems. Given a default theory <
W, D>, the default rules Dare simply understood as restrictions on the tableaux construction of the logic. Different default approaches have their own way of understanding these restrictions and executing them. For each default approach (such as Reiter, Brewka or Lukaszewicz), the allowable default extensions can be obtained from the default tableau construction. The advantage of our approach, besides being simple and neat, is in its generality: it allows for the development of a default theory for any logic with a tableau formulation, such as intuitionistic logic, linear logic or modal logic. Default systems, tableau systems, modal logic.
Part of the OUP Journal of Logic and Computation WWW service
Click here to register with OUP.
This page is maintained by OUP admin
Last updated 15 Jul 96
Part of the OUP Journals World Wide Web service.
Copyright Oxford University Press, 1996