Mechanization of Reasoning in a Historical PerspectiveRodopi, 1995 - 267 This volume is written jointly by Witold Marciszewski, who contributed the introductory and the three subsequent chapters, and Roman Murawski who is the author of the next ones - those concerned with the 19th century and the modern inquiries into formalization, algebraization and mechanization of reasonings. Besides the authors there are other persons, as well as institutions, to whom the book owes its coming into being. The study which resulted in this volume was carried out in the Historical Section of the research project Logical Systems and Algorithms for Automatic Testing of Reasoning, 1986-1990, in which participated nine Polish universities; the project was coordinated by the Department of Logic, Methodology and Philosophy of Science of the Bia??l??ystok Branch of the University of Warsaw, and supported by the Ministry of Education (some of its results are reported in (Srzednicki (Ed.) 1987). The major part of the project was focussed on the software for computer-aided theorem proving called Mizar MSE (Multi-Sorted first-order logic with Equality, reported in (Marciszewski 1994a)) due to Dr. Andrzej Trybulec. He and other colleagues deserve a grateful mention for a hands-on experience and theoretical stimulants owed to their collaboration. |
Spis treści
| 11 | |
The Formalization of Arguments | 45 |
Leibnizs Idea of Mechanical Reasoning | 77 |
The English Algebra of Logic in the 19th Century | 129 |
The 20th Century Way to Formalization | 161 |
Mechanized Deduction Systems | 209 |
References | 231 |
| 253 | |
Extended Table of Contents | 261 |
Inne wydania - Wyświetl wszystko
Mechanization of Reasoning in a Historical Perspective Witold Marciszewski,Roman Murawski Ograniczony podgląd - 1995 |
Kluczowe wyrazy i wyrażenia
17th century abstract algebra of logic algorithm Analysis of Logic Aristotle arithmetic automated theorem automated theorem proving axioms Begriffsschrift Boole Boole's C₁ chapter clause cognitive column combination conjunctive normal form consists denote Descartes diagrams discussion domain equation example expressions fact finite formal formula Frege function Gentzen geometry given Hauptsatz hence Herbrand Hilbert Hilbert's program human idea interpretation introduced invention Jevons language Leibniz letters logical consequence logical form logicians Lull Lull's machine mathematical logic mathematician means mechanization of reasonings method middle term mind Morgan namely natural deduction negation notation objects operations paper Peano philosophical predicate calculus predicate logic premises prenex normal form Principia problem procedure proof propositional propositional calculus quantifiers relations resolution resolvent rules of inference Russell sentence sequences Skolem syllogism syllogistic symbols tableaux theorem proving theory tion truth universal validity variables Venn wrote xA(x
Popularne fragmenty
Strona 13 - At this point it only furnishes another illustration of the situation outlined earlier. There is an equivalence between logical principles and their embodiment in a neural network, and while in the simpler cases the principles might furnish a simplified expression of the network, it is quite possible that in cases of extreme complexity the reverse is true. All of this does not alter my belief that a new, essentially logical, theory is called for in order to understand high-complication automata and,...