HOME > 상세정보

상세정보

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 (1회 대출)

자료유형
단행본
개인저자
Schubert, E. Thomas , 1959-. Windley, Phillip J. , 1958-. Alves-Foss, James , 1964-.
서명 / 저자사항
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.
발행사항
Berlin ;   New York :   Springer-Verlag ,   1995.  
형태사항
viii, 400 p. : ill. ; 24 cm.
총서사항
Lecture notes in computer science ; 971.
ISBN
3540602755 (alk. paper)
서지주기
Includes bibliographical references.
일반주제명
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-.

소장정보

No. 소장처 청구기호 등록번호 도서상태 반납예정일 예약 서비스
No. 1 소장처 과학도서관/Sci-Info(2층서고)/ 청구기호 004.015113 H638 8 등록번호 121035138 도서상태 대출가능 반납예정일 예약 서비스 B M

컨텐츠정보

목차

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.


정보제공 : Aladin

관련분야 신착자료