Volume 6: January - December 1996

Issue 2: April 1996


A proof theoretical approach to default reasoning I: tableaux for default logic

  • A proof theoretical approach to default reasoning I: tableaux for default logic
  • G. Amati1, LC. Aiello2, D. Gabbay3 and F. Pirri2 1Fondazione Ugo Bordoni, via Baldassarre Castiglione 59, 00142 Rome, Italy, 2Dipartimento di Informatica e Sistemistica, Universita di Roma 'La Sapienza', via Salaria 113, 00198 Rome, Italy and 3Department of Computing, Imperial College of Science, Technology and Medicine, 180 Queen's Gate, London SW1 2BZ, UK


    We present a general proof theoretical methodology for default systems. Given a default theory <W, D>, the default rules D are 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.

    Keywords: Default systems, tableau systems, modal logic.

    Pages: 205 - 231

    Part of the OUP Journal of Logic and Computation WWW service

    General Information

    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