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 considered in depth in this volume. Other systems based on higher order logic, namely Nuprl and LAMBDA are also discussed.

Features given particular consideration are: novel developments in higher order logic and its implementations in HOL; formal design and verification methodologies for hardware and software; public domain availability of the HOL system.

Papers addressing these issues have been divided as follows: Mathematical Logic; Induction; General Modelling and Proofs; Formalizing and Modelling of Automata; Program Verification; Hardware Description Language Semantics; Hardware Verification Methodologies; Simulation in Higher Order Logic; Extended Uses of Higher Order Logic.

Academic and industrial researchers involved in formal hardware and software design and verification methods should find the publication especially interesting and it is hoped it will also provide a useful reference tool for those working at software institutes and within the electronics industries.

Frequently asked questions

Simply head over to the account section in settings and click on “Cancel Subscription” - it’s as simple as that. After you cancel, your membership will stay active for the remainder of the time you’ve paid for. Learn more here.

At the moment all of our mobile-responsive ePub books are available to download via the app. Most of our PDFs are also available to download and we're working on making the final remaining ones downloadable now. Learn more here.

Both plans give you full access to the library and all of Perlego’s features. The only differences are the price and subscription period: With the annual plan you’ll save around 30% compared to 12 months on the monthly plan.

We are an online textbook subscription service, where you can get access to an entire online library for less than the price of a single book per month. With over 1 million books across 1000+ topics, we’ve got you covered! Learn more here.

Look out for the read-aloud symbol on your next book to see if you can listen to it. The read-aloud tool reads text aloud for you, highlighting the text as it is being read. You can pause it, speed it up and slow it down. Learn more here.

Yes, you can access Higher Order Logic Theorem Proving and its Applications by L.J.M. Claesen, M.J.C. Gordon, L.J.M. Claesen,M.J.C. Gordon in PDF and/or ePUB format, as well as other popular books in Mathematics & Logic in Mathematics. We have over one million books available in our catalogue for you to explore.

Information

Publisher

North Holland

Year

2014

ISBN

9781483298405

Topic

Mathematics

Subtopic

Logic in Mathematics

Index

Mathematics

Front Cover
Higher Order Logic Theorem Proving and its Applications
Copyright Page
Table of Contents
Preface
Conference organization
Part 1. Mathematical Logic
Part 2: Induction
Part 3: General Modelling and Proofs
Part 4: Formalizing and Modelling ofAutomata
Part 5: Program Verification
Part 6: Hardware Description LanguageSemantics
Part 7: Hardware Verification Methodologies
Part 8: Simulation in Higher Order Logic
Part 9: Extended uses of Higher Order Logic