• Produktbild: Theorem Proving in Higher Order Logics
  • Produktbild: Theorem Proving in Higher Order Logics
Band 2410

Theorem Proving in Higher Order Logics 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings

49,99 €

inkl. gesetzl. MwSt., Versandkostenfrei


Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

07.08.2002

Abbildungen

X, 347 p.

Herausgeber

Victor A. Carreno + weitere

Verlag

Springer Berlin

Seitenzahl

347

Maße (L/B/H)

23,5/15,5/2 cm

Gewicht

552 g

Auflage

2002

Sprache

Englisch

ISBN

978-3-540-44039-0

Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

07.08.2002

Abbildungen

X, 347 p.

Herausgeber

Verlag

Springer Berlin

Seitenzahl

347

Maße (L/B/H)

23,5/15,5/2 cm

Gewicht

552 g

Auflage

2002

Sprache

Englisch

ISBN

978-3-540-44039-0

Herstelleradresse

Springer-Verlag KG
Sachsenplatz 4-6
1201 Wien
AT

Email: ProductSafety@springernature.com

Noch keine Bewertungen vorhanden

Verfassen Sie die erste Bewertung zu diesem Artikel

Helfen Sie anderen Kundinnen und Kunden durch Ihre Meinung.

Kundinnen und Kunden meinen

Bewertungen (0)

  • Produktbild: Theorem Proving in Higher Order Logics
  • Produktbild: Theorem Proving in Higher Order Logics
  • Invited Talks.- Formal Methods at NASA Langley.- Higher Order Unification 30 Years Later.- Regular Papers.- Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction.- Efficient Reasoning about Executable Specifications in Coq.- Verified Bytecode Model Checkers.- The 5 Colour Theorem in Isabelle/Isar.- Type-Theoretic Functional Semantics.- A Proposal for a Formal OCL Semantics in Isabelle/HOL.- Explicit Universes for the Calculus of Constructions.- Formalised Cut Admissibility for Display Logic.- Formalizing the Trading Theorem for the Classification of Surfaces.- Free-Style Theorem Proving.- A Comparison of Two Proof Critics: Power vs. Robustness.- Two-Level Meta-reasoning in Coq.- PuzzleTool: An Example of Programming Computation and Deduction.- A Formal Approach to Probabilistic Termination.- Using Theorem Proving for Numerical Analysis Correctness Proof of an Automatic Differentiation Algorithm.- Quotient Types: A Modular Approach.- Sequent Schema for Derived Rules.- Algebraic Structures and Dependent Records.- Proving the Equivalence of Microstep and Macrostep Semantics.- Weakest Precondition for General Recursive Programs Formalized in Coq.