Automated Theorem Proving
1st Edition
Published on 1. January 1982
Book
Paperback/Softback
292 pages
978-3-528-08520-9 (ISBN)
Description
Among the dreams of mankind is the one dealing with the mecha nization of human thought. As the world today has become so complex that humans apparently fail to manage it properly with their intellectual gifts, the realization of this dream might be regarded even as something like a necessity. On the other hand, the incredible advances in computer technology let it appear as a real possibility. Of course, it is not easy to say what sort of thing human thinking actually is, a theme which over the centuries occupied many thinkers, mainly philosophers. From a critical point of view most of their theories were of a speculative nature since their only way of testing was by Gedanken-experi ments. It is the computer which has opened here a wide range of new possibilities since with this tool we now can model real experiments and thus test such theories like physicists do in their field. About a quarter of a century ago, scientific activi ties of that sort were started under the label of artificial intelligence Today these activities establish a wide and prosperous field which the author, in lack of any better name, prefers to call intellectics. Without any doubt, the com puter programs developed in this field have tought us much about the nature of human thinking.
More details
Language
German
Place of publication
Wiesbaden
Germany
Publishing group
Vieweg & Teubner
Target group
Professional and scholarly
Research
Illustrations
292 S.
Dimensions
Height: 244 mm
Width: 170 mm
Thickness: 17 mm
Weight
542 gr
ISBN-13
978-3-528-08520-9 (9783528085209)
DOI
10.1007/978-3-322-90100-2
Schweitzer Classification
Other editions
Additional editions
Wolfgang Bibel
Automated Theorem Proving
E-Book
03/2013
Vieweg+Teubner Verlag
€42.99
Available for download
Person
Prof. Dr. Wolfgang Bibel lehrt das Fachgebiet Intellektik am Fachbereich Informatik der TH Darmstadt. Dr. Steffen Hölldobler und Dr. Torsten Schaub sind wissenschaftliche Mitarbeiter am gleichen Fachbereich.
Content
I. Natural and formal logic.- 1. Logic abstracted from natural reasoning.- 2. Logical rules.- II. The connection method in propositional logic.- 1. The language of propositional logic.- 2. The semantics of propositional logic.- 3. A basic syntactic characterization of validity.- 4. The connection calculus.- 5. Consistency, completeness, and confluence.- 6. Algorithmic aspects.- 7. Exercises.- 8. Bibliographical and historical remarks.- III. The connection method in first-order logic.- 1. The language of first-order logic.- 2. The semantics of first-order logic.- 3. A basic syntactic characterization of validity.- 4. Transformation to normal form.- 5. Unification.- 6. The connection calculus.- 7. Algorithmic aspects.- 8. Exercises.- 9. Bibliographical and historical remarks.- IV. Variants and improvements.- 1. Resolution.- 2. Linear resolution and the connection method.- 3. On performance evaluation.- 4. Connection graph resolution and the connection method.- 5. A connection procedure for arbitrary matrices.- 6. Reduction, factorization, and tautological circuits.- 7. Logical calculi of natural deduction.- 8. An alternative for skolemization.- 9. Linear unification.- 10. Splitting by need.- 11. Summary and prospectus.- 12. Exercises.- 13. Bibliographical and historical remarks.- V. Applications and extensions.- 1. Structuring and processing knowledge.- 2. Programming and problem solving.- 3. The connection method with equality.- 4. Rewrite rules and generalized unification.- 5. The connection method with induction.- 6. The connection method in higher-order logic.- 7. Aspects of actual implementations.- 8. Omissions.- 9. Exercises.- 10. Bibliographical and historical remarks.- References.- List of Symbols.