Focusing on the groundbreaking contributions of Professor Jacob T. Schwartz, this text explores computational logic and set theory through the lens of proof verification techniques. It introduces the ÆtnaNova system, a prototype for verifying mathematical proofs in set theory. Key topics include leveraging first-order theories for reasoning in computer science and mathematics, automated proof verification for large software systems, and critical proof-engineering issues. An appendix provides formalized proofs of ordinals, transitive closure properties, induction principles, and Zorn's lemma.
Domenico Cantone Knihy




Theory of Money
- 102 stránek
- 4 hodiny čtení
This title, first published in 1965, provides an analysis of the forces and mechanisms governing the formation of the overall level of money prices. Even though this problem has a long history, and in spite of its obvious practical importance, it remains one of the most poorly understood questions in economic theory. This title will be of interest to students of monetary economics and the history of economic thought.
Set theory for computing
- 409 stránek
- 15 hodin čtení
"Set Theory for Computing" provides a comprehensive account of set-oriented symbolic manipulation methods suitable for automated reasoning. Its main objective is twofold: 1) to provide a flexible formalization for a variety of set languages, and 2) to clarify the semantics of set constructs firmly established in modern specification languages and in the programming practice. Topics include: semantic unification, decision algorithms, modal logics, declarative programming, tableau-based proof techniques, and theory-based theorem proving. The style of presentation is self-contained, rigorous and accurate. Some familiarity with symbolic logic is helpful but not a requirement. This book is a useful resource for all advanced students, professionals, and researchers in computing sciences, artificial intelligence, automated reasoning, logic, and computational mathematics. It will serve to complement their intuitive understanding of set concepts with the ability to master them by symbolic and logically based algorithmic methods and deductive techniques.
Lectures on the Mathematical Method in Analytical Economics
- 304 stránek
- 11 hodin čtení
An early but still useful and frequently cited contribution to the science of mathematical economics, this volume is geared toward graduate students in the field. Prerequisites include familiarity with the basic theory of matrices and linear transformations and with elementary calculus. Author Jacob T. Schwartz begins his treatment with an exploration of the Leontief input-output model, which forms a general framework for subsequent material. An introductory treatment of price theory in the Leontief model is followed by an examination of the business-cycle theory, following ideas pioneered by Lloyd Metzler and John Maynard Keynes. In the final section, Schwartz applies the teachings of previous chapters to a critique of the general equilibrium approach devised by Léon Walras as the theory of supply and demand, and he synthesizes the notions of Walras and Keynes. 1961 edition.