Top
| Series Foreword | |
| Preface to the First Edition | |
| Preface to the Second Edition | |
| Introduction | p. 3 |
| A Primer for the Logic | p. 19 |
| Formalization Within the Logic | p. 69 |
| A Precise Description of the Logic | p. 119 |
| Proving Theorems in the Logic | p. 187 |
| Mechanized Proofs in the Logic | p. 211 |
| An Introduction to the System | p. 221 |
| A Sample Session with the Theorem Prover | p. 231 |
| How to Use the Theorem Prover | p. 251 |
| How the Theorem Prover Works | p. 263 |
| The Four Classes of Rules Generated from Lemmas | p. 275 |
| Reference Guide | p. 295 |
| Hints on Using the Theorem Prover | p. 393 |
| Installing Nqthm | p. 413 |
| A Parser for the Syntax | p. 437 |
| The Primitive Shell Axioms | p. 475 |
| On the Difficulty of Proofs | p. 483 |
| References | p. 493 |
| Index | p. 507 |
| Table of Contents provided by Blackwell. All Rights Reserved. |
