Procedimiento de refutación para un conjunto de restricciones sobre documentos XML

We present a prototype that implements a set of logical rules to prove the satis ability for a class of speci cations on XML documents. Speci cations are given by means of constraints built on Boolean XPath patterns. The main goal of this tool is to test if a given speci cation is satis able or not, showing the history of the execution. It can also be used to test if a given document is a model of a given speci cation and, as a subproduct, it allows to look for all the relations (monomorphisms) between two patterns or the result of doing some operations by combining patterns in di erent ways. The results of these operations are visually shown and therefore the tool makes these operations more understandable. The implementation of the algorithm has been written in Prolog but the prototype has a Java interface for an easy and friendly use.

PICC vs Catéter central insertado en vena subclavia en pacientes críticos

[Es]Introducción: actualmente, en servicios como UCIs, quirófanos y Urgencias cada vez es más común el empleo de CVCS y PICC. Ambos están asociados a graves complicaciones como CLABSI, TVP, EP, arritmia, etc. Dado que la enfermería juega un papel importante tanto en la inserción de estos dispositivos, como en el mantenimiento y prevención de las adversidades, es necesario poseer los conocimientos y habilidades adecuados para su afrontamiento. Objetivo y metodología: determinar cuál de los dos supone menor riesgo de complicaciones en pacientes críticos mediante la evidencia científica y utilizando la EBE. Para ello se ha realizado una revisión bibliográfica de estudios encontrados en bases de datos como Pubmed, Cochrane y Cinhal mediante la combinación de términos MeSH y palabras clave con operadores booleanos. Resultados y discusión: se han incluido en total 13 publicaciones (6 RS, 4 estudios de cohorte, 1 ECA y 2 GPC), de las cuales 3 poseen calidad alta, 3 media y 5 baja. Tanto los PICC como los CVCS implican diversas complicaciones, divididas en infecciosas, trombo-embolicas y mecánicas/otras. Existe insuficiente evidencia científica y gran heterogeneidad entre los artículos, lo que dificulta su extrapolación. Conclusiones: en pacientes críticos los PICC poseen mayor riesgo de TVP, los CVCS de complicaciones mecánicas, y ambos presentan tasas similares de CLABSI. Es importante escoger de forma individualizada el catéter a implantar, estimando los riesgos-beneficios de cada uno. Los cuidados preventivos son fundamentales en la reducción de estas contingencias. Son necesarios más estudios prospectivos comparativos.

Beyond Q-Resolution and Prenex Form: a Proof System for Quantified Constraint Satisfaction

We consider the quanti fied constraint satisfaction problem (QCSP) which is to decide, given a structure and a first-order sentence (not assumed here to be in prenex form) built from conjunction and quanti fication, whether or not the sentence is true on the structure. We present a proof system for certifying the falsity of QCSP instances and develop its basic theory; for instance, we provide an algorithmic interpretation of its behavior. Our proof system places the established Q-resolution proof system in a broader context, and also allows us to derive QCSP tractability results.

Digital Quantum Simulation of Spin Models with Circuit Quantum Electrodynamics

Systems of interacting quantum spins show a rich spectrum of quantum phases and display interesting many-body dynamics. Computing characteristics of even small systems on conventional computers poses significant challenges. A quantum simulator has the potential to outperform standard computers in calculating the evolution of complex quantum systems. Here, we perform a digital quantum simulation of the paradigmatic Heisenberg and Ising interacting spin models using a two transmon-qubit circuit quantum electrodynamics setup. We make use of the exchange interaction naturally present in the simulator to construct a digital decomposition of the model-specific evolution and extract its full dynamics. This approach is universal and efficient, employing only resources that are polynomial in the number of spins, and indicates a path towards the controlled simulation of general spin dynamics in superconducting qubit platforms.