HOME > Detail View

Detail View

Higher order logic theorem proving and its applications : proceedings of the IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and Its Applications--HOL '92

Higher order logic theorem proving and its applications : proceedings of the IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and Its Applications--HOL '92

Material type
단행본
Personal Author
Claesen, Luc J. M. Gordon, Michael J. C., 1948-.
Corporate Author
Interuniversity Micro-Electronics Center.
Title Statement
Higher order logic theorem proving and its applications : proceedings of the IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and Its Applications--HOL '92 / organized by CHEOPS ESPRIT BRA 3215 ; sponsored by IMEC and the Commission of the European Communities, Leuven, Belgium, 21-24 September 1992 ; edited by Luc J.M. Claesen, Michael J.C. Gordon.
Publication, Distribution, etc
Amsterdam ;   New York :   North-Holland,   1993.  
Physical Medium
xiii, 568 p. : ill. ; 23 cm.
Series Statement
IFIP transactions. ;A, . Computer science and technology, = 0926-5473 ; A-20.
ISBN
0444898808 (acid-free)
Bibliography, Etc. Note
Includes bibliographical references.
Subject Added Entry-Topical Term
Automatic theorem proving --Congresses. Logic, Symbolic and mathematical --Congresses.
000 01540camuuu200313 a 4500
001 000000478144
003 OCoLC
005 19980922102651.0
008 921211s1993 ne a b 100 0 eng
010 ▼a 92046537
020 ▼a 0444898808 (acid-free)
040 ▼a DLC ▼c DLC
049 ▼l 121024204 ▼f 과학 ▼l 121035402 ▼f 과학
050 0 0 ▼a QA76.9.A96 ▼b I34 1992
082 0 0 ▼a 004/.01/5113 ▼2 20
090 ▼a 004.015113 ▼b I23h ▼c 1992
111 2 ▼a IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and Its Applications ▼d (1992 : ▼c Leuven, Belgium)
245 1 0 ▼a Higher order logic theorem proving and its applications : ▼b proceedings of the IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and Its Applications--HOL '92 / ▼c organized by CHEOPS ESPRIT BRA 3215 ; sponsored by IMEC and the Commission of the European Communities, Leuven, Belgium, 21-24 September 1992 ; edited by Luc J.M. Claesen, Michael J.C. Gordon.
260 ▼a Amsterdam ; ▼a New York : ▼b North-Holland, ▼c 1993.
300 ▼a xiii, 568 p. : ▼b ill. ; ▼c 23 cm.
440 0 ▼a IFIP transactions. ; ▼n A, . ▼p Computer science and technology, = ▼x 0926-5473 ; ▼v A-20.
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 Claesen, Luc J. M.
700 1 ▼a Gordon, Michael J. C., ▼d 1948-.
710 2 ▼a Interuniversity Micro-Electronics Center.
710 2 ▼a Commission of the European Communities.

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 I23h 1992 Accession No. 121024204 Availability Available Due Date Make a Reservation Service B M
No. 2 Location Science & Engineering Library/Sci-Info(Stacks2)/ Call Number 004.015113 I23h 1992 Accession No. 121035402 Availability Available Due Date Make a Reservation Service B M

Contents information

Table of Contents


CONTENTS
Preface = ⅴ
Conference Organization = ⅶ
Chapter 1 : Mathematical Logic Issues
 "The HOL Logic Extended with Quantification over Type Variables" / Thomas F. Melham = 3
 "A Lazy Approach to Fully-Expansive Theorem Proving" / Richard Boulton = 19
 "Efficient Representation and Computation of Tableaux Proofs" / Klaus Schneider ; Ramayya Kumar ; Thomas Kropf = 39
 "A Note on Interactive Theorem Proving with Theorem Continuation Functions" / Ching-Tsun Chou = 59
 "A Sequent Formulation of a Logic of Predicates in HOL" / Ching-Tsun Chou = 71
 "A Classical Type Theory with Transfinite Types" / Garrel Pottinger = 81
Chapter 2 : Induction
 "Unification-Based Induction" / Holger Busch = 97
 "Introducing well-founded function definitions in HOL" / Mark van der Voort = 117
 "Boyer-Moore Automation for the HOL System" / Richard J. Boulton = 133
Chapter 3 : General Modelling and Proofs
 "Constructing the real numbers in HOL" / John Harrison = 145
 "Modelling Generic Hardware Structures by Abstract Datatypes" / Klaus Schneider ; Ramayya Kumar ; Thomas Kropf = 165
 "A Methodology for Reusable Hardware Proofs" / Mark Aagaard ; Miriam Leeser = 177
 "Abstract Theories in HOL" / Phillip J. Windley = 197
 "Machine Abstraction in Microprocessor Specification" / Michael McAllister = 211
Chapter 4 : Formalizing and Modelling of Automata
 "A Formal Theory of Simulations Between Infinite Automata" / Paul Loewenstein = 227
 "A Comparison between Statecharts and State Transition Assertions" / Nancy Day = 247
 "An Embedding of Timed Transition Systems in HOL" / Rachel Cardell-Oliver Roger Hale ; John Herbert = 263
 "Formalizing a Modal Logic for CSS in the HOL Theorem Prover" / Monica Nesi = 279
 "Modelling Non-Deterministic Systems in HOL" / Jim Alves-Foss = 295
Chapter 5 : Program Verification
 "Mechanising some Advanced Refinement Concepts" / Hoakim von Wright ; J. Hekanaho ; P. Luostarinen ; T. Langb$$a^\circ $$ka = 307
 "Deriving Correctness Properties of Compiled Code" / Paul Curzon = 327
 "A HOL Mechanization of The Axiomatic Semantics of a Simple Distributed Programming Language" / William L. Harrison ; Myla M. Archer ; Karl N. Levitt = 347
Chapter 6 : Hardware Description Language Semantics
 "A Formalisation of the VHDL Simulation Cycle" / John P. van Tassel = 359
 "The Formal Semantics Definition of a Multi-Rate DSP Specification Language in HOL" / C. Angelo ; L. Claesen ; H. De Man = 375
 "Design-Flow Graph Partitioning" / R. B. Hughes ; G. Musgrave = 395
Chapter 7 : Hardware Verification Methodologies
 "Implementation and Use of Annotations in HOL" / Saraswati Kalvala ; Myla Archer ; Karl Levitt = 407
 "Towards a Formal Verification of a Floating Point Coprocessor and its Composition with a Central Processing Unit" / Jing Pan ; Karl N. Levitt ; Myla Archer ; Sara Kalvala = 427
 "Derving a Correct Computer" / Li-Guo Wang = 449
 "Formal Tools for Tri-State Design in Busses" / R. B. Hughes ; M. D. Francis ; S. P. Finn ; G. Musgrave = 459
 "Specification and Formal Synthesis of Digital Circuits" / M. Bombana ; P. Cavalloro ; G. Zaza = 475
Chapter 8 : Simulation in Higher Order Logic
 "Operational Semantics Based Formal Symbolic Simulation" / K. G. W. Goossens = 487
 "Simulating Microprocessors from Formal Specifications" / Kelly M. Hall ; Phillip J. Windley = 507
 "Executing HOL Specifications : Towards an Evaluation Semantics for Classical Higher Order Logic" / P. Sreeranga Rajan = 527
Chapter 9 : Extended uses of Higher Order Logic
 "Linking Other Theorem Provers to HOL Using PM : Proof manager" / Myla Archer ; George Fink ; Lie Yang = 539
 "Adding New Rules to an LCF-style Logic Implementation" / Konrad Slind = 549
 "Why We Can't have SML Style datatype Declarations in HOL" / Elsa L. Gunter = 561


New Arrivals Books in Related Fields

김종원 (2020)