Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Theorem Proving in Higher Order Logics [[electronic resource] ] : 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings / / edited by Jim Grundy, Malcolm Newey
| Theorem Proving in Higher Order Logics [[electronic resource] ] : 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings / / edited by Jim Grundy, Malcolm Newey |
| Edizione | [1st ed. 1998.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 |
| Descrizione fisica | 1 online resource (IX, 496 p.) |
| Disciplina | 004/.01/5113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer logic
Artificial intelligence Software engineering Mathematical logic Logic design Logics and Meanings of Programs Artificial Intelligence Software Engineering/Programming and Operating Systems Mathematical Logic and Formal Languages Software Engineering Logic Design |
| ISBN | 3-540-49801-X |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Verified lexical analysis -- Extending window inference -- Program abstraction in a higher-order logic framework -- The village telephone system: A case study in formal software engineering -- Generating embeddings from denotational descriptions -- An interface between CLAM and HOL -- Classical propositional decidability via Nuprl proof extraction -- A comparison of PVS and Isabelle/HOL -- Adding external decision procedures to HOL90 securely -- Formalizing basic first order model theory -- Formalizing Dijkstra -- Mechanical verification of total correctness through diversion verification conditions -- A type annotation scheme for Nuprl -- Verifying a garbage collection algorithm -- Hot: A concurrent automated theorem prover based on higher-order tableaux -- Free variables and subexpressions in higher-order meta logic -- An LPO-based termination ordering for higher-order terms without ?-abstraction -- Proving isomorphism of first-order logic proof systems in HOL -- Exploiting parallelism in interactive theorem provers -- I/O automata and beyond: Temporal logic and abstraction in Isabelle -- Object-oriented verification based on record subtyping in Higher-Order Logic -- On the effectiveness of theorem proving guided discovery of formal assertions for a register allocator in a high-level synthesis system -- Co-inductive axiomatization of a synchronous language -- Formal specification and theorem proving breakthroughs in geometric modeling -- A tool for data refinement -- Mechanizing relevant logics with HOL -- Case studies in meta-level theorem proving -- Formalization of graph search algorithms and its applications. |
| Record Nr. | UNINA-9910143491503321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Theorem Proving in Higher Order Logics [[electronic resource] ] : 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings / / edited by Jim Grundy, Malcolm Newey
| Theorem Proving in Higher Order Logics [[electronic resource] ] : 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings / / edited by Jim Grundy, Malcolm Newey |
| Edizione | [1st ed. 1998.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 |
| Descrizione fisica | 1 online resource (IX, 496 p.) |
| Disciplina | 004/.01/5113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer logic
Artificial intelligence Software engineering Mathematical logic Logic design Logics and Meanings of Programs Artificial Intelligence Software Engineering/Programming and Operating Systems Mathematical Logic and Formal Languages Software Engineering Logic Design |
| ISBN | 3-540-49801-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Verified lexical analysis -- Extending window inference -- Program abstraction in a higher-order logic framework -- The village telephone system: A case study in formal software engineering -- Generating embeddings from denotational descriptions -- An interface between CLAM and HOL -- Classical propositional decidability via Nuprl proof extraction -- A comparison of PVS and Isabelle/HOL -- Adding external decision procedures to HOL90 securely -- Formalizing basic first order model theory -- Formalizing Dijkstra -- Mechanical verification of total correctness through diversion verification conditions -- A type annotation scheme for Nuprl -- Verifying a garbage collection algorithm -- Hot: A concurrent automated theorem prover based on higher-order tableaux -- Free variables and subexpressions in higher-order meta logic -- An LPO-based termination ordering for higher-order terms without ?-abstraction -- Proving isomorphism of first-order logic proof systems in HOL -- Exploiting parallelism in interactive theorem provers -- I/O automata and beyond: Temporal logic and abstraction in Isabelle -- Object-oriented verification based on record subtyping in Higher-Order Logic -- On the effectiveness of theorem proving guided discovery of formal assertions for a register allocator in a high-level synthesis system -- Co-inductive axiomatization of a synchronous language -- Formal specification and theorem proving breakthroughs in geometric modeling -- A tool for data refinement -- Mechanizing relevant logics with HOL -- Case studies in meta-level theorem proving -- Formalization of graph search algorithms and its applications. |
| Record Nr. | UNISA-996466102203316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||