Automated Reasoning : (Registro nro. 296600)
[ vista simple ]
| 000 -CABECERA | |
|---|---|
| campo de control de longitud fija | 06441nam a22003855i 4500 |
| 001 - NÚMERO DE CONTROL | |
| campo de control | 296600 |
| 003 - IDENTIFICADOR DEL NÚMERO DE CONTROL | |
| campo de control | MX-SnUAN |
| 005 - FECHA Y HORA DE LA ÚLTIMA TRANSACCIÓN | |
| campo de control | 20170705134236.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 | 150903s2006 gw | o |||| 0|eng d |
| 020 ## - NÚMERO INTERNACIONAL ESTÁNDAR DEL LIBRO | |
| Número Internacional Estándar del Libro | 9783540371885 |
| -- | 9783540371885 |
| 024 7# - IDENTIFICADOR DE OTROS ESTÁNDARES | |
| Número estándar o código | 10.1007/11814771 |
| Fuente del número o código | doi |
| 035 ## - NÚMERO DE CONTROL DEL SISTEMA | |
| Número de control de sistema | vtls000349275 |
| 039 #9 - NIVEL DE CONTROL BIBLIOGRÁFICO Y DETALLES DE CODIFICACIÓN [OBSOLETO] | |
| Nivel de reglas en descripción bibliográfica | 201509030737 |
| Nivel de esfuerzo utilizado para asignar no-encabezamientos de materia en puntos de acceso | VLOAD |
| Nivel de esfuerzo utilizado en la asignación de encabezamientos de materia | 201404121212 |
| Nivel de esfuerzo utilizado para asignar clasificación | VLOAD |
| Nivel de esfuerzo utilizado en la asignación de encabezamientos de materia | 201404090949 |
| Nivel de esfuerzo utilizado para asignar clasificación | VLOAD |
| -- | 201402071158 |
| -- | staff |
| 040 ## - FUENTE DE LA CATALOGACIÓN | |
| Centro catalogador/agencia de origen | MX-SnUAN |
| Lengua de catalogación | spa |
| Centro/agencia transcriptor | MX-SnUAN |
| Normas de descripción | rda |
| 050 #4 - CLASIFICACIÓN DE LA BIBLIOTECA DEL CONGRESO | |
| Número de clasificación | Q334-342 |
| 100 1# - ENTRADA PRINCIPAL--NOMBRE DE PERSONA | |
| Nombre de persona | Furbach, Ulrich. |
| Término indicativo de función/relación | editor. |
| 9 (RLIN) | 302039 |
| 245 10 - MENCIÓN DE TÍTULO | |
| Título | Automated Reasoning : |
| Resto del título | Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006. Proceedings / |
| Mención de responsabilidad, etc. | edited by Ulrich Furbach, Natarajan Shankar. |
| 264 #1 - PRODUCCIÓN, PUBLICACIÓN, DISTRIBUCIÓN, FABRICACIÓN Y COPYRIGHT | |
| Producción, publicación, distribución, fabricación y copyright | Berlin, Heidelberg : |
| Nombre del de productor, editor, distribuidor, fabricante | Springer Berlin Heidelberg, |
| Fecha de producción, publicación, distribución, fabricación o copyright | 2006. |
| 300 ## - DESCRIPCIÓN FÍSICA | |
| Extensión | xv, 680 páginas Also available online. |
| Otras características físicas | recurso en línea. |
| 336 ## - TIPO DE CONTENIDO | |
| Término de tipo de contenido | texto |
| Código de tipo de contenido | txt |
| Fuente | rdacontent |
| 337 ## - TIPO DE MEDIO | |
| Nombre/término del tipo de medio | computadora |
| Código del tipo de medio | c |
| Fuente | rdamedia |
| 338 ## - TIPO DE SOPORTE | |
| Nombre/término del tipo de soporte | recurso en línea |
| Código del tipo de soporte | cr |
| Fuente | rdacarrier |
| 347 ## - CARACTERÍSTICAS DEL ARCHIVO DIGITAL | |
| Tipo de archivo | archivo de texto |
| Formato de codificación | |
| Fuente | rda |
| 490 0# - MENCIÓN DE SERIE | |
| Mención de serie | Lecture Notes in Computer Science, |
| Número Internacional Normalizado para Publicaciones Seriadas | 0302-9743 ; |
| Designación de volumen o secuencia | 4130 |
| 500 ## - NOTA GENERAL | |
| Nota general | Springer eBooks |
| 505 0# - NOTA DE CONTENIDO CON FORMATO | |
| Nota de contenido con formato | Invited Talks -- Mathematical Theory Exploration -- Searching While Keeping a Trace: The Evolution from Satisfiability to Knowledge Compilation -- Representing and Reasoning with Operational Semantics -- Session 1. Proofs -- Flyspeck I: Tame Graphs -- Automatic Construction and Verification of Isotopy Invariants -- Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms -- Using the TPTP Language for Writing Derivations and Finite Interpretations -- Session 2. Search -- Stratified Context Unification Is NP-Complete -- A Logical Characterization of Forward and Backward Chaining in the Inverse Method -- Connection Tableaux with Lazy Paramodulation -- Blocking and Other Enhancements for Bottom-Up Model Generation Methods -- Session 3. System Description 1 -- The MathServe System for Semantic Web Reasoning Services -- System Description: GCLCprover + GeoThms -- A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms -- Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation -- Session 4. Higher-Order Logic -- Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics -- Towards Self-verification of HOL Light -- An Interpretation of Isabelle/HOL in HOL Light -- Combining Type Theory and Untyped Set Theory -- Session 5. Proof Theory -- Cut-Simulation in Impredicative Logics -- Interpolation in Local Theory Extensions -- Canonical Gentzen-Type Calculi with (n,k)-ary Quantifiers -- Dynamic Logic with Non-rigid Functions -- Session 6. System Description 2 -- AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework -- CEL — A Polynomial-Time Reasoner for Life Science Ontologies -- FaCT++ Description Logic Reasoner: System Description -- Importing HOL into Isabelle/HOL -- Session 7. Search -- Geometric Resolution: A Proof Procedure Based on Finite Model Search -- A Powerful Technique to Eliminate Isomorphism in Finite Model Search -- Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems -- Session 8. Proof Theory -- Strong Cut-Elimination Systems for Hudelmaier’s Depth-Bounded Sequent Calculus for Implicational Logic -- Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach -- First-Order Logic with Dependent Types -- Session 9. Proof Checking -- Automating Proofs in Category Theory -- Formal Global Optimisation with Taylor Models -- A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers -- Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials -- Session 10. Combination -- A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA) -- Solving Sparse Linear Constraints -- Inferring Network Invariants Automatically -- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL -- Session 11. Decision Procedures -- Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures -- Verifying Mixed Real-Integer Quantifier Elimination -- Presburger Modal Logic Is PSPACE-Complete -- Tree Automata with Equality Constraints Modulo Equational Theories -- Session 12. CASC-J3 -- CASC-J3 The 3rd IJCAR ATP System Competition -- Session 13. Rewriting -- Matrix Interpretations for Proving Termination of Term Rewriting -- Partial Recursive Functions in Higher-Order Logic -- On the Strength of Proof-Irrelevant Type Theories -- Consistency and Completeness of Rewriting in the Calculus of Constructions -- Session 14. Description Logic -- Specifying and Reasoning About Dynamic Access-Control Policies -- On Keys and Functional Dependencies as First-Class Citizens in Description Logics -- A Resolution-Based Decision Procedure for . |
| 520 ## - SUMARIO, ETC. | |
| Sumario, etc. | This book constitutes the refereed proceedings of the Third International Joint Conference on Automated Reasoning, IJCAR 2006, held in Seattle, WA, USA in August 2006 as part of the 4th Federated Logic Conference, FLoC 2006. IJCAR 2006 is a merger of CADE, FroCoS, FTP, TABLEAUX, and TPHOLs. The 41 revised full research papers and 8 revised system descriptions presented together with 3 invited papers and a summary of a systems competition were carefully reviewed and selected from a total of 152 submissions. The papers address the entire spectrum of research in automated reasoning including formalization of mathematics, proof theory, proof search, description logics, interactive proof checking, higher-order logic, combination methods, satisfiability procedures, and rewriting. The papers are organized in topical sections on proofs, search, higher-order logic, proof theory, search, proof checking, combination, decision procedures, CASC-J3, rewriting, and description logic. |
| 590 ## - NOTA LOCAL (RLIN) | |
| Nota local | Para consulta fuera de la UANL se requiere clave de acceso remoto. |
| 700 1# - PUNTO DE ACCESO ADICIONAL--NOMBRE DE PERSONA | |
| Nombre de persona | Shankar, Natarajan. |
| Término indicativo de función/relación | editor. |
| 9 (RLIN) | 331789 |
| 710 2# - PUNTO DE ACCESO ADICIONAL--NOMBRE DE ENTIDAD CORPORATIVA | |
| Nombre de entidad corporativa o nombre de jurisdicción como elemento de entrada | SpringerLink (Servicio en línea) |
| 9 (RLIN) | 299170 |
| 776 08 - ENTRADA/ENLACE A UN FORMATO FÍSICO ADICIONAL | |
| Información de relación/Frase instructiva de referencia | Edición impresa: |
| Número Internacional Estándar del Libro | 9783540371878 |
| 856 40 - LOCALIZACIÓN Y ACCESO ELECTRÓNICOS | |
| Identificador Uniforme del Recurso | <a href="http://remoto.dgb.uanl.mx/login?url=http://dx.doi.org/10.1007/11814771">http://remoto.dgb.uanl.mx/login?url=http://dx.doi.org/10.1007/11814771</a> |
| Nota pública | Conectar a Springer E-Books (Para consulta externa se requiere previa autentificación en Biblioteca Digital UANL) |
| 942 ## - ELEMENTOS DE PUNTO DE ACCESO ADICIONAL (KOHA) | |
| Tipo de ítem Koha | Recurso en línea |
No hay ítems disponibles.