Structured proofs in Isar/HOL

DOI10.1007/3-540-39185-1_15MaRDI QIDQ4435474zbMATH OpenFDO

Authors Tobias Nipkow

Publication date 12 November 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2646/26460259.htm

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited in

(19)

• Introduction to ``Milestones in interactive theorem proving
• Formalizing axiomatic systems for propositional logic in Isabelle/HOL
• Proving pointer programs in higher-order logic
• Verification of clock synchronization algorithms: experiments on a combination of deductive tools
• The teaching tool CalcCheck: a proof-checker for Gries and Schneider's ``Logical approach to discrete math
• The Isabelle Framework
• Hotel Key Card
• DiskPaxos
• More Church-Rosser proofs (in Isabelle/HOL)
• scientific article; zbMATH DE number 2110621 (Why is no real title available?)
• Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL
• Verified Real Asymptotics in Isabelle/HOL
• Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle
• Types for Proofs and Programs
• Representing model theory in a type-theoretical logical framework
• Representing Isabelle in LF
• Invertibility in Sequent Calculi
• Tarski's Parallel Postulate implies the 5th Postulate of Euclid, the Postulate of Playfair and the original Parallel Postulate of Euclid
• Mathematical method and proof

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/Isar

This page was built for publication: Structured proofs in Isar/HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4435474)