Witold Marciszewski and Roman Murawski
This survey is identical with the table of contents of the book by the same authors entitled Mechanization of Reasoning in a Historical Perspective, published by Editions Rodopi, Amsterdam 1995. The table is so detailed that that it can function as a distinct text (linked with with other ones in this issue), provided that it is introduced by the following comment.
The development of logic displays new and illuminating aspects when seen from the angle of mechanized reasoning. Even those who doubt in the use of logical theories as a guide for common sense or scientific research have to agree that they proved indispensable for producing reasoning machines. The story has three turning points which most concisely can be listed with the three following terms: formalization (started in the Middle Ages, appreciated and developed by Leibniz), algebraization (started by Leibniz and his contemporaries, accomplished by Boole at al), elimination of the quantifiers (Skolem, Hilbert, Gentzen et al) to reduce the whole of logic to its algebraized and finitistic part.
These results belong to the most significant in the history of Western civilization. Owing to formalization, a reasoning becomes a mere operation on symbols (not on thoughts!) as physical objects, and so turns manageable for a machine. Owing to algebraization and finitization, a reasoning can be carried out as a purely combinatorial, finitistic and syntactic procedure -- just of the kind perfectly suited to computers. Mechanized reasoning, in turn, is a starting point for artificial intelligence, hence it introduces that new era in which machines should incredibly advance the intellectual potential of humans. This is the course of events that looks as if ingeniously plotted by Genius of Evolution. The following table displays the main phases of the process and their components parts, up to some minute episodes; its first part (corresponding to Ch. 1) hints at some general ideas to introduce the historical narration.
1. FROM THE MECHANIZATION OF REASONING TO A STUDY OF HUMAN INTELLIGENCE
1.1. Von Neumann's project related to cognitive science
2. THE FORMALIZATION OF ARGUMENTS IN THE MIDDLE AGES
2.1. The contention of the present chapter
3. LEIBNIZ'S IDEA OF MECHANICAL REASONING AT THE HISTORICAL BACKGROUND
3.1. An interaction between logic and mathematics
4. BETWEEN LEIBNIZ AND BOOLE: TOWARDS THE ALGEBRAIZATION OF LOGIC
4.1. Preliminary remarks
5. THE ENGLISH ALGEBRA OF LOGIC IN THE 19TH CENTURY
5.1. A. De Morgan's syllogistic and the theory of relations
6. THE 20TH CENTURY WAY TO FORMALIZATION AND MECHANIZATION
6.1. Introduction
7. MECHANIZED DEDUCTION SYSTEMS
7.1. Introduction
File put on WWW server 17-02-96.
1.1.1. Is logic a device-independent system?
1.1.2. Mechanization as formalization and mechanization in the strict sense
1.1.3. The laws of logic as controlling a machine
1.2. The Leibniz-style Cybernetic Universe
1.2.1. The Cybernetic Universe - the world seen as consisting of
information-processing machines
1.2.2. A model-theoretical description of the Cybernetic Universe
1.3. Information-processing through data-processing
1.3.1. Information items as abstract entities
1.3.2. The relationship between information-processing
and data-processing
1.3.3. The information-processing in reasoning compared
with that in computing: a crucial difference
1.4. Intelligence and model-based reasoning
1.4.1. On the existence of reasonings which are not
text-based but model-based
1.4.2. On the existence of model-based non-apperceived
("unconscious") reasonings
1.4.3. On the Encoded Potential Concepts with which a
machine should be equipped to match natural intelligence in model-based
reasoning
2.1.1. Did Lull belong to the forerunners of the idea
of mechanizing arguments?
2.1.2. Risse's results in the above question
2.1.3. On the genuine contribution of medieval logic;
its evaluation at the background of the later role of algebra
2.2. Heuristic algorithms in the Middle Ages
2.2.1. Simple conceptual apprehension as the basic
operation of the mind
2.2.2. Lull's combinatory procedure of formingjudgements
2.2.3. The syllogistic method of producing proofs
2.2.4. The intellectual background in the Middle Ages
which encouraged the idea of mechanizing reasonings
2.2.5. The problems of inventio medii in logica inventionis
2.2.6. Some rules of a mechanical construction of
syllogisms by inventing middle terms
2.2.7. The postscholastic criticism of syllogistic
formalism in a contemporary perspective
2.3. The Role of Lull and Lullism
2.3.1. Lull - his life and personality
2.3.2. The source of the legend of Lull
2.3.3. On an instructive misinterpretation concerning Lull
2.3.4\it Ars Magna as a metaphysical and theological doctrine
2.3.5. The structure of Ars Magna as a combinatorial device
2.3.6. The lack in Ars Magna of formal methods to
check validity of syllogisms
2.3.7. On Lull's intuitionist approach, the problem
of its compatibility with his combinatorial approach
3.1.1. The early links between logic and geometry
3.1.2. The first encounter of logic and algebra in Leibniz
3.1.3. The decisive encounter of logic and algebra
in the 19th century
3.1.4. Examples of applying algebra to syllogistic
3.1.5. How logic evolved from the algebraic pattern
toward the modern characteristica (predicate logic)
3.1.6. A recent new reproachement between logic and
mathematics
3.2. The Renaissance reformism and intuitionism in logic
3.2.1. The civilizational and intellectual environment
of the new programmes of reforming logic: economic development, Platonian
inspiration
3.2.2. Ramus's reformatory ideas, Bacon's programme of
the inductive logic of discovery, and other
projects
3.2.3. The problem of how apt is deductive logic to
assist discoveries
3.2.4. The programme of deductive-intuitive logic in
Descartes and the Cartesian school
3.3. Leibniz on the mechanization of arguments
3.3.1. The notion of logical form in a historical perspective
3.3.2. On the algorithmic (mechanical) as a method
of mechanical problem-solving (caeca cogitatio)
3.3.3. Logical form, algorithms and computers
3.3.4. The counterpoint between the Leibnizian and
the Cartesian approach to logic
4.1.1. An overview of the process of mechanizing reasonings
4.1.2. The place of the 18th century in the process
under study
4.2. Leibniz's direct successors
4.2.1. Contributions of the brothers Bernouilli
4.2.2. On Wollf's role
4.2.3. Ploucquet's algebraic approach to syllogistic
4.3. The work of J. H. Lambert
4.3.1. On Lambert's (1728--1777) relation to Leibniz
4.3.2. A bridge between syllogistic forms and
algebraic equations
4.3.3. The notion of identity in syllogistic
4.3.4. The problem of influence of Leibniz and other
continental logicians upon the British algebra of logic
5.1.1. Aristotle's syllogistic
5.1.2. W. Hamilton and the quantification of the predicate
5.1.3. De Morgan's theory of syllogisms
5.1.4. De Morgan's study of relations
5.2. G. Boole and his algebra of logic
5.2.1. Logical works of G. Boole
5.2.2. Guiding principles of Boole's logic
5.2.3. Operations of the algebra of logic and their fundamental properties
5.2.4. Truth-value interpretation of the algebra of logic
5.2.5. Probabilistic interpretation of the algebra of logic
5.2.6. The process of development
5.2.7. The operation of solution
5.2.8. The operation of elimination
5.2.9. The meaning and significance of Boole's works
5.2.10. The comparison of works of Boole and De Morgan
5.3. The Logical works of Jevons
5.3.1. Jevons and Boole
5.3.2. The system of Jevons
5.3.3. Logical machine of Jevons
5.3.4. Other logical machines
5.3.5. The significance of Jevon's logical works
5.4. J. Venn and logical diagrams
5.4.1. Venn and Jevons
5.4.2. The logic of Venn
5.4.3. Venn's logical diagrams
5.4.4. The development of Venn's logical diagrams. Diagrams of L. Carrol
5.4.5. Venn's diagrams and the propositional calculus
5.4.6. The significance of Venn's method
5.5. Conclusions
6.2. G. Peano - symbolic language and the
axiomatization of mathematics
6.2.1. Early logical works
6.2.2 Arithmetices principia and the
axiomatization of arithmetic
6.2.3. The development of symbolic language
6.2.4. The significance of Peano's logical activity
6.3. G. Frege and the idea of a formal system
6.3.1. Frege and his predecessors
6.3.2. Fundamental ideas of Begriffsschrift
6.3.3. The symbolism of Frege
6.3.4. Frege's system of logic
6.3.5. The significance of Frege's work
6.3.6. The reception of Frege's ideas
6.4. B. Russell and the fulfillment of Peano's and Frege's projects
6.4.1. Discovery of inconsistency in Frege's Grundgesetze
6.4.2. Loooking for solutions to paradoxes
6.4.3. The theory of types
6.4.4 Principia Mathematica
6.4.5. The work of Russell as a fulfillment of Peano's and Frege's projects
6.4.6. Russell's philosophy of logic
6.5. Skolemization
6.5.1. Loewenheim and the Schr\"oderian tradition178
6.5.2. Loewenheim's theorem
6.5.3. Skolem's generalization of Loewenheim's theorem
6.5.4. Skolem normal form
6.5.5. Skolem's proof procedure
6.5.6. The meaning of Loewenheim's and Skolem's work
6.6. D. Hilbert and his program
6.6.1. Hilbert and his predecessors
6.6.2. Hilbert's program
6.6.3. Hilbert's system of logic
6.6.4. epsilon-terms
6.6.5. The significance of Hilbert's program
6.7. J. Herbrand
6.7.1. Herbrand and Hilbert's finitistic viewpoint
6.7.2. The fundamental theorem of Herbrand
6.7.3. Errors in Herbrand's proof
6.7.4. The elimination of modus ponens
6.7.5. Applications of the fundamental theorem
6.8. G. Gentzen and natural deduction
6.8.1. Historical background of Gentzen's works
6.8.2. Gentzen's natural deduction
6.8.3. Gentzen's logistic calculi
6.8.4.Hauptsatz and its applications
6.8.5. The significance and further development of Gentzen's systems
6.8.6. Gentzen and Herbrand
6.9. Semantic and analytic tableaux
6.9.1. The method of tableaux versus the method of Gentzen
6.9.2. Semantic tableaux of Beth
6.9.3. The significance and further development of the method
6.9.4. Analytic tableaux
6.10. Conclusions
7.1.1. Turing's and Church's limitative theorems
7.1.2. Presentation of the contents of the chapter
7.1.3. Automated theorems proving
7.1.4. Two philosophies of automated proving
7.2. First mechanized deduction systems
7.2.1. The Petersburger prover of M. Davis
7.2.2. The logic theorist of A.~Newell, J. S. Shaw and H. A. Simon
7.2.3. The Geometry Theorem-proving Machine of
Gelertner and others
7.2.4. Beth tableau prover of Gilmore
7.2.5. Gentzen-Herbrand prover of Hao Wang
7.2.6. The idea of A. Robinson
7.2.7. Davis-Putman procedure
7.3. Unification and resolution
7.3.1. The idea of Prawitz
7.3.2. The program of M. Davis
7.3.3. The origin of the resolution procedure
7.3.4. Prenex normal form
7.3.5. Skolmization
7.3.6. The conjunctive normal form and the clause form
7.3.7. The resolution clause for the propositional formulas
7.3.8. Unification algorithm
7.3.9. General form of the resolution
7.3.10. Completness of resolution
7.3.11. Improvements and modification of resolution
7.3.11.1. Unit-preference and set-of-support
7.3.11.2. Hyperresolution
7.3.11.3. Linear resolution
7.3.11.4. Model elimination
7.3.11.5. Lock-resolution
7.3.11.6. Semantic resolution
7.3.11.7. Unit clause resolution and input clause resolution
7.3.11.8. Paramodulation
7.3.12. The inverse method of Maslov
7.4.Further development of mechanized deduction systems after 1965
7.4.1. Semi Automated Mathematics
7.4.2. ADEPT
7.4.3. PLANNER
7.4.4. Human-oriented prover of Nevins
7.4.5. Automated theorem prover project of Bledsoe
7.4.6. Knuth and Bendix's provers
7.4.7. Resolution of (equational) theories
7.4.8. Automated reasoning Assistant
7.4.9. Computational Logic Theorem Prover of Boyer and Moore
7.4.10. Graph representation
7.4.11. Proving systems for higher order logics
7.4.12. Margraf Karl Refutation Procedure
7.5. Final remarks