## Resolution Proof Systems: An Algebraic TheoryResolution Proof Systems: An Algebraic Theory presents a new algebraic framework for the design and analysis of resolution- based automated reasoning systems for a range of non-classical logics. It develops an algebraic theory of resolution proof systems focusing on the problems of proof theory, representation and efficiency of the deductive process. A new class of logical calculi, the class of resolution logics, emerges as a second theme of the book. The logical and computational aspects of the relationship between resolution logics and resolution proof systems is explored in the context of monotonic as well as nonmonotonic reasoning. This book is aimed primarily at researchers and graduate students in artificial intelligence, symbolic and computational logic. The material is suitable as a reference book for researchers and as a text book for graduate courses on the theoretical aspects of automated reasoning and computational logic. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

LOGICAL PRELIMINARIES | 1 |

PROPOSITIONAL RESOLUTION PROOF | 23 |

PROPOSITIONAL RESOLUTION LOGICS | 47 |

Copyright | |

9 other sections not shown

### Other editions - View all

### Common terms and phrases

3-valued Lukasiewicz algebra algorithm AND-OR resolution circuit atomic formulas automated reasoning classical propositional logic Cm(X consistency status constant symbols constructed cumulative inference systems deduced set deductive process defined as follows designated truth-values Example finite and clean finite set first-order resolution Hence Herbrand's Theorem Hom(C implies inconsistent sets inference rules interpretation substitution Lemma let us assume Let X C L logic defined logical matrix Lukasiewicz logic matrix induced maximal consistent maximal consistent set minimal resolution counterpart Moreover negative non-creative notion operator polarity pol2 polarity strategy polarity values poll positive preferential matrix proof of Theorem refutation tree replacing resolution logic resolution principle resolution proof system resolution rule resolvent Rver satisfies Section semantic tree sequence set of support set of verifiers sets of formulas strong resolution counterpart subformula t(Rs Theorem 7.7 transformation rules unrestricted polarity verifier polarity VerR X C L be finite