Kluwer Academic Publishers (1996)
ISBN 0-7923-4017-5
This book introduces an algebraic framework for defining and analyzing
resolution-based automated reasoning systems for a range of non-classical
logics. It provides an algebraic theory of resolution proof systems,
focusing on proof theory, representation, and the efficiency of deductive processes.
A new class of logical calculi, the resolution logics, emerges as the
second theme of the book. The logical and computational aspects of the
relationship between resolution logics and resolution proof systems are explored
in the context of monotonic as well as nonmonotonic reasoning.
This book targets primarily researchers and graduate students in Artificial Intelligence, Symbolic Logic, and Computational Logic. The content serves as both a reference for researchers and a textbook for graduate courses focusing on the theoretical aspects of Automated Reasoning and Computational Logic.
Contents
Preface
1 LOGICAL PRELIMINARIES
1.1 Logical Systems
1.2 Refutational Principle
1.3 Propositional Logics - Syntax
1.4 Propositional Logics - Semantics
1.5 Semantic Trees
1.6 First-Order Logics
1.7 Herbrand's Theorem
2 PROPOSITIONAL RESOLUTION PROOF SYSTEMS
2.1 Resolution Principle
2.2 Resolution Proof Systems
2.3 Deductive Process
2.4 Resolution Logics
2.5 Resolving Upon Subformulas
2.6 Strong Resolution Counterparts
3 PROPOSITIONAL RESOLUTION LOGICS
3.1 Matrices Induced by Resolution Proof Systems
3.2 Characterization of Resolution Logics
3.3 Disjunctive Resolution Logics
3.4 Relative Soundness of the Resolution Rule
3.5 Lattices of Resolution Logics
4 EFFICIENCY OF THE DEDUCTIVE PROCESS
4.1 Minimal Resolution Counterparts
4.2 Verifier Degrees of Resolution Logics
4.3 Minimal Resolution Counterparts of Lukasiewicz
Logics
4.4 Simplification of the Resolution Rule
4.5 Simplification of the Termination Test
5 THEOREM PROVING STRATEGIES
5.1 Set of Support Strategy
5.2 Polarity Strategy
5.3 Operator Polarity
5.4 Unrestricted Polarity
5.5 Verifier Polarity
5.6 Strengthening the Polarity Strategy
5.7 Polarity and the Simplification of Resolvents
5.8 Polarity and the Deductive Process
5.9 Test Results
6 RESOLUTION CIRCUITS
6.1 Propositional AND-OR Circuits
7 FIRST-ORDER RESOLUTION PROOF SYSTEMS
7.1 Unification
7.2 Resolution Counterparts of FFO Logics
7.3 Existence of Resolution Counterparts
7.4 Theorem Proving Strategies
7.5 Resolution Circuits for FFO Logics
8 NONMONOTONIC RESOLUTION INFERENCE SYSTEMS
8.1 Cumulative Inference Systems
8.2 Preferential Matrices
8.3 Monotone Bases of Inference Operations
8.4 Consistency Preservation
A RESOLUTION COUNTERPART Rs_2 of P_2
B RESOLUTION COUNTERPART Rs_3 of P_3
C RESOLUTION COUNTERPART Rs_4 of P_4
D RESOLUTION COUNTERPART Rs_5 of P_5
E RESOLUTION COUNTERPART Rs_3* of P_3*
F RESOLUTION COUNTERPART Rs_3^s of P_3^s
See errata.
|
ZBIGNIEW STACHNIAK
