The resolution calculus

Bibliographic Information

The resolution calculus

Alexander Leitsch

(Texts in theoretical computer science, An EATCS series)

Springer, c1997

Available at  / 30 libraries

Search this Book/Journal

Note

Includes bibliographical references and index

With 36 figures

Description and Table of Contents

Description

This is a completely new presentation of resolution as a logical calculus and as a basis for computational algorithms and decision procedures. The first part deals with the traditional topics (Herbrand's theorem, completeness of resolution, refinements and deletion) but with many new features and concepts like normalization of clauses, resolution operators and search complexity. The second part gives a systematic treatment of recent research topics. It is shown how resolution decision procedures can be applied to solve the decision problem for some important first-order classes. The complexity of resolution is analyzed in terms of Herbrand complexity, new concepts are used to classify the complexity of refinements, and functional extension is introduced with resolution to give a strong calculus.

by "Nielsen BookData"

Related Books: 1-1 of 1

Details

  • NCID
    BA29530994
  • ISBN
    • 3540618821
  • Country Code
    gw
  • Title Language Code
    eng
  • Text Language Code
    eng
  • Place of Publication
    Berlin
  • Pages/Volumes
    viii, 300 p.
  • Size
    24 cm
  • Parent Bibliography ID
Page Top