## A Computer System for Checking Proofs |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

Introduction | 7 |

Representations for Bound Variables 75 | 15 |

The Predicate Calculus | 37 |

Copyright | |

7 other sections not shown

### Common terms and phrases

accessible Algorithm Eq APL/CV proof APL/CV tree applied array Assertion Table assignment statement ASSUME automatic rules axioms bound variable called CLOSE-NEW instruction Computer construct contains Critical Region declared defined deleted derived Elimination rule EqAssert Eqlnsert equivalence class example execution path exit expression FIXED formula function graph hypothesis indexed loop INTRO Introduction rule invariant label LAMBDA language LBOUND(A LEAVE statements lemma loop body modified Natural Deduction ND tree Negation Distribution nest node normal form omnibus statement OPEN instruction operand links operator parameters parse parse graph parse tree performed PL/CS PL/CV point q pointer predicate calculus procedure PROCLAIM program verification proof block Proof Checker proof rule proof tree prove quantifier READONLY recla(e recla(ei recursive replacement rules representation reprlink reprlist REQUIRE RETURN statement routine rule in figure sequence shown in figure simple path substitution subtree syntax template theorem TrueNode undischarged assumptions V-code instructions V-code Interpreter