Overview

Full Product Details

Author:   M. Laudet ,  D. Lacombe ,  L. Nolin ,  M. Schützenberger
Publisher:   Springer-Verlag Berlin and Heidelberg GmbH & Co. KG
Imprint:   Springer-Verlag Berlin and Heidelberg GmbH & Co. K
Edition:   1970 ed.
Volume:   125
Dimensions:   Width: 15.50cm , Height: 1.70cm , Length: 23.50cm
Weight:   1.000kg
ISBN:  

9783540049142

ISBN 10:   3540049142
Pages:   310
Publication Date:   01 January 1970
Audience:   Professional and scholarly ,  Professional & Vocational
Format:   Paperback
Publisher's Status:   Active
Availability:   In Print  
This item will be ordered in for you from one of our suppliers. Upon receipt, we will promptly dispatch it out to you. For in store availability, please contact us.

Table of Contents

Allocution d'ouverture.- Presentation d'un langage de formalisation des demonstrations mathematiques naturelles.- The mathematical language AUTOMATH, its usage, and some of its extensions.- Proof theory and the accuracy of computations.- Aspects du Theoreme de completude selon Herbrand.- Decision procedure for theories categorical in Alefo.- On the long-range prospects of automatic theorem-proving.- The case for using equality axioms in automatic demonstration.- Hilbert's programme and the search for automatic proof procedures.- A linear format for resolution.- Refinement theorems in resolution theory.- Definitional approach to automatic demonstration.- Heuristic interest of using metatheorems.- A proof procedure with matrix reduction.- Axiom systems in automatic theorem proving.- Constructive validity.- Paramodulation and set of support.

Reviews

Author Information

Tab Content 6

Author Website:  

Customer Reviews

Recent Reviews

No review item found!

Add your own review!

Countries Available

All regions