![Theorem Proving in Higher Order Logics [electronic resource] : 9th International Conference, TPHOLs’96 Turku, Finland, August 26–30, 1996 Proceedings /](/search/themes/bootstrap3/images/libros.png)
Theorem Proving in Higher Order Logics [electronic resource] : 9th International Conference, TPHOLs’96 Turku, Finland, August 26–30, 1996 Proceedings /
This book constitutes the refereed proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, TPHOL '96, held in Turku, Finland, in August 1996. The 27 revised full papers included together with one invited paper were carefully selected from a total of 46 submissions. The topics addressed are theorem proving technology, proof automation and decision procedures, mechanized theorem proving, extensions of higher order logics, integration of external tools, novel applications, and others. All in all, the volume is an up-to-date report on the state of the art in this increasingly active field.
Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Texto biblioteca |
| Language: | eng |
| Published: |
Berlin, Heidelberg : Springer Berlin Heidelberg,
1996
|
| Subjects: | Computer science., Logic design., Software engineering., Computer logic., Mathematical logic., Artificial intelligence., Computer Science., Mathematical Logic and Formal Languages., Artificial Intelligence (incl. Robotics)., Logic Design., Logics and Meanings of Programs., Mathematical Logic and Foundations., Software Engineering., |
| Online Access: | http://dx.doi.org/10.1007/BFb0105392 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| id |
KOHA-OAI-TEST:188763 |
|---|---|
| record_format |
koha |
| spelling |
KOHA-OAI-TEST:1887632018-07-30T23:12:04ZTheorem Proving in Higher Order Logics [electronic resource] : 9th International Conference, TPHOLs’96 Turku, Finland, August 26–30, 1996 Proceedings / Goos, Gerhard. editor. Hartmanis, Juris. editor. Leeuwen, Jan van. editor. Wright, Joakim von. editor. Grundy, Jim. editor. Harrison, John. editor. SpringerLink (Online service) textBerlin, Heidelberg : Springer Berlin Heidelberg,1996.engThis book constitutes the refereed proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, TPHOL '96, held in Turku, Finland, in August 1996. The 27 revised full papers included together with one invited paper were carefully selected from a total of 46 submissions. The topics addressed are theorem proving technology, proof automation and decision procedures, mechanized theorem proving, extensions of higher order logics, integration of external tools, novel applications, and others. All in all, the volume is an up-to-date report on the state of the art in this increasingly active field.Translating specifications in VDM-SL to PVS -- A comparison of HOL and ALF formalizations of a categorical coherence theorem -- Modeling a hardware synthesis methodology in isabelle -- Inference rules for programming languages with side effects in expressions -- Deciding cryptographic protocol adequacy with HOL: The implementation -- Proving liveness of fair transition systems -- Program derivation using the refinement calculator -- A proof tool for reasoning about functional programs -- Coq and hardware verification: A case study -- Elements of mathematical analysis in PVS -- Implementation issues about the embedding of existing high level synthesis algorithms in HOL -- Five axioms of alpha-conversion -- Set theory, higher order logic or both? -- A mizar mode for HOL -- Stålmarck’s algorithm as a HOL derived rule -- Towards applying the composition principle to verify a microkernel operating system -- A modular coding of UNITY in COQ -- Importing mathematics from HOL into Nuprl -- A structure preserving encoding of Z in isabelle/HOL -- Improving the result of high-level synthesis using interactive transformational design -- Using lattice theory in higher order logic -- Formal verification of algorithm W: The monomorphic case -- Verification of compiler correctness for the WAM -- Synthetic domain theory in type theory: Another logic of computable functions -- Function definition in higher-order logic -- Higher-order annotated terms for proof search -- A comparison of MDG and HOL for hardware verification -- A mechanisation of computability theory in HOL.This book constitutes the refereed proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, TPHOL '96, held in Turku, Finland, in August 1996. The 27 revised full papers included together with one invited paper were carefully selected from a total of 46 submissions. The topics addressed are theorem proving technology, proof automation and decision procedures, mechanized theorem proving, extensions of higher order logics, integration of external tools, novel applications, and others. All in all, the volume is an up-to-date report on the state of the art in this increasingly active field.Computer science.Logic design.Software engineering.Computer logic.Mathematical logic.Artificial intelligence.Computer Science.Mathematical Logic and Formal Languages.Artificial Intelligence (incl. Robotics).Logic Design.Logics and Meanings of Programs.Mathematical Logic and Foundations.Software Engineering.Springer eBookshttp://dx.doi.org/10.1007/BFb0105392URN:ISBN:9783540706410 |
| institution |
COLPOS |
| collection |
Koha |
| country |
México |
| countrycode |
MX |
| component |
Bibliográfico |
| access |
En linea En linea |
| databasecode |
cat-colpos |
| tag |
biblioteca |
| region |
America del Norte |
| libraryname |
Departamento de documentación y biblioteca de COLPOS |
| language |
eng |
| topic |
Computer science. Logic design. Software engineering. Computer logic. Mathematical logic. Artificial intelligence. Computer Science. Mathematical Logic and Formal Languages. Artificial Intelligence (incl. Robotics). Logic Design. Logics and Meanings of Programs. Mathematical Logic and Foundations. Software Engineering. Computer science. Logic design. Software engineering. Computer logic. Mathematical logic. Artificial intelligence. Computer Science. Mathematical Logic and Formal Languages. Artificial Intelligence (incl. Robotics). Logic Design. Logics and Meanings of Programs. Mathematical Logic and Foundations. Software Engineering. |
| spellingShingle |
Computer science. Logic design. Software engineering. Computer logic. Mathematical logic. Artificial intelligence. Computer Science. Mathematical Logic and Formal Languages. Artificial Intelligence (incl. Robotics). Logic Design. Logics and Meanings of Programs. Mathematical Logic and Foundations. Software Engineering. Computer science. Logic design. Software engineering. Computer logic. Mathematical logic. Artificial intelligence. Computer Science. Mathematical Logic and Formal Languages. Artificial Intelligence (incl. Robotics). Logic Design. Logics and Meanings of Programs. Mathematical Logic and Foundations. Software Engineering. Goos, Gerhard. editor. Hartmanis, Juris. editor. Leeuwen, Jan van. editor. Wright, Joakim von. editor. Grundy, Jim. editor. Harrison, John. editor. SpringerLink (Online service) Theorem Proving in Higher Order Logics [electronic resource] : 9th International Conference, TPHOLs’96 Turku, Finland, August 26–30, 1996 Proceedings / |
| description |
This book constitutes the refereed proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, TPHOL '96, held in Turku, Finland, in August 1996. The 27 revised full papers included together with one invited paper were carefully selected from a total of 46 submissions. The topics addressed are theorem proving technology, proof automation and decision procedures, mechanized theorem proving, extensions of higher order logics, integration of external tools, novel applications, and others. All in all, the volume is an up-to-date report on the state of the art in this increasingly active field. |
| format |
Texto |
| topic_facet |
Computer science. Logic design. Software engineering. Computer logic. Mathematical logic. Artificial intelligence. Computer Science. Mathematical Logic and Formal Languages. Artificial Intelligence (incl. Robotics). Logic Design. Logics and Meanings of Programs. Mathematical Logic and Foundations. Software Engineering. |
| author |
Goos, Gerhard. editor. Hartmanis, Juris. editor. Leeuwen, Jan van. editor. Wright, Joakim von. editor. Grundy, Jim. editor. Harrison, John. editor. SpringerLink (Online service) |
| author_facet |
Goos, Gerhard. editor. Hartmanis, Juris. editor. Leeuwen, Jan van. editor. Wright, Joakim von. editor. Grundy, Jim. editor. Harrison, John. editor. SpringerLink (Online service) |
| author_sort |
Goos, Gerhard. editor. |
| title |
Theorem Proving in Higher Order Logics [electronic resource] : 9th International Conference, TPHOLs’96 Turku, Finland, August 26–30, 1996 Proceedings / |
| title_short |
Theorem Proving in Higher Order Logics [electronic resource] : 9th International Conference, TPHOLs’96 Turku, Finland, August 26–30, 1996 Proceedings / |
| title_full |
Theorem Proving in Higher Order Logics [electronic resource] : 9th International Conference, TPHOLs’96 Turku, Finland, August 26–30, 1996 Proceedings / |
| title_fullStr |
Theorem Proving in Higher Order Logics [electronic resource] : 9th International Conference, TPHOLs’96 Turku, Finland, August 26–30, 1996 Proceedings / |
| title_full_unstemmed |
Theorem Proving in Higher Order Logics [electronic resource] : 9th International Conference, TPHOLs’96 Turku, Finland, August 26–30, 1996 Proceedings / |
| title_sort |
theorem proving in higher order logics [electronic resource] : 9th international conference, tphols’96 turku, finland, august 26–30, 1996 proceedings / |
| publisher |
Berlin, Heidelberg : Springer Berlin Heidelberg, |
| publishDate |
1996 |
| url |
http://dx.doi.org/10.1007/BFb0105392 |
| work_keys_str_mv |
AT goosgerhardeditor theoremprovinginhigherorderlogicselectronicresource9thinternationalconferencetphols96turkufinlandaugust26301996proceedings AT hartmanisjuriseditor theoremprovinginhigherorderlogicselectronicresource9thinternationalconferencetphols96turkufinlandaugust26301996proceedings AT leeuwenjanvaneditor theoremprovinginhigherorderlogicselectronicresource9thinternationalconferencetphols96turkufinlandaugust26301996proceedings AT wrightjoakimvoneditor theoremprovinginhigherorderlogicselectronicresource9thinternationalconferencetphols96turkufinlandaugust26301996proceedings AT grundyjimeditor theoremprovinginhigherorderlogicselectronicresource9thinternationalconferencetphols96turkufinlandaugust26301996proceedings AT harrisonjohneditor theoremprovinginhigherorderlogicselectronicresource9thinternationalconferencetphols96turkufinlandaugust26301996proceedings AT springerlinkonlineservice theoremprovinginhigherorderlogicselectronicresource9thinternationalconferencetphols96turkufinlandaugust26301996proceedings |
| _version_ |
1756265828179771392 |