scientific article; zbMATH DE number 2003161

zbMath1023.68657MaRDI QIDQ4435474

Tobias Nipkow

Publication date: 12 November 2003

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

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Verification of clock synchronization algorithms: experiments on a combination of deductive tools, Mathematical method and proof, Introduction to ``Milestones in interactive theorem proving, Representing model theory in a type-theoretical logical framework, The Isabelle Framework, Proving pointer programs in higher-order logic, The Teaching Tool CalcCheck A Proof-Checker for Gries and Schneider’s “Logical Approach to Discrete Math”, Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle

Uses Software

• Isabelle
• Isabelle/Isar