عنوان

Resolution Proof Systems :

9400916779

9789400916777

b592686

Resolution Proof Systems :

[Book]

an Algebraic Theory

by Zbigniew Stachniak.

Dordrecht

Springer Netherlands

1996

(xvi, 207 pages)

Automated reasoning series, 4.

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?ukasiewicz 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 --; References --; Index of Symbols.

Resolution 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.

Algebra -- Data processing.

Artificial intelligence.

Computer science.

by Zbigniew Stachniak.

Zbigniew Stachniak

[Book]

Y