| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNISA996466826103316 |
|
|
Titolo |
Barred Galaxies and Circumnuclear Activity [[electronic resource] ] : Proceedings of the NOBEL SYMPOSIUM 98 Held at Stockholm Observatory, Saltsjöbaden, Sweden, 30 November – 3 December 1995 / / edited by Aaage Sandqvist, Per O. Lindblad |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1996 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 1996.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (XI, 308 p.) |
|
|
|
|
|
|
Collana |
|
Lecture Notes in Physics, , 0075-8450 ; ; 474 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Observations, Astronomical |
Astronomy—Observations |
Astrophysics |
Space sciences |
Astronomy, Observations and Techniques |
Astrophysics and Astroparticles |
Space Sciences (including Extraterrestrial Physics, Space Exploration and Astronautics) |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Bibliographic Level Mode of Issuance: Monograph |
|
|
|
|
|
|
Nota di contenuto |
|
Some historical remarks on Bertil Lindblad's work on galactic dynamics -- Formation and evolution mechanisms of barred spiral galaxies -- Orbits in barred galaxies -- Secular evolution in barred galaxies -- The fate of barred galaxies in interacting and merging systems -- H i in barred spirals -- Hi Observations of a sample of barred spirals -- Hydrodynamical simulations of the barred spiral galaxy NGC 1365 -- Evolution of galaxies along the Hubble sequence -- Rings, lenses, nuclear bars: the fundamental role of gas -- The barred galaxy NGC 1530 -- A circumnuclear molecular torus in NGC 1365 -- Dynamics of inner galactic disks: The striking case of M 100 -- Dynamical substructures in two nearby galaxy nuclei -- The spheroidal component of Seyfert galaxies -- The pattern speed of the Galactic bulge -- The central Parsec of the Milky Way: Star formation and central |
|
|
|
|
|
|
|
|
|
|
|
|
|
dark mass -- Radio continuum and molecular gas in the Galactic Center -- The galactic center dynamics -- Observational evidence for the AGN paradigm -- Bar triggered nuclear activity and the anisotropic radiation fields of Active Galactic Nuclei -- Circumnuclear starbursts in barred galaxies -- Circumnuclear activity -- Outflows from the nearest barred galaxies -- The nuclear high excitation outflow cone in NGC 1365 -- Hubble Space Telescope observations of the centers of elliptical galaxies. |
|
|
|
|
|
|
Sommario/riassunto |
|
This collection of articles emerged from the Nobel Symposium 98 that celebrated the centenary of the Nobel Prize as well as the one of the famous Swedish astronomer Bertil Lindblad. Many outstanding scientists contributed to this unique review of the state of the art in barred galaxy research. Theoretical papers describe their evolution, the dynamics as well as fundamental physical effects near their nuclei. Other contributions cover numerical and observational aspects and thus represent a very active area in astrophysics. The centre of our galaxy was also amply dealt with. The collection addresses researchers as well as graduate students. |
|
|
|
|
|
|
|
|
2. |
Record Nr. |
UNISA996465954203316 |
|
|
Titolo |
Theorem Proving in Higher Order Logics [[electronic resource] ] : 9th International Conference, TPHOLs'96, Turku, Finland, August 26 - 30, 1996, Proceedings / / edited by Joakim von Wright, Jim Grundy, John Harrison |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1996 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 1996.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (VIII, 447 p.) |
|
|
|
|
|
|
Collana |
|
Lecture Notes in Computer Science, , 0302-9743 ; ; 1125 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Mathematical logic |
Artificial intelligence |
Logic design |
Computer logic |
Software engineering |
Mathematical Logic and Formal Languages |
Artificial Intelligence |
Logic Design |
Logics and Meanings of Programs |
Mathematical Logic and Foundations |
Software Engineering |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Bibliographic Level Mode of Issuance: Monograph |
|
|
|
|
|
|
Nota di contenuto |
|
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. |
|
|
|
|
|
|
|
|
Sommario/riassunto |
|
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. |
|
|
|
|
|
|
|
| |