MARC details
| 000 -CABECERA |
|---|
| campo de control de longitud fija |
04321nam a22004335i 4500 |
| 001 - NÚMERO DE CONTROL |
|---|
| campo de control |
88278 |
| 003 - IDENTIFICADOR DEL NÚMERO DE CONTROL |
|---|
| campo de control |
ES-MaUEC |
| 005 - FECHA Y HORA DE LA ÚLTIMA TRANSACCIÓN |
|---|
| campo de control |
20230207040630.0 |
| 007 - CAMPO FIJO DE DESCRIPCIÓN FÍSICA--INFORMACIÓN GENERAL |
|---|
| campo de control de longitud fija |
cr nn 008mamaa |
| 008 - DATOS DE LONGITUD FIJA--INFORMACIÓN GENERAL |
|---|
| campo de control de longitud fija |
161122s2016 gw | s |||| 0|eng d |
| 020 ## - NÚMERO INTERNACIONAL ESTÁNDAR DEL LIBRO |
|---|
| Número Internacional Estándar del Libro |
9783662504970 |
| 024 7# - IDENTIFICADOR DE OTROS ESTÁNDARES |
|---|
| Número estándar o código |
10.1007/978-3-662-50497-0 |
| Fuente del número o código |
doi |
| 040 ## - FUENTE DE LA CATALOGACIÓN |
|---|
| Centro catalogador/agencia de origen |
ES-MaUEC |
| 050 #4 - SIGNATURA TOPOGRÁFICA DE LA BIBLIOTECA DEL CONGRESO |
|---|
| Número de clasificación |
QA279.4 |
| Número de documento/Ítem |
K764 2016 EB |
| 100 1# - ENTRADA PRINCIPAL--NOMBRE DE PERSONA |
|---|
| Nombre de persona |
Kroening, Daniel |
| Número de control del registro de autoridad o número normalizado |
http://id.loc.gov/authorities/names/no2009033013 |
| -- |
Local |
| 9 (RLIN) |
101914 |
| 245 10 - MENCIÓN DE TÍTULO |
|---|
| Título |
Decision Procedures : |
| Resto del título |
An Algorithmic Point of View |
| Mención de responsabilidad, etc. |
by Daniel Kroening, Ofer Strichman. |
| 250 ## - MENCIÓN DE EDICIÓN |
|---|
| Mención de edición |
2nd ed. 2016. |
| 260 ## - PUBLICACIÓN, DISTRIBUCIÓN, ETC. |
|---|
| Lugar de publicación, distribución, etc. |
Berlin, Heidelberg |
| Nombre del editor, distribuidor, etc. |
Springer |
| Fecha de publicación, distribución, etc. |
2016 |
| 300 ## - DESCRIPCIÓN FÍSICA |
|---|
| Extensión |
1 recurso en línea (XXI, 356 p.) |
| Otras características físicas |
64 ilustraciones, 5 ilustraciones en color |
| 336 ## - TIPO DE CONTENIDO |
|---|
| Término de tipo de contenido |
Texto (visual) |
| Código de tipo de contenido |
txt |
| Fuente |
rdacontent |
| 337 ## - TIPO DE MEDIO |
|---|
| Nombre/término del tipo de medio |
electrónico |
| Código del tipo de medio |
c |
| Fuente |
rdamedia |
| 338 ## - TIPO DE SOPORTE |
|---|
| Nombre/término del tipo de soporte |
recurso electrónico |
| Código del tipo de soporte |
cr |
| Fuente |
rdacarrier |
| 490 1# - MENCIÓN DE SERIE |
|---|
| Mención de serie |
Texts in Theoretical Computer Science. An EATCS Series |
| Número Internacional Normalizado para Publicaciones Seriadas |
1862-4499 |
| 505 0# - NOTA DE CONTENIDO CON FORMATO |
|---|
| Nota de contenido con formato |
Introduction and Basic Concepts -- Decision Procedures for Propositional Logic -- From Propositional to Quantifier-Free Theories -- Equalities and Uninterpreted Functions -- Linear Arithmetic -- Bit Vectors -- Arrays -- Pointer Logic -- Quantified Formulas -- Deciding a Combination of Theories -- Propositional Encodings -- Applications in Software Engineering -- SMT-LIB 2.0: A Brief Tutorial -- A C++ Library for Developing Decision Procedures. |
| 520 ## - SUMARIO, ETC. |
|---|
| Sumario, etc. |
A decision procedure is an algorithm that, given a decision problem, terminates with a correct yes/no answer. Here, the authors focus on theories that are expressive enough to model real problems, but are still decidable. Specifically, the book concentrates on decision procedures for first-order theories that are commonly used in automated verification and reasoning, theorem-proving, compiler optimization and operations research. The techniques described in the book draw from fields such as graph theory and logic, and are routinely used in industry. The authors introduce the basic terminology of SAT, Satisfiability Modulo Theories (SMT) and the DPLL(T) framework. Then, in separate chapters, they study decision procedures for propositional logic; equalities and uninterpreted functions; linear arithmetic; bit vectors; arrays; pointer logic; and quantified formulas. They also study the problem of deciding combined theories based on the Nelson-Oppen procedure. The first edition of this book was adopted as a textbook in courses worldwide. It was published in 2008 and the field now called SMT was then in its infancy, without the standard terminology and canonic algorithms it has now; this second edition reflects these changes. It brings forward the DPLL(T) framework. It also expands the SAT chapter with modern SAT heuristics, and includes a new section about incremental satisfiability, and the related Constraints Satisfaction Problem (CSP). The chapter about quantifiers was expanded with a new section about general quantification using E-matching and a section about Effectively Propositional Reasoning (EPR). The book also includes a new chapter on the application of SMT in industrial software engineering and in computational biology, coauthored by Nikolaj Bjørner and Leonardo de Moura, and Hillel Kugler, respectively. Each chapter includes a detailed bibliography and exercises. Lecturers� slides and a C++ library for rapid prototyping of decision procedures are available from the authors� website. |
| 650 07 - PUNTO DE ACCESO ADICIONAL DE MATERIA--TÉRMINO DE MATERIA |
|---|
| Término de materia o nombre geográfico como elemento de entrada |
Ingeniería del software |
| Fuente del encabezamiento o término |
embne |
| 9 (RLIN) |
152630 |
| 650 07 - PUNTO DE ACCESO ADICIONAL DE MATERIA--TÉRMINO DE MATERIA |
|---|
| Término de materia o nombre geográfico como elemento de entrada |
Ordenadores |
| Fuente del encabezamiento o término |
embne |
| 9 (RLIN) |
138111 |
| 650 07 - PUNTO DE ACCESO ADICIONAL DE MATERIA--TÉRMINO DE MATERIA |
|---|
| 9 (RLIN) |
145705 |
| Término de materia o nombre geográfico como elemento de entrada |
Optimización matemática |
| Fuente del encabezamiento o término |
embne |
| 650 #7 - PUNTO DE ACCESO ADICIONAL DE MATERIA--TÉRMINO DE MATERIA |
|---|
| Término de materia o nombre geográfico como elemento de entrada |
Informática |
| Fuente del encabezamiento o término |
embne |
| 9 (RLIN) |
139268 |
| 700 1# - PUNTO DE ACCESO ADICIONAL--NOMBRE DE PERSONA |
|---|
| Nombre de persona |
Strichman, Ofer |
| Número de control del registro de autoridad o número normalizado |
Local |
| 9 (RLIN) |
101915 |
| 830 #0 - PUNTO DE ACCESO ADICIONAL DE SERIE-TÍTULO UNIFORME |
|---|
| Título uniforme |
Texts in Theoretical Computer Science. An EATCS Series |
| Número Internacional Normalizado para Publicaciones Seriadas |
1862-4499 |
| 9 (RLIN) |
134292 |
| 856 40 - LOCALIZACIÓN Y ACCESO ELECTRÓNICOS |
|---|
| Identificador Uniforme del Recurso |
https://go.openathens.net/redirector/universidadeuropea.es?url=https://link.springer.com/book/10.1007/978-3-662-50497-0zAcceso a este recurso digital (usuarios Universidad Europea de Madrid) |
| 999 ## - NÚMEROS DE CONTROL DE SISTEMA (KOHA) |
|---|
| -- |
1 |
| 901 ## - ID MILLENIUM |
|---|
| Id Millenium |
i9783662504970 |
| 907 ## - TRANSACCIONES MILLENIUM |
|---|
| id bib interno millenium |
.b12982829 |
| fecha actualizac reg bib |
10-10-17 |
| fecha creacion reg bib |
08-03-17 |
| 942 ## - ELEMENTOS DE PUNTO DE ACCESO ADICIONAL (KOHA) |
|---|
| Fuente del sistema de clasificación o colocación |
Library of Congress Classification |
| Tipo de ítem Koha |
LIBRO-E NO PRÉSTAMO |
| 945 ## - ITEM MILLENIUM |
|---|
| Signatura |
QA279.4 K764 2016 EB |
| Número de copia |
1 |
| Código de barras |
eBOOK |
| Agencia |
0 |
| Localización del ejemplar (ubicación) |
mae |
| Código 2 (categoría) |
- |
| Precio |
EUR0.00 |
| Mensaje (popup en cliente staff) |
- |
| Mensaje (visible en OPAC) |
- |
| Estado |
b |
| Tipo de ejemplar |
15 |
| Total de préstamos |
0 |
| Total de renovaciones |
0 |
| Préstamos del año en curso |
0 |
| Préstamos del año anterior |
0 |
| Identificador de la copia de ejemplar en Millennium |
.i11604669 |
| Fecha de creación del ejemplar |
06-04-17 |
| 988 ## - NOTA LOCAL 598 |
|---|
| Nota local 598 |
EBOOK, EBSPRINGER |
| 998 ## - FONDO MILLENIUM |
|---|
| Biblioteca |
m |
| -- |
_alco |
| -- |
_vill |
| Fecha creación |
- - |
| Tipo de registro |
m |
| Tipo de materia |
E-book |
| e |
- |
| Idioma |
eng |
| País |
gw |
| h |
0 |