## Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96, Turku, Finland, August 26 - 30, 1996, ProceedingsJoakim von Wright, Jim Grundy, John Harrison This book constitutes the refereed proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, TPHOL '96, held in Turku, Finland, in August 1996. The 27 revised full papers included together with one invited paper were carefully selected from a total of 46 submissions. The topics addressed are theorem proving technology, proof automation and decision procedures, mechanized theorem proving, extensions of higher order logics, integration of external tools, novel applications, and others. All in all, the volume is an up-to-date report on the state of the art in this increasingly active field. |

### What people are saying - Write a review

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

### Contents

Translating Specifications in VDMSL to PVS | 1 |

S Agerholm | 15 |

Modeling a Hardware Synthesis Methodology in Isabelle | 33 |

Copyright | |

24 other sections not shown

### Other editions - View all

### Common terms and phrases

a)term abstract algorithm applied asize assignment assumptions Automated automatically axioms behavior BGNY bool boolean calculus circuit composed Computer Science constants construction constructors corresponding datatype defined definition derived described domain Domain Theory embedding equations equivalent example expression Formal Synthesis formula function functional programs goal hardware high level synthesis higher order logic higher-order logic implementation induction inference rules input instantiated Isabelle Isabelle/HOL lambda lambda-terms lattice Lecture Notes lemma mathematical Melham Mizar modules natural numbers node Nuprl operational semantics operator predicate progress properties proof propositions protocol reasoning recursive Refinement Calculator refinement calculus relation represented result schema semantics set theory specification Springer-Verlag step structure subgoal subnode substitution syntax tactics term tion tool transformation transition translated type checking type inference type theory type variables universal quantification VDM-SL verification window inference