Abstract
In this chapter we introduce two key notions of our theory of resolution proof systems: the notion of a propositional resolution proof system and the notion of a propositional resolution logic. Resolution proof systems studied in this book are deductive proof systems that are based on the non-clausal form of the resolution principle, i.e., formulas which are involved in the resolution based deductive process are not assumed to be in any special ‘normal form’. Neither the relation between classical and non-classical automated proof methods nor the problem of ‘clausal’ versus ‘non-clausal’ proof procedures will be discussed in depth in this book. For the discussion on these and related topics the reader is referred to [19, 73, 75].
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1996 Kluwer Academic Publishers
About this chapter
Cite this chapter
Stachniak, Z. (1996). Propositional Resolution Proof Systems. In: Resolution Proof Systems. Automated Reasoning Series, vol 4. Springer, Dordrecht. https://doi.org/10.1007/978-94-009-1677-7_2
Download citation
DOI: https://doi.org/10.1007/978-94-009-1677-7_2
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-010-7251-9
Online ISBN: 978-94-009-1677-7
eBook Packages: Springer Book Archive