Home
Publishing
DrugRxiv
Drug Repurposing
Network Medicine
About
REPO4EU
Meet the team
Drug Repurposing Research Collection
Conference
Blog
My ScienceOpen
Sign in
Register
Dashboard
Search
Home
Publishing
DrugRxiv
Drug Repurposing
Network Medicine
About
REPO4EU
Meet the team
Drug Repurposing Research Collection
Conference
My ScienceOpen
Sign in
Register
Dashboard
Search
33
views
14
references
Top references
cited by
12
Cite as...
0 reviews
Review
0
comments
Comment
0
recommends
+1
Recommend
0
collections
Add to
0
shares
Share
Twitter
Sina Weibo
Facebook
Email
2,502
similar
All similar
Record
: found
Abstract
: not found
Book Chapter
: not found
Theorem Proving in Higher Order Logics
Source-Level Proof Reconstruction for Interactive Theorem Proving
other
Author(s):
Lawrence C. Paulson
,
Kong Woei Susanto
Publication date
(Print):
2007
Publisher:
Springer Berlin Heidelberg
Read this book at
Publisher
Buy book
Review
Review book
Invite someone to review
Bookmark
Cite as...
There is no author summary for this book yet. Authors can add summaries to their books on ScienceOpen to make them more accessible to a non-specialist audience.
Related collections
Online interactive cancer simulations and demos
Most cited references
14
Record
: found
Abstract
: not found
Book
: not found
Isabelle/HOL
Tobias Nipkow
,
Markus Wenzel
,
Lawrence Paulson
(2002)
0
comments
Cited
199
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Book
: not found
Edinburgh LCF
Michael J. C. Gordon
,
Arthur Milner
,
Christopher Wadsworth
(1979)
0
comments
Cited
89
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
HOL Light: A tutorial introduction
John Harrison
(1996)
0
comments
Cited
53
times
– based on
0
reviews
Bookmark
All references
Author and book information
Book Chapter
Pages
: 232-245
DOI:
10.1007/978-3-540-74591-4_18
SO-VID:
5164b3b8-4170-4567-98f1-8661823db685
History
Data availability:
Comments
Comment on this book
Sign in to comment
Book chapters
pp. 5
Separation Logic for Small-Step cminor
pp. 22
Formalising Java’s Data Race Free Guarantee
pp. 383
Mizar’s Soft Type System
pp. 102
Verifying Nonlinear Real Formulas Via Sums of Squares
pp. 232
Source-Level Proof Reconstruction for Interactive Theorem Proving
pp. 334
HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism
Similar content
2,502
Static semantic analysis and theorem proving for CASL
Authors:
Till Mossakowski
,
Kolyang
,
Bernd Krieg-Brückner
CardioMEMS: Proving that Failure is not the only option for HF patients
Authors:
Carolyn Nissley
,
Justin D. Roberts
,
Lisa D. Rathman
…
Proving properties of a ring of finite-state machines
Authors:
Ichiro Suzuki
See all similar
Cited by
12
Automatic Proof and Disproof in Isabelle/HOL
Authors:
Jasmin Christian Blanchette
,
Lukas Bulwahn
,
Tobias Nipkow
Premise Selection for Mathematics by Corpus Analysis and Kernel Methods
Authors:
Jesse Alama
,
Tom Heskes
,
Daniel Kühlwein
…
Sledgehammer: Judgement Day
Authors:
Sascha Böhme
,
Tobias Nipkow
See all cited by