HOME > Detail View

Detail View

Higher order logic theorem proving and its applications : 8th International Workshop, Aspen Grove, UT, USA, September 11-14, 1995 : proceedings

Higher order logic theorem proving and its applications : 8th International Workshop, Aspen Grove, UT, USA, September 11-14, 1995 : proceedings (Loan 1 times)

Material type
단행본
Personal Author
Schubert, E. Thomas , 1959-. Windley, Phillip J. , 1958-. Alves-Foss, James , 1964-.
Title Statement
Higher order logic theorem proving and its applications : 8th International Workshop, Aspen Grove, UT, USA, September 11-14, 1995 : proceedings / E. Thomas Schubert, Phillip J. Windley, James Alves-Foss, eds.
Publication, Distribution, etc
Berlin ;   New York :   Springer-Verlag ,   1995.  
Physical Medium
viii, 400 p. : ill. ; 24 cm.
Series Statement
Lecture notes in computer science ; 971.
ISBN
3540602755 (alk. paper)
Bibliography, Etc. Note
Includes bibliographical references.
Subject Added Entry-Topical Term
Automatic theorem proving -- Congresses. Logic, Symbolic and mathematical -- Congresses.
000 01149camuu2200277 a 4500
001 000000601519
005 20080716095707
008 950801s1995 gw a b 100 0 eng
010 ▼a 95024951
020 ▼a 3540602755 (alk. paper)
040 ▼a DLC ▼c DLC ▼d 211009
049 ▼l 121035138 ▼f 과학
050 0 0 ▼a QA76.9.A96 ▼b H54 1995
082 0 0 ▼a 004/.01/5113 ▼2 20
090 ▼a 004.015113 ▼b H638 ▼c 8
245 0 0 ▼a Higher order logic theorem proving and its applications : ▼b 8th International Workshop, Aspen Grove, UT, USA, September 11-14, 1995 : proceedings / ▼c E. Thomas Schubert, Phillip J. Windley, James Alves-Foss, eds.
260 ▼a Berlin ; ▼a New York : ▼b Springer-Verlag , ▼c 1995.
300 ▼a viii, 400 p. : ▼b ill. ; ▼c 24 cm.
440 0 ▼a Lecture notes in computer science ; ▼v 971.
504 ▼a Includes bibliographical references.
650 0 ▼a Automatic theorem proving ▼x Congresses.
650 0 ▼a Logic, Symbolic and mathematical ▼x Congresses.
700 1 ▼a Schubert, E. Thomas , ▼d 1959-.
700 1 ▼a Windley, Phillip J. , ▼d 1958-.
700 2 ▼a Alves-Foss, James , ▼d 1964-.

Holdings Information

No. Location Call Number Accession No. Availability Due Date Make a Reservation Service
No. 1 Location Science & Engineering Library/Sci-Info(Stacks2)/ Call Number 004.015113 H638 8 Accession No. 121035138 Availability Available Due Date Make a Reservation Service B M

Contents information

Table of Contents

Mechanizing a ?-calculus equivalence in HOL.- Non-primitive recursive function definitions.- Experiments with ZF set theory in HOL and Isabelle.- Automatically synthesized term denotation predicates: A proof aid.- On the refinement of symmetric memory protocols.- Combining decision procedures in the HOL system.- Deciding cryptographic protocol adequacy with HOL.- A practical method for reasoning about distributed systems in a theorem prover.- A theory of finite maps.- Virtual theories.- An automata theory dedicated towards formal circuit synthesis.- Interfacing HOL90 with a functional database query language.- Floating point verification in HOL.- Inductive definitions: Automation and application.- A formulation of TLA in Isabelle.- Formal verification of serial pipeline multipliers.- TkWinHOL: A tool for Window Inference in HOL.- Formal verification of counterflow pipeline architecture.- Deep embedding VHDL.- HOLCF: Higher order logic of computable functions.- A mechanized logic for secure key escrow protocol verification.- A new interface for HOL - Ideas, issues and implementation.- Very efficient conversions.- Recording and checking HOL proofs.- Formalization of planar graphs.- A hierarchical method for reasoning about distributed programming languages.


Information Provided By: : Aladin

New Arrivals Books in Related Fields

김종원 (2020)