Mechanizing proof: computing, risk, and trust
Most aspects of our private and social lives now depend on computing. But how can we know that this computing is trustworthy? In 'Mechanizing Proof', Donald MacKenzie addresses this key issue by investigating the interrelations of computing, risk, and mathematical proof.
Mechanizing proof: computing, risk, and trust
Most aspects of our private and social lives--our safety, the integrity of the financial system, the functioning of utilities and other services, and national security--now depend on computing. But how can we know that this computing is trustworthy? In Mechanizing Proof, Donald …
The book contains English translations of three outstanding dissertations in mathematical logic and complexity theory. L. Beklemishev proves that all provability logics must belong to one of the four previously known classes. The dissertation of M. Pentus proves the Chomsky conj…
The classical decision problem
by Gurevich, Yuri, Börger, Egon, Grädel, Erich
fromPerspectives in mathematical logic
The purpose of this book is to discuss whether statistical methods make sense. The present volume begins the task of providing interpretations and explanations of several theories of statistical evidence. It should be relevant to anyone interested in the logic of experimental sc…
Discussing whether statistical methods make sense, this book interprets and explains several theories of statistical evidence. It explains the senses in which Bayesian statistics and p-values allow us to draw conclusions. It is useful for anyone interested in the logic of experi…
Higher order logic theorem proving and its applications: proceedings of the IFIP TC10/WG10.2 International…
by Gordon, Michael J.C.,, informatica, Claesen, Luc J.M, International Federation for Information Processing., WG 10.2, CHEOPS ESPRIT BRA 3215, International Workshop on Higher Order Logic Theorem Proving and its Applications; HOL '92, Leuven,)
Higher order logic theorem proving and its applications: proceedings of the IFIP TC10/WG10.2 International…
by Commission of the European Communities, Gordon, Michael J. C., IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and Its Applications, Leuven, Belgium), Claesen, Luc J. M., Interuniversity Micro-Electronics Center
Higher order logic theorem proving and its applications: proceedings of the IFIP TC10/WG10.2 International…
by Commission of the European Communities, Gordon, Michael J. C., IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and Its Applications, Leuven, Belgium), Claesen, Luc J. M., Interuniversity Micro-Electronics Center
The HOL system is a higher order logic theorem proving system implemented at Edinburgh University, Cambridge University and INRIA. Its many applications, from the verification of hardware designs at all levels to the verification of programs and communication protocols are consi…
Selected papers in proof theory
