A Labelled Tableau Calculus for Nonmonotonic (Cumulative) Consequence Relations

Artosi, Alberto, Governatori, Guido and Rotolo, Antonino (2000). A Labelled Tableau Calculus for Nonmonotonic (Cumulative) Consequence Relations. In: Dyckhoff, Roy Tableaux 2000, St Andrews, Scotland, (82-97). Jul 03-07, 2000.

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads
Tab2000f.pdf Tab2000f.pdf application/pdf 189.60KB 537

Author Artosi, Alberto
Governatori, Guido
Rotolo, Antonino
Title of paper A Labelled Tableau Calculus for Nonmonotonic (Cumulative) Consequence Relations
Conference Paper Type Fully Published Paper
Conference name Tableaux 2000
Conference location St Andrews, Scotland
Conference dates Jul 03-07, 2000
Journal name Automated Reasoning with Analytic Tableaux and Related Methods   Check publisher's open access policy
Editor Dyckhoff, Roy
Publication date 2000-01-01
Volume number 1847
ISBN 3-540-67697-X
ISSN 0302-9743
Start page 82
End page 97
Total pages 16
Language eng
Abstract/Summary In this paper we present a labelled proof method for computing nonmonotonic consequence relations in a conditional logic setting. The method is based on the usual possible world semantics for conditional logic. The label formalism KEM, introduced to account for the semantics of normal modal logics, is easily adapted to the semantics of conditional logic by simply indexing labels with formulas. The inference rules are provided by the propositional system KE+ - a tableau-like analytic proof system devised to be used both as a refutation and a direct method of proof - enlarged with suitable elimination rules for the conditional connective. The resulting algorithmic framework is able to compute cumulative consequence relations in so far as they can be expressed as conditional implications.
Subjects 280403 Logics and Meanings of Programs
440106 Logic
280402 Mathematical Logic and Formal Languages
280000 Information, Computing and Communication Sciences
Keyword labelled tableaux
conditional logic
non-monotonic logic
cumulative consequence relations
automated theorem proving
Q-Index Code E1
Q-Index Status Provisional Code
Institutional Status Unknown
Additional Notes Copyright (c) 2000 Springer.

Document type: Conference Paper
Sub-type: Fully Published Paper
Collection: School of Information Technology and Electrical Engineering Publications
 
Versions
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 2 times in Thomson Reuters Web of Science Article | Citations
Google Scholar Search Google Scholar
Access Statistics: 211 Abstract Views, 537 File Downloads  -  Detailed Statistics
Created: Thu, 07 Apr 2005, 10:00:00 EST by Guido Governatori