Labelled resolution for classical and non-classical logics

Studia Logica 59 (2):179-216 (1997)

Uwe Reyle
Universität Stuttgart
Dov Gabbay
Hebrew University of Jerusalem
Resolution is an effective deduction procedure for classical logic. There is no similar "resolution" system for non-classical logics (though there are various automated deduction systems). The paper presents resolution systems for intuistionistic predicate logic as well as for modal and temporal logics within the framework of labelled deductive systems. Whereas in classical predicate logic resolution is applied to literals, in our system resolution is applied to L(abelled) R(epresentation) S(tructures). Proofs are discovered by a refutation procedure defined on LRSs, that imposes a hierarchy on clause sets of such structures together with an inheritance discipline. This is a form of Theory Resolution. For intuitionistic logic these structures are called I(ntuitionistic) R(epresentation) S(tructures). Their hierarchical structure allows the restriction of unification of individual variables and/or constants without using Skolem functions. This structures must therefore be preserved when we consider other (non-modal) logics. Variations between different logics are captured by fine tuning of the inheritance properties of the hierarchy. For modal and temporal logics IRS's are extended to structures that represent worlds and/or times. This enables us to consider all kinds of combined logics.
Keywords Philosophy   Logic   Mathematical Logic and Foundations   Computational Linguistics
Categories (categorize this paper)
DOI 10.1023/A:1004952317276
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 46,148
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

Add more citations

Similar books and articles


Added to PP index

Total views
39 ( #230,361 of 2,285,426 )

Recent downloads (6 months)
1 ( #841,072 of 2,285,426 )

How can I increase my downloads?


My notes

Sign in to use this feature