bluuebunny/crossref_metadata_2025 huggingface dataset:
Eclampsia en embarazo pretérmino, causas, sintomatología y métodos de prevención
Authors: Fuentes Aguilera Carlos Tomas , Espinoza Troya Joselyn Ivonne , Zea Pin Vanessa Alexandra , Choéz Macías Jeniffer Vanessa
Published: June 2023

La eclampsia es una complicación severa de la enfermedad hipertensiva del embarazo que afecta al sistema nervioso central, manifestándose con un cuadro clínico de convulsiones generalizadas y/o coma en una gestante con hipertensión y proteinuria previas (preeclampsia). La metodología utilizada para el presente trabajo de investigación, se enmarca dentro de una revisión bibliográfica de tipo documental. La técnica para la recolección de datos está constituida por materiales electrónicos, estos últimos como Google Académico, entre otros, apoyándose para ello en el uso de descriptores certificados y avalados por el tesauro de la UNESCO. La información aquí obtenida será revisada, resumida y analizada para su exposición organizada en los resultados. Los trastornos hipertensivos en el embarazo pueden ser desencadenado por varios factores, como la edad, obesidad, tradición familiar hipertensa, entre otras. Sin embargo, la eclampsia está determinada como una complicación de la preeclampsia, por ello es fundamental una vigilancia continua de parte del médico tratante, ya que esta patología puede ser silenciosa y conlleva a complicaciones que pueden desencadenar en la muerte de la paciente y feto, así como la interrupción del embarazo como uno de los manejos para evitar la muerte de la paciente, el diagnóstico es variado e incluye exploración física, estudios de laboratorios e imágenes.
Solución informática basada en un sistema estructurado de gestión y control de riesgos profesionales
Authors: González Mendoza Otto Rodrigo , Rodas Soto Patricia Estefanny , Olvera Morán Mariuxi Yomaira , Avellán Torres Oscar Alfredo
Published: June 2023

El presente artículo esbosa la solución que es plasmada en un sistema estructurado de Gestión y control de riesgos profesionales a los cuales los empleados de las empresas están expuestos durante el desarrollo de sus actividades cotidianas dentro de la compañía. Con lo que se plantea en este artículo permitirá poder tener un control exacto de los posibles accidentes, o enfermedades de los colaboradores. Estos procesos antes se gestionaba de forma mecánica y se elaboraban los registros en hojas de cálculo. Para la elaboración de este artículo se usó en un principio, un análisis de la situación actual de los procesos internos, logrando identificar de esa forma las falencias existentes; luego de ello se utilizó insumo tales como: la metodología de desarrollo, técnicas de la entrevista y la encuesta. Con estos resultados de acuerdo a los datos obtenidos permitieron cubrir las necesidades, logrando la satisfacción de los usuarios internos tales como los Jefes de Gestión y Calidad, Gerente de Recursos Humanos, Jefe de Recursos Humanos y en mayor proporción de los colaboradores de la empresa, al poder conocer todos los riesgos y metodologías de prevención que se deben ejecutar. A través de esta solución Web, además, se garantiza la disponibilidad en cualquier momento de la información, la integridad de los datos almacenados y confiabilidad de la información, así como de los indicadores.
Efectividad del aprendizaje virtual en comparación con el aprendizaje presencial usando una herramienta de IA basada en Machine Learning
Authors: García Torres Ingrid Angélica , Castillo León Rosa Elizabeth , Taranto Vera Gilda Judith
Published: June 2023

Para esta investigación se utilizó una herramienta de IA basada en Machine Learning para evaluar la efectividad del aprendizaje virtual en comparación con el aprendizaje presencial. El estudio se llevó a cabo en una universidad de la ciudad de Guayaquil y se analizaron datos de rendimiento y comportamiento de los estudiantes en ambos tipos de enseñanza. Sin embargo, se descubrió que el aprendizaje virtual requería una mayor motivación y disciplina por parte de los estudiantes. La herramienta de IA utilizada en este estudio analizó varios aspectos, como el tiempo de inactividad, el tiempo dedicado a tareas y la participación en discusiones en línea. Teniendo en cuenta que el objetivo principal de esta investigación es el de evaluar la eficacia del aprendizaje virtual frente al aprendizaje presencial utilizando una herramienta de Inteligencia Artificial basadas en Machine Learning con la metodología de experimentar dichos aprendizajes, se encontró que el aprendizaje virtual permitía a los estudiantes trabajar a su propio ritmo y adaptarse mejor a su programación personal. Sin embargo, también se observó que los estudiantes podían sentirse más aislados y menos comprometidos en comparación con el aprendizaje presencial. La herramienta de IA demostró ser útil para evaluar la efectividad de ambos tipos de enseñanza y proporcionar una mayor comprensión de cómo los estudiantes interactúan con el contenido.
Generación del conocimiento en Instituciones de Salud mediante la aplicación de metadatos
Authors: Bustamante Chong César Antonio , Cabezas Galarza Franklin Augusto , Bustamante Chong Mariana Elizabeth
Published: June 2023

Las unidades hospitalarias del país carecen de médicos especialistas para atender el volumen intenso de pacientes que existen, muchas veces este número reducido de expertos se debe, entre otras cosas: ofertas de posgrado inexistentes, no existencia de políticas claras en la oferta y demanda. Por lo expuesto, se tiene como información, la demanda de las atenciones médicas a los pacientes, su posterior sintomatología y medicación; el número de profesionales y sus diferentes especialidades, etc.; lo cual nos conlleva a determinar cómo gestionar y aprovechar dicha información para impulsar mediante un enfoque predictivo, una herramienta de inteligencia de negocios Knime y ayudada por la metodología CRISP-DM propia de los proyectos que emplean minería de datos; el análisis y la toma de decisiones en seleccionar las mejores especialidades. El objetivo es analizar la crisis de especialidades médicas mediante un enfoque predictivo de la información a través de herramientas y metodologías de minado de datos; los principales objetivos específicos son: identificar la información pertinente a partir de la información relevada; diseñar el enfoque predictivo a través de modelos y metodología de minería de datos y evaluar el modelo predictivo mediante variables en la toma de decisiones. Finalmente, con el análisis predictivo de la información de datos hospitalarios, se pudo identificar, seleccionar y mejorar las variables que permitieron la toma de decisiones oportuna para la apertura de especialidades médicas necesarias y acertadas; identificar fuentes de trabajo; detectar las enfermedades catastróficas con un alto índice de mortalidad y poder mitigar su incidencia en la sociedad.
Estrategias para evitar la deserción universitaria
Authors: Pimentel Elbert Michael Jonathan , Villamar Cárdenas María Auxiliadora , Andrade Zumárraga Diego Andrés , Zambrano Mendoza Bernardita Monserrate
Published: June 2023

La deserción universitaria es un fenómeno mundial donde convergen muchos factores, según cada región, con carácter alarmante ya que sus consecuencias son importantes y afectan a diferentes actores como: estudiantes, instituciones y Estado. La aplicación de estrategias para eliminar y prevenir la deserción estudiantil es esencial para las instituciones de educación superior, por lo tanto, se deben implementar técnicas que permitan establecer estas estrategias o proyectos idóneos para una situación particular. En base a lo anterior, es que se define el objetivo de la presente investigación la cual intenta plasmar las principales estrategias generales para evitar la deserción universitaria, especialmente en América Latina. En razón de ello, se decidió que el estudio se adelantara en base a un diseño bibliográfico y una metodología de revisión, mediante el cual se fue seleccionando artículos de interés científico académico, así como también otras clases de documentos formales. El estudio de las causas de la deserción escolar es imperioso para el establecimiento de estrategias que permitan combatirla. Entre las principales estrategias generales aplicadas en diferentes universidades de Latinoamérica se encontraron las siguientes: estrategias institucionales, académicas, personales y económicas. De estas variables macro, se pueden derivar los planes y programas necesarios según la condición de cada región e incluso de cada institución. Es necesario facilitar el acceso y la permanencia de los jóvenes en la educación superior. Las revisiones constantes de las prácticas pedagógicas e institucionales, elementos como el currículo, los diferentes perfiles del egresado, incluso los sistemas de evaluación e incentivos, a los fines de garantizar una oferta educativa que evite la deserción universitaria.
Prácticas de economía circular en mercados públicos
Authors: Morante Galarza Marianela Sara , Benítez Troya Fausto Arturo , Parrales León Aldo Gerardo
Published: June 2023

Se centra en la importancia de la economía circular como modelo sostenible en respuesta a la crisis ambiental global. Se mencionan los objetivos del desarrollo sostenible y la necesidad de reconsiderar el modelo de negocio en favor de la economía circular. También se destacan los efectos del cambio climático y se argumenta a favor de una reforma profunda de los sistemas de producción para lograr un crecimiento sostenible. Tiene como objetivo llevar a cabo una caracterización de la economía circular en mercados públicos, mediante el análisis de prácticas actuales, la identificación de barreras, oportunidades. Además, se explora la importancia de los mercados públicos como bienes municipales y se mencionan aspectos económicos y espaciales relacionados con los mercados. Luego, se describe la metodología utilizada en la investigación sobre economía circular en mercados públicos, incluyendo la revisión de literatura y la selección de fuentes relevantes. Por último, se presentan los resultados y discusiones, como el enfoque político en la economía circular, la mejora de normas y regulaciones, y la importancia de modelos macro y encuestas en la implementación de prácticas de economía circular. También se mencionan los desafíos y retos que enfrentan los mercados públicos en relación con la economía circular.
La intervención de la logística en la gestión de residuos sólidos en Latinoamérica
Authors: Banguera Arroyo Leonardo Alvaro , Vera Nicola Rina Jacqueline , Vásquez Moreno Wagner , Llamuca Baque Gerardo David
Published: June 2023

Los residuos sólidos es un tema de mucha importancia debido a que abarca a todas las comunidades a nivel nacional e internacional en la siguiente investigación se basa en dar a conocer a las personas sobre los desechos sólidos a nivel nacional e internacional, como podrían ayudar a reducir estos desechos. El estudio aborda desde la aplicación de la red circular donde las industrias y fabricas son responsables de eliminar la basura que ellos mismos fabrican y esto a su vez son utilizados para la fabricación de nuevos productos, la situación actual de Ecuador frente a la innovación que debe enfrentar. Con base a los datos recolectados por el Instituto Nacional de Estadística y Censos (INEC) y la información que nos brinda el Ministerio del Ambiente del Ecuador (MAE). Mediante estas investigaciones se ha podido deducir que en la actualidad las estrategias de la economía circular a nivel internacional aplicada a las empresas han beneficiado a actores como el productor, consumidor y en especial al medio ambiente.
Influencia de la formación docente-investigador, en el acrecentamiento de la excelencia académica, Universidad de Guayaquil
Authors: López Coloma Rodrigo Víctor , Moscoso Zamora Víctor Hugo , Nájera Núñez Bélgica Cecilia , Maquizaca Najera Raizza Belen
Published: June 2023

La mundialización, ha influenciado en la gestión de la educación superior latinoamericana; en sus actividades para la planificación académica institucional e investigación, por ende, la Universidad Ecuatoriana deberá innovar sus procesos para el logro de la excelencia académica. Nuestro estudio se centró en medir el nivel de influencia del plan de formación docente en investigación, en el desarrollo de la excelencia académica en la Universidad de Guayaquil durante el periodo 2022. Nuestro diseño de investigación fue; el transeccional descriptivo, método; dialéctico, analógico e inferencial, utilizamos técnicas estadísticas mediante el SPSS, y el coeficiente de correlación de Spearman, cuyos resultados cuantificaron de manera directa y significativa el nivel de influencia, a partir de los cuales, se determinó la relevancia de la formación continua de los profesores de la Universidad de Guayaquil-Ecuador, en investigación para el logro de sus objetivos institucionales.
Avances tecnológicos y científicos en radiología
Authors: Calva Sánchez Ricardo Javier , Jimenez Buri Karla Fernanda , Herrera Sarango Stephany Catherine , Núñez Cabrera Carlos Magno
Published: June 2023

Desde el surgimiento de la era digital, las nuevas tecnologías han evolucionado a un paso acelerado y, la radiología no es un campo que ha escapado a esta realidad, por lo que se ha creado la necesidad de que los profesionales del área se deban actualizar constantemente sobre los nuevos avances científicos y tecnológicos que existen con el fin de desarrollar las competencias necesarias para brindar un servicio óptimo a los pacientes. La metodología utilizada para el presente trabajo de investigación, se enmarca dentro de una revisión bibliográfica de tipo documental. La técnica para la recolección de datos está constituida por materiales electrónicos, estos últimos como Google Académico, entre otros, apoyándose para ello en el uso de descriptores certificados y avalados por el tesauro de la UNESCO. La información aquí obtenida será revisada, resumida y analizada para su exposición organizada en los resultados. Los estudios de Rayos X fueron los primeros estudios de imágenes en la historia de la medicina, su contribución en el diagnóstico y tratamiento de diferentes patologías ha sido fundamental para salvar la vida de innumerables personas en todo el mundo, y como la medicina y la ciencia evoluciona, los estudios de imágenes como los rayos x también, estos estudios no son invasivos, sin embargo, el cuerpo humano está sometido a radiaciones que no han generado complicaciones o efectos a considerar. Las nuevas tecnologías lo que buscan es mejorar la calidad de las imágenes, menor radiación, más precisión en el diagnóstico y por consiguiente seguir mejorando la eficiencia de los servicios de salud a nivel mundial, entre las nuevas tecnologías se tienen la utilización de equipos portátiles, inclusión de inteligencia artificial, trabajo remoto, conteo de fotones para reducirlos niveles de radiación sin alterar la calidad de la imagen, la incorporación de lo digital implica un menor coste ya que no es necesaria la impresión del acetato a menos que sea necesario.
Utilidad de tecnologías recientes en imágenes diagnosticas
Authors: Moncayo Tamayo Susana Paulette , Rosero Feijoo Arleth Paola , Ronquillo del Pozo Sally Estefanía , Limones Moncada María Stephania
Published: June 2023

La imagen para el diagnóstico es una de las mejores herramientas de las que dispone el sistema sanitario actual para conseguir visualizar con detalle el interior del organismo de un paciente, pero en los tiempos que corren no solo basta con disponer de equipos que brinden unas imágenes claras, nítidas y de calidad. En la actualidad, si se desean conseguir diagnósticos rápidos y realmente fiables, es preciso ayudarse de sistemas inteligentes, automatizados y modernos que sean capaces de ofrecer imágenes, así como resultados sobre aquello que analizan en la imagen. La metodología utilizada para el presente trabajo de investigación, se enmarca dentro de una revisión bibliográfica de tipo documental. La técnica para la recolección de datos está constituida por materiales electrónicos, estos últimos como Google Académico, entre otros, apoyándose para ello en el uso de descriptores certificados y avalados por el tesauro de la UNESCO. La información aquí obtenida será revisada, resumida y analizada para su exposición organizada en los resultados. Las últimas tecnologías de imágenes han sido fundamentales para el diagnóstico y tratamiento de prácticamente todas las patologías que así lo requieran, los rayos X fueron los primeros estudios de imágenes empleados en la medicina, sin embargo, como todo tienen sus limitaciones, por ello la irrupción de la tomografía axial computarizada y la resonancia magnética, para optimizar las imágenes de las estructuras del organismo con una mayor precisión y visión, esto sumado la incorporación de la tecnología 3D y los simuladores, han brindado una amplio espectro para el diagnóstico y tratamiento de patologías complejas que antes podían ser tratadas a ciegas, a su vez que a medida que la tecnología aumenta, la disminución de complicaciones y errores humanos también disminuye.
Contraste en tomografía axial computarizada
Authors: Ronquillo del Pozo Sally Estefanía , Limones Moncada María Stephania , Moncayo Tamayo Susana Paulette , Rosero Feijoo Arleth Paola
Published: June 2023

La tomografía axial computarizada (TAC) permite obtener imágenes de las estructuras densas dentro del cuerpo, como los huesos, mientras que los tejidos blandos varían en su capacidad para detener los rayos X, por lo que pueden ser borrosos o difíciles de visualizar, en cuyo caso se usan medios de contraste que son altamente visibles y que son seguros de usar en los pacientes. No obstante, la TAC con medio de contraste puede tener algunos efectos adversos como la reacción alérgica al medio de contraste, daño a la función renal y exposición a la radiación. Es importante destacar al respecto que, algunas personas tienen alergias al medio de contraste y algunos de sus efectos secundarios más comunes son: náuseas o vómitos, estornudos, picazón o urticaria. Asimismo, en pocas ocasiones, el medio de contraste puede ocasionar una respuesta alérgica potencialmente mortal llamada anafilaxia. De lo anterior se infiere la importancia de que el personal clínico que solicita un TAC con contraste tenga el deber de conocer sus características, los riesgos, contraindicaciones, posibles efectos secundarios y protocolos de administración. En tal sentido, el objetivo principal de la presente investigación es plasmar las generalidades acerca de los medios de contraste usados en tomografía axial computarizada. La investigación se desarrolló mediante una metodología de tipo documental bibliográfica bajo la modalidad de revisión. La identificación de los factores de riesgo para el uso de medios de contraste y la clasificación de estos pacientes es fundamental para tomar las medidas necesarias que garanticen su bienestar y minimizar o evitar la aparición de efectos secundarios. El contraste yodado es uno de los más usados en TAC por ser altamente efectivo y con menos efectos adversos, no obstante, pueden presentarse. Uno de estos efectos adversos más importantes es el daño renal agudo (IRA) inducido por contraste, cuyo factor principal de riesgo es la enfermedad renal crónica pre existente.
Comparación de la precisión diagnóstica de tomografía computarizada y resonancia magnética de lesiones de hígado
Authors: Fabre Morales Erick Josue , Maila Zuñiga Sergio Andrés , Araujo Acuña Priscila Adriana , Gómez Méndez Daniel Gustavo
Published: June 2023

Las enfermedades difusas del hígado son entidades que comprometen globalmente el parénquima hepático; estas pueden ser agudas, destacándose la hepatitis aguda de etiología viral (virus hepatotrópicos A, B, C, D, E y G), tóxicas o alcohólicas. Las hepatitis agudas suelen ser autolimitadas y en algunas ocasiones evolucionan hacia la cronicidad o terminan en una falla hepática fulminante. En relación con los procesos crónicos podemos identificar la hepatitis crónica de causa viral, autoinmune, por tóxicos o fármacos, y secundaria a enfermedades metabólicas; la cirrosis hepática y las morbilidades colestásicas pueden ser de origen intra o extrahepáticas. La metodología utilizada para el presente trabajo de investigación, se enmarca dentro de una revisión bibliográfica de tipo documental. La técnica para la recolección de datos está constituida por materiales electrónicos, estos últimos como Google Académico, entre otros, apoyándose para ello en el uso de descriptores certificados y avalados por el tesauro de la UNESCO. La información aquí obtenida será revisada, resumida y analizada para su exposición organizada en los resultados. Hay distintas lesiones que se puede presentar en el hígado, sin embargo, las más comunes son el cáncer, la cirrosis hepática y el hígado graso, como método diagnostico tanto la tomografía computarizada y la resonancia magnética, cumplen un papel fundamental en el diagnóstico de estas patologías, ya que dependiendo del grado de la enfermedad se puede utilizar una u otro medio diagnóstico, o incluso ambas, esto nos indica que la resonancia magnética es más utilizada en los inicios de las enfermedades o los primeros estadios, mientras que la tomografía computarizada es un estudio más amplio para las enfermedades que ya tienen un alto grado de avance.
Trust and Innovative Behavior: A Multilevel Analysis of Competence-based Trust, Compassion-based Trust, and LMX Differentiation
Authors:   Korean Academy Of Management, Kim Jeeyoung , Oh Hongseok , Chung Myung-Ho
Published: June 2023

In current turbulent business environments, innovative behavior is critical to the long-term survival and growth of an organization. This study investigates the effect of being trusted by coworkers on an individual’s innovative behavior. Based on the social network perspective, we develop hypotheses regarding the effects of being trusted on employees’ innovative behavior in two dimensions of the trust relationship in a work team: competence-based trust from work-related abilities and compassion-based trust from emotional bonds between Coworkers. We also examine the moderating role of leader-member exchange differentiation (LMXD) as an upper-level context influencing trust networks and employees’ innovative behavior. For this, we collected data from 102 employees from 19 teams in 10 Korean firms and tested our research model using hierarchical linear modeling (HLM). Our results reveal the positive effect of receiving competence-based trust on innovative behavior. However, contrary to our expectations, being trusted in compassion-based trust relationships has no significant effect on employees’ innovative behavior. Moreover, results of this study show different moderation effects of LMXD alongside the two types of trust. All in all, LMXD mitigates the positive effects of competence-based trust but strengthens the negative effects of compassion-based trust on employees’ innovative behavior. We go on to discuss the theoretical and practical implications of these findings.
Learning English through YouTube videos to foster speaking skills: Public Administration students’ perceptions
Authors: Sholikhi Fu'ad
Published: June 2023

Many teachers use YouTube as an internet-based application to share their areas of expertise, such as sharing writing skills, English pronunciation, English speaking, and so on. In this research, the lecturer uses YouTube as an audiovisual application to help Public Administration students learn English speaking. This research fills the gap of previous research in higher education, precisely about learning to support their careers in the near future. This research aims to understand YouTube as a medium for speaking English based on Public Administration students’ perceptions in class. Therefore, the qualitative method was ideal to answer the purpose of the research. This study involved 15 students, and the researcher served as the primary instrument because of his capacity to provide clarity about the phenomenon utilizing questionnaires and semi-structured interviews. The finding showed that YouTube was the right tool to support their speaking skill. YouTube enhances students’ understanding of Public Interest vocabulary. However, a stable internet connection was the most common problem in learning. Furthermore, there must be similar research in the Department of Elementary School Teacher Education to fill the gap in this research and enrich the understanding of English-speaking skills.
A Modified Algorithms for New Krasnoselskii's Type for Strongly Monotone and Lipschitz Mappings
Authors: Mendy Furmose , Mendy John T
Published: June 2023

Let E be a 2 uniformly smooth and convex real Banach space and let a mapping A: E → E∗ be lipschitz and strongly monotone such that A−1(0)≠∅. For an arbitrary ({x1}, {y1})∈E, we define the sequences {xn} and {yn} byyn = xn − θnJ−1(Axn), n≥1xn+1 = yn − λnJ−1(Ayn), n≥1where λn and θn are positive real number and J is the duality mapping of E. Letting (λn, θn)∈(0, 1), then xn and yn converges strongly to ρ∗, a unique solution of the equation Ax = 0. We also applied our algorithm in convex minimization and also proved the convergence of it in Lp, lp or Wm,p. At the end we proposed the algorithm of it in Lp(Ω) and its inverse Lq(Ω).
TPACK-based HOTS in Teaching Writing for Promoting EFL Learning Quality on Higher Education: Applying “Program Merdeka Belajar – Kampus Merdeka and Kurikulum Paradikma Baru”
Authors: Waluyo Bagus , Nahdiyah Umi , Fahriana Cholida Indrian
Published: June 2023

The purpose of the study is to describe the technology on TPACK-based HOTS applied by lecturers of a suburban university in teaching writing, and its challenge faced in-class interaction. Four English lecturers from Universitas Nahdlatul Ulama Blitar in Indonesia are the participants selected using the purposive sampling design. The process of data collection uses depth interviewing through the online system. Data are analyzed using a "holistic" viewpoint in case study. The results revealed that simple technology dominates the general interactions when teaching writing. Some lecturers may only have a basic understanding of utilizing technology to teach writing. Even they still favour using manual teaching. Because the internet network is poor, few students have technology equipment like laptops, and the interaction is tedious because students are unfamiliar with the technology. It is better that the government, schools, the community, and the primary critical holders for learning must work together in determining policies in the face of changes to use technology in all aspects of school interaction.
Silver and Culinary MSMEs Assistance in the Purbayan Tourism Village through Synergized Promotional Design
Authors: Wiyatiningsih Wiyatiningsih , Oentoro Kristian , Satwikasanti Winta Tridhatu , Mahendra Marcellino Aditya
Published: June 2023

Purbayan Tourism Village is one of 17 tourist villages that received a decree from the Yogyakarta City Government, located in Kotagede. This area has a unique cultural potential that exhibits both historical and cultural wealth  in the form of traditions that exist even today. These traditions include traditional culinary arts, silversmithing and batik craft. However, the potential of this cultural heritage is not visible when compared to the development of the Purbayan Tourism Village. Promotional efforts from business groups and tourism are lacking synergy. Based on these problems, this community service activity aims to assist Micro, Small and Medium Enterprises (MSMEs) to design synergistic tourism promotions. MSMEs that became community service partners are Kopi Lumbung Mataram culinary shop and Studio 76  silver art school. The implementation of this activity uses a user-centered approach to design thinking. In this method, partners as users are actively involved in Focus Group Discussions and workshops on content design and tourism promotion strategies in synergy. The activities described in this paper are understanding, observing, defining point of view, and ideation phase of design thinking. The activity resulted in the promotion concept of Studio 76 silver art school in the form of a draft booth design for silver making exhibitions and photography designs for culinary products of Warung Kopi Lumbung Mataram. Promotion synergy between the two MSMEs is carried out by combining the two tourism service products into an interactive exhibition. The collaboration of these MSME’s aims to promote and increase the number of visitors to the area.
Introdução à modernidade
Authors: Ribeiro Débora , Melo Alessandro de
Published: June 2023

O objetivo deste artigo é trazer duas visões da modernidade, uma a partir de dentro, que a compreende como emancipação, racionalidade, progresso, desenvolvimento etc. A outra visão parte de pensadores decoloniais e traz a perspectiva da modernidade como colonialidade, que oculta a irracionalidade violenta do processo colonial, o qual dá início à modernidade. Por fim, algumas discussões sobre epistemicídio, conhecimento e branquitude são levantadas.
Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties
Authors: Tušil Jan , Serbanuta Traian , Obdrzalek Jan
Published: June 2023

We introduce a language-parametric calculus for k-safety verification - Cartesian Reach- ability logic (CRL).

In recent years, formal verification of hyperproperties has become an important topic in the formal methods community. An interesting class of hyperproperties is known as k-safety properties, which express the absence of a bad k-tuple of execution traces. Many security policies, such as noninterference, and functional properties, such as commutativity, monotonicity, and transitivity, are k-safety properties. A prominent example of a logic that can reason about k-safety properties of software systems is Cartesian Hoare logic (CHL). However, CHL targets a specific, small imperative language. In order to use it for sound verification of programs in a different language, one needs to extend it with the desired features or hand-craft a translation. Both these approaches require a lot of tedious, error- prone work.

Unlike CHL, CRL is language-parametric: it can be instantiated with an operational semantics (of a certain kind) of any deterministic language. Its soundness theorem is proved once and for all, with no need to adapt or re-prove it for different languages or their variants. This approach can significantly reduce the development costs of tools and techniques for sound k-safety verification of programs in deterministic languages: for exam- ple, of smart contracts written for EVM (the language powering the Ethereum blockchain), which already has an operational semantics serving as a reference.
Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic
Authors: Steen Alexander , Sutcliffe Geoff , Fontaine Pascal , McKeown Jack
Published: June 2023

This paper describes a new format for representing Tarskian-style interpretations for formulae in typed first-order logic, using the TPTP TF0 language. It further describes a technique and an implemented tool for verifying models using this representation, and a tool for visualizing interpretations. The research contributes to the advancement of au- tomated reasoning technology for model finding, which has several applications, including verification.
How Much Should This Symbol Weigh? A GNN-Advised Clause Selection
Authors: Bártek Filip , Suda Martin
Published: June 2023

Clause selection plays a crucial role in modern saturation-based automatic theorem provers. A commonly used heuristic suggests prioritizing small clauses, i.e., clauses with few symbol occurrences. More generally, we can give preference to clauses with a low weighted symbol occurrence count, where each symbol’s occurrence count is multiplied by a respective symbol weight. Traditionally, a human domain expert would supply the symbol weights.

In this paper, we propose a system based on a graph neural network that learns to predict symbol weights with the aim of improving clause selection for arbitrary first-order logic problems. Our experiments demonstrate that by advising the automatic theorem prover Vampire on the first-order fragment of TPTP using a trained neural network, the prover’s problem solving capability improves by 6.6% compared to uniformly weighting symbols and by 2.1% compared to a goal-directed variant of the uniformly weighting strategy.
Scalable Probabilistic Routes
Authors: Yang Suwei , Liang Victor , Meel Kuldeep S.
Published: June 2023

Inference and prediction of routes have become of interest over the past decade owing to a dramatic increase in package delivery and ride-sharing services. Given the underlying combinatorial structure and the incorporation of probabilities, route prediction involves techniques from both formal methods and machine learning. One promising approach for predicting routes uses decision diagrams that are augmented with probability values. However, the effectiveness of this approach depends on the size of the compiled decision diagrams. The scalability of the approach is limited owing to its empirical runtime and space complexity. In this work, our contributions are two-fold: first, we introduce a relaxed encoding that uses a linear number of variables with respect to the number of vertices in a road network graph to significantly reduce the size of resultant decision diagrams. Secondly, instead of a stepwise sampling procedure, we propose a single pass sampling-based route prediction. In our evaluations arising from a real-world road network, we demonstrate that the resulting system achieves around twice the quality of suggested routes while being an order of magnitude faster compared to state-of-the-art.
Formalization of Algebraic Theorems in PVS (Invited Talk)
Authors: Ayala-Rincón Mauricio , Arielly de Lima Thaynara , Avelar Andréia B. , Galdino André Luiz
Published: June 2023

This talk discusses current extensions on the theory algebra from the NASA/PVSlibrary on formal developments for the Prototype Verification System (PVS). It discusses the approach to formalizing theorems of the ring theory and how they are applied to infer properties of specific algebraic structures. As cases of study, we will present recent formalizations on the theories of Euclidean Domains and Quaternions. Moreover, we will show how a general verification of Euclid’s division algorithm can be specialized to verify this algorithm for specific Euclidean Domains, and how the abstract theory of Quaternions can be parameterized to deal with the structure of Hamilton’s Quaternions.
Syntactic computation of Fagin-Halpern conditioning in possibility theory
Authors: Ettarguy Omar , Begdouri Ahlame , Benferhat Salem , Delenne Carole
Published: June 2023

Conditioning plays an important role in revising uncertain information in light of new evidence. This work focuses on the study of Fagin and Halpern (FH-)conditioning in the context where uncertain information is represented by weighted or possibilistic belief bases. Weighted belief bases are extensions of classical logic belief bases where a weight or degree of belief is associated with each propositional logic formula. This paper proposes a characterization of a syntactic computation of the revision of weighted belief bases (in the light of new information) which is in full agreement with the semantics of the FH- conditioning of possibilistic distributions. We show that the size of the revised belief base is linear with respect to the size of the initial base and that the computational complexity amounts to performing O(log2(n)) calls to the propositional logic satisfiability tests, where n is the number of different degrees of certainty used in the initial belief base.
Embedding Intuitionistic into Classical Logic
Authors: Pluska Alexander , Zuleger Florian
Published: June 2023

The famous double negation translation [16, 17] establishes an embedding of classical into intuitionistic logic. Curiously, the reverse direction has not been covered in literature. Utilizing a normal form for intuitionistic logic [20], we establish a small model property for intuitionistic propositional logic. We use this property for a direct encoding of the Kripke semantics into classical propositional logic and quantified Boolean formulae. Next, we transfer the developed techniques to the first order case and provide an embedding of intuitionistic first-order logic into classical first-order-logic. Our goal here is an encoding that facilitates the use of state-of-the-art provers for classical first-order logic for deter- mining intuitionistic validity. In an experimental evaluation, we show that our approach can compete with state-of-the-art provers for certain classes of benchmarks, in particular when the intuitionistic content is low. We further note that our constructions support the transfer of counter-models to validity, which is a desired feature in model checking applications.
A Mathematical Benchmark for Inductive Theorem Provers
Authors: Gauthier Thibault , Brown Chad , Janota Mikoláš , Urban Josef
Published: June 2023

We present a benchmark of 29687 problems derived from the On-Line Encyclopedia of Integer Sequences (OEIS). Each problem expresses the equivalence of two syntactically different programs generating the same OEIS sequence. Such programs were conjectured by a learning-guided synthesis system using a language with looping operators. The operators implement recursion, and thus many of the proofs require induction on natural numbers. The benchmark contains problems of varying difficulty from a wide area of mathematical domains. We believe that these characteristics will make it an effective judge for the progress of inductive theorem provers in this domain for years to come.
Toward Optimal Radio Colorings of Hypercubes via SAT-solving
Authors: Subercaseaux Bernardo , Heule Marijn
Published: June 2023

Radio 2-colorings of graphs are a generalization of vertex colorings motivated by the problem of assigning frequency channels in radio networks. In a radio 2-coloring of a graph, vertices are assigned integer colors so that the color of two vertices u and v differ by at least 2 if u and v are neighbors, and by at least 1 if u and v have a common neighbor. Our work improves the best-known bounds for optimal radio 2-colorings of small hypercube graphs, a combinatorial problem that has received significant attention in the past. We do so by using automated reasoning techniques such as symmetry breaking and Cube and Conquer, obtaining that for n = 7 and n = 8, the coding-theory upper bounds of Whittlesey et al. (1995) are not tight. Moreover, we prove the answer for n = 7 to be either 12 or 13, thus making a substantial step towards answering an open problem by Knuth (2015). Finally, we include several combinatorial observations that might be useful for further progress, while also arguing that fully determining the answer for n = 7 will require new techniques.
Experiments on Infinite Model Finding in SMT Solving
Authors: Parsert Julian , Brown Chad , Janota Mikolas , Kaliszyk Cezary
Published: June 2023

We propose infinite model finding as a new task for SMT-Solving. Model finding has a long-standing tradition in SMT and automated reasoning in general. Yet, most of the current tools are limited to finite models despite the fact that many theories only admit infinite models. This paper shows a variety of such problems and evaluates synthesis approaches on them. Interestingly, state-of-the-art SMT solvers fail even on very small and simple problems. We target such problems by SyGuS tools as well as heuristic approaches.
Trace-based Deductive Verification
Authors: Bubel Richard , Gurov Dilian , Hähnle Reiner , Scaletta Marco
Published: June 2023

Contracts specifying a procedure’s behavior in terms of pre- and postconditions are essential for scalable software verification, but cannot express any constraints on the events occurring during execution of the procedure. This necessitates to annotate code with intermediate assertions, preventing full specification abstraction.

We propose a logic over symbolic traces able to specify recursive procedures in a mod- ular manner that refers to specified programs only in terms of events. We also provide a deduction system based on symbolic execution and induction that we prove to be sound relative to a trace semantics.

Our work generalizes contract-based to trace-based deductive verification by extending the notion of state-based contracts to trace-based contracts.
Keep me out of the loop: a more flexible choreographic projection
Authors: Cruz-Filipe Luís , Montesi Fabrizio , Rasmussen Robert R.
Published: June 2023

Choreographic programming is a paradigm where programmers write global descrip- tions of distributed protocols, called choreographies, and correct implementations are au- tomatically generated by a mechanism called projection. Not all choreographies are pro- jectable, because decisions made by one process must be communicated to other processes whose behaviour depends on them – a property known as knowledge of choice.

The standard formulation of knowledge of choice disallows protocols such as third-party authentication with retries, where two processes iteratively interact, and other processes wait to be notified at the end of this loop. In this work we show how knowledge of choice can be weakened, extending the class of projectable choreographies with these and other interesting behaviours. The whole development is formalised in Coq. Working with a proof assistant was crucial to our development, because of the help it provided with detecting counterintuitive edge cases that would otherwise have gone unnoticed.
Evaluation of the psychological distress and mental well-being of pre-hospital care providers in Saudi Arabia during COVID-19
Authors: Alghamdi Abdulrhman , Alharbi Meshal , Alshibani Abdullah , Allohidan Fahad , Alabdali Abdullah , Aljerian Nawfal
Published: June 2023

Background:Pre-hospital care providers are the first line of contact when emergencies occur. They are at high risk of mental health disorders associated with trauma and stress. The magnitude of their stress could increase during difficult times such as the COVID-19 pandemic.Objectives:This study reports on the state of mental well-being and the degree of psychological distress among pre-hospital care workers (paramedics, emergency medical technicians, doctors, paramedic interns and other healthcare practitioners) during the COVID-19 pandemic in Saudi Arabia.Methods:The study was a cross-sectional survey study in Saudi Arabia. A questionnaire was distributed among pre-hospital care workers in Saudi Arabia during the first wave of the COVID-19 pandemic. The questionnaire was based on the Kessler Psychological Distress Scale (K10) and the World Health Organization Well-Being Index (WHO-5).Results:In total, 427 pre-hospital care providers completed the questionnaire; 60% of the respondents had scores of more than 30 in the K10 and were likely to have a severe disorder. The WHO-5 showed a similar percentage of respondents with a score of more than 50 and coded as having poor well-being.Conclusions:The findings of this study provide evidence around mental health and well-being for pre-hospital care workers. They also highlight the need to better understand the quality of mental health and well-being for this population and to provide appropriate interventions to improve their quality of life.
PROPOSTA DE UM MODELO DIGITAL DE RECONCILIAÇÃO TERAPÊUTICA COM RECURSO A BLOCKCHAIN E INTELIGÊNCIA ARTIFICIAL
Authors: Albuquerque Ricardo , Sardinha Luís , Albuquerque Susana , Romana Maria , Leite Eduardo , Fragoeiro Isabel
Published: June 2023

O Registo de Saúde Eletrónico (RSE) é o resultado da mudança do atual sistema de saúde, influenciado pela inovação, integração e partilha de dados clínicos. O RSE deve incluir sumário clínico dos pacientes, prescrições eletrónicas, registo eletrónico de dispensa de medicação, resultados laboratoriais, imagens e/ou relatórios médicos e notas de alta hospitalar. A prescrição médica e a administração de terapêutica são dos erros evitáveis mais comuns em Saúde, a sexta maior causa de morte nos EUA e uma prioridade para a Organização Mundial de Saúde desde que lançou a iniciativa “Medication Without Harm”. Os objetivos deste trabalho são: i) apresentar um modelo digital de reconciliação terapêutica; ii) propor uma solução interoperável e legalmente conforme; iii) integrar a tecnologia Blockchain e Inteligência Artificial no modelo apresentado. Através de uma revisão bibliográfica descritiva e exploratória, propôs-se a utilização dos “standards” HL7 FHIR e SNOMED-CT, modelo “client-CA” para a Blockchain e modelos de “machine learning” e “natural language processing” para a Inteligência Artificial. É complexo garantir a transmissão de dados clínicos de forma interoperável e segura, mas teoricamente exequível. As vantagens ao nível da reconciliação terapêutica serão mensuráveis com a contínua diminuição da morbimortalidade associada ao erro terapêutico.
EFISIENSI PROSES FINANCIAL CLOSING PADA OPERASIONAL MONTH-END CLOSING INDUSTRI REFINERY (STUDI KASUS: PT XYZ)
Authors: Hidayat Septian , Saputra Muhardi , Puspitasari Warih
Published: June 2023

Tingginya produksi minyak sawit olahan (CPO) di Indonesia menuntut perusahaan untuk dapat menyeimbangkan kegiatan operasional yang melibatkan banyak alat penunjang produksi. Dengan besarnya kegiatan operasional tersebut berdampak pada banyaknya data yang harus dikumpulkan pada akhir periode keuangan dalam proses financial closing. sehingga dalam hal ini perusahaan seringkali mengalami keterlambatan proses financial closing yang diakibatkan lamanya proses record material balance dari warehouse ke dalam sistem, selain itu masih terdapat proses yang dilakukan secara manual, hal ini tentu berdampak pada keterlambatan pembukuan keuangan baru pada periode berikutnya karena adanya inkonsistensi data pada sistem yang ada dengan warehouse. Oleh karena itu, penelitian ini mempercepat proses financial closing, sehingga perusahaan dapat membuka pembukuan keuangan baru pada periode berikutnya. Penelitian ini menggunakan metode Service Engineering Methodology (SEEM) dalam menyelesaikan permasalahan tersebut, dengan mengikuti tahapan-tahapan pada metode tersebut diharapkan mampu menjawab permasalahan dengan output rancangan perbaikan alur proses bisnis dan konfigurasi sistem SAP yang ada di perusahaan. Hasil dari sistem konfigurasi ini akan membantu pengguna menjaga konsistensi data dan mempercepat proses penutupan keuangan dengan program otoma-tisasi. Hasil dari penelitian ini yakni aktivitas financial closing menjadi lebih cepat karena pembuatan fitur yang meng-gantikan kegiatan yang masih dilakukan secara manual tiap bulannya dan pembuatan pengaturan dari permission nega-tive stocks allowance yang memudahkan user melakukan closing terlebih dahulu tanpa harus menunggu balance dari ma-terial pada proses maintenance.
ANALYSIS OF THE EFFECT OF VSM ON THE MEMORY ACQUISITION PROCESS USING THE DYNAMIC ANALYSIS METHOD
Authors: Maulina Sinta Nur , Cahyani Niken Dwi Wahyu , Jadied Erwid Musthofa
Published: June 2023

At first, forensics was restricted to studying data that was stored on a system's hard disk. However, as storage capacity and data encryption increased, applying conventional digital forensic procedures became more challenging. As a result, memory forensics techniques are developed, or are frequently referred to as live forensics, because the process is quicker and more sophisticated. Volatile memory forensics, often known as live forensics, are necessary for this condition. Live forensics has flaws, specifically that some programs can fail when the computer is in active VSM (virtual secure mode). This results in the retrievable evidence being lost. Therefore, determining the cause is essential. The software-based memory acquisition tools Autopsy, Isobuster, DumpIt, and Magnet RAM Capturer are just a few examples. According to the findings of the experiments, the tools that have crashed include DumpIt v1.3.2.20110401. A dynamic code analysis using WindBg as a tool was utilized to study the impact of VSM on the memory acquisition tool. This study's goal is to identify the instances of crashes in various forensic instruments, which will be highly useful for forensic experts performing investigations.