• Produktbild: Higher Order Logic Theorem Proving and Its Applications
  • Produktbild: Higher Order Logic Theorem Proving and Its Applications
Band 780

Higher Order Logic Theorem Proving and Its Applications 6th International Workshop, HUG '93, Vancouver, B.C., Canada, August 11-13, 1993. Proceedings

49,99 €

inkl. gesetzl. MwSt., Versandkostenfrei


Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

28.04.1994

Abbildungen

X, 526 p.

Herausgeber

Jeffrey J. Joyce + weitere

Verlag

Springer Berlin

Seitenzahl

526

Maße (L/B/H)

23,5/15,5/2,9 cm

Gewicht

803 g

Auflage

1994

Sprache

Englisch

ISBN

978-3-540-57826-0

Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

28.04.1994

Abbildungen

X, 526 p.

Herausgeber

Verlag

Springer Berlin

Seitenzahl

526

Maße (L/B/H)

23,5/15,5/2,9 cm

Gewicht

803 g

Auflage

1994

Sprache

Englisch

ISBN

978-3-540-57826-0

Herstelleradresse

Springer-Verlag KG
Sachsenplatz 4-6
1201 Wien
AT

Email: GPSR Kontakt

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: Higher Order Logic Theorem Proving and Its Applications
  • Produktbild: Higher Order Logic Theorem Proving and Its Applications
  • Program verification using HOL-UNITY.- Graph model of LAMBDA in higher order logic.- Mechanizing a programming logic for the concurrent programming language microSR in HOL.- Reasoning with the formal definition of standard ML in HOL.- HOL-ML.- Structure and behaviour in hardware verification.- Degrees of formality in shallow embedding hardware description languages in HOL.- A functional approach for formalizing regular hardware structures.- A proof development system for the HOL theorem prover.- A HOL package for reasoning about relations defined by mutual induction.- A broader class of trees for recursive type definitions for HOL.- Some theorems we should prove.- Using PVS to prove some theorems of David Parnas.- Extending the HOL theorem prover with a computer algebra system to reason about the reals.- The HOL-Voss system: Model-checking inside a general-purpose theorem-prover.- Linking Higher Order Logic to a VLSI CAD system.- Alternative proof procedures for finite-state machines in higher-order logic.- A formalization of abstraction in LAMBDA.- Report on the UCD microcoded Viper verification project.- Verification of the Tamarack-3 microprocessor in a hybrid verification environment.- Abstraction techniques for modeling real-world interface chips.- Implementing a methodology for formally verifying RISC processors in HOL.- Domain theory in HOL.- Predicates, temporal logic, and simulations.- Formalization of variables access constraints to support compositionality of liveness properties.- The semantics of statecharts in HOL.- Value-passing CCS in HOL.- TPS: An interactive and automatic tool for proving theorems of type theory.- Modelling bit vectors in HOL: The word library.- Eliminating higher-order quantifiers to obtain decision procedures for hardware verification.- Toward a super duper hardware tactic.- A mechanisation of name-carrying syntax up to alpha-conversion.- A HOL decision procedure for elementary real algebra.- AC unification in HOL90.- Server-process restrictiveness in HOL.- Safety in railway signalling data: A behavioural analysis.- On the style of mechanical proving.- From abstract data types to shift registers:.- Verification in higher order logic of mutual exclusion algorithm.- Using Isabelle to prove simple theorems.