bluuebunny/crossref_metadata_2025_split huggingface dataset:
Fractal Sets as Final Coalgebras Obtained by Completing an Initial Algebra
Authors: Moss Larry , Ratnayake Jayampathy , Rose Robert 
Published: January 2018

This paper is a contribution to the presentation of fractal sets in terms of final coalgebras.The first result on this topic was Freyd's Theorem: the unit interval [0,1] is the final coalgebra ofa certain functor on the category of bipointed sets. Leinster 2011 offersa sweeping generalization of this result. He is able to represent many of what would be intuitivelycalled "self-similar" spaces using (a) bimodules (also called profunctors or distributors),(b) an examination of non-degeneracy conditions on functors of various sorts; (c) a construction offinal coalgebras for the types of functors of interest using a notion of resolution. In addition to thecharacterization of fractals sets as sets, his seminal paper also characterizes them as topological spaces.Our major contribution is to suggest that in many cases of interest, point (c) above on resolutionsis not needed in the construction of final coalgebras. Instead, one may obtain a number of spaces ofinterest as the Cauchy completion of an initial algebra,and this initial algebra is the set of points in a colimit of an omega-sequence of finite metric spaces.This generalizes Hutchinson's 1981 characterization of fractal attractors asclosures of the orbits of the critical points. In addition to simplifying the overall machinery, it also presents a metric space which is ``computationally related'' to the overall fractal. For example, when applied to Freyd's construction, our method yields the metric space.of dyadic rational numbers in [0,1].Our second contribution is not completed at this time, but it is a set of results on \emph{metric space}characterizations of final coalgebras. This point was raised as an open issue in Hasuo, Jacobs, and Niqui 2010,and our interest in quotient metrics comes from their paper. So in terms of (a)--(c) above, our workdevelops (a) and (b) in metric settings while dropping (c).
Deep Incremental Boosting
Authors: Mosca Alan , Magoulas George 
Published: January 2018

This paper introduces Deep Incremental Boosting, a new technique derived from AdaBoost, specifically adapted to work with Deep Learning methods, that reduces the required training time and improves generalisation. We draw inspiration from Transfer of Learning approaches to reduce the start-up time to training each incremental Ensemble member. We show a set of experiments that outlines some preliminary results on some common Deep Learning datasets and discuss the potential improvements Deep Incremental Boosting brings to traditional Ensemble methodsin Deep Learning.
Automatic Inference of Term Equivalence in Term Rewriting Systems
Authors: Comini Marco , Torella Luca 
Published: January 2018

In this paper we propose a parametric technique to automatically infer algebraic property-oriented specifications from Term Rewriting Systems. Namely, given the source code of a TRS we infer a specification which consists of a set of most general equations relating terms that rewrite, for all possible instantiations, to the same set of normal forms.The semantic-based inference method that we propose can cope with non-constructor-based TRSs, and considers non-ground terms. Particular emphasis is posed to avoid the generation of “redundant” equations that can be a logical consequence of other ones.To experiment on the validity of our proposal we have considered an instance of the method employing a novel (condensed) semantics for left-linear TRSs and we have implemented a “proof of concept” prototype in Haskell which is available online.
Efficient Rule-Matching for Hyper-Tableaux
Authors: Holen Bjarne , Hovland Dag , Giese Martin 
Published: January 2018

Over the past decades, a number of calculi for automatedreasoning have been proposed that share some core features:1. proofs are built in a tableau/sequent style as trees wherenodes are labeled with literals, and 2. these proofs are expandedby interpreting the problem clause set as a set of rules, andrequiring all negative literals in clauses to present on a branchfor expansion. This applies to hyper-tableaux, MGTP, coherentlogic, and others. Existing implementations typically spend muchof their time in the process of matching branch literals with thenegative literals of the input clauses. We present analternative to this matching process by applying a modifiedversion of the RETE algorithm. The RETE algorithm was developedin the 1970s for production systems in artificialintelligence. We exploit the similarities between the mentionedcalculi and production systems in order to make the RETEalgorithm solve the matching problem. We also investigate theeffect of working on several independent branches present intableau proof search but not in production systems.
Compiling Hilbert's epsilon operator
Authors: Leino Rustan 
Published: January 2018

Hilbert's epsilon operator is a binder that picks an arbitrary element froma nonempty set. The operator is typically used in logics and proof engines.This paper contributes a discussion of considerations in supporting this operatorin a programming language. More specifically, the paper presents the design choicesmade around supporting this operator in the verification-aware language Dafny.
Applicative Abstract Categorial Grammar
Authors: Kiselyov Oleg 
Published: January 2018

We present the grammar/semantic formalism of Applicative AbstractCategorial Grammar (AACG), based on the recent techniques fromfunctional programming: applicative functors, staged languages andtyped final language embeddings. AACG is a generalization ofAbstract Categorial Grammars (ACG), retaining the benefits of ACG as agrammar formalism and making it possible and convenient to express avariety of semantic theories.We use the AACG formalism to uniformly formulate Potts' analyses ofexpressives, the dynamic-logic account of anaphora, and thecontinuation tower treatment of quantifier strength, quantifierambiguity and scope islands. Carrying out these analyses in ACGrequired compromises and the ballooning of parsing complexity, or wasnot possible at all. The AACG formalism brings modularity, which comesfrom the compositionality of applicative functors, in contrast tomonads, and the extensibility of the typed final embedding. Theseparately developed analyses of expressives and QNP are used as theyare to compute truth conditions of sentences with both these features.AACG is implemented as a `semantic calculator', which is the ordinaryHaskell interpreter. The calculator lets us interactively writegrammar derivations in a linguist-readable form and see their yields,inferred types and computed truth conditions. We easily extendfragments with more lexical items and operators, and experiment withdifferent semantic-mapping assemblies. The mechanization lets asemanticist test more and more complex examples, making empirical testsof a semantic theory more extensive, organized and systematic.
Initial Experiments with External Provers and Premise Selection on HOL Light Corpora
Authors: Kaliszyk Cezary , Urban Josef 
Published: January 2018

This paper reports our initial experiments withusing external ATP and premise selection methodson some corpora built with the HOL Light system.The testing is done in three different settings,corresponding to those used earlier for evaluatingsuch methods on the Mizar/MML corpus.This is intended to provide the first estimate aboutthe usefulness of such external reasoning and AI systems forsolving problems over HOL Light and its libraries.
Local Driving in Higher-Order Positive Supercompilation via the Omega-theorem
Authors: Hamilton Geoff , Sørensen Morten Heine 
Published: January 2018

A program transformation technique should terminate, return efficient output programs and be efficient itself.For positive supercompilation ensuring termination requires memoisation of expressions, and these are subsequently used to determine when to perform generalization and folding. For a first-order language, every infinitesequence of transformation steps must include function unfolding, so it is sufficient to memoise only those expressions immediately prior to a function unfolding step.However, for a higher-order language, it is possible for an expression to have an infinite sequence of transformation steps which do not include function unfolding, so memoisation prior to a function unfolding step is not sufficient by itselfto ensure termination. But memoising additional expressions is expensive during transformation and may lead to less efficient output programs due to auxiliary functions. This additional memoisation may happen explicitly during transformationor implicitly via a pre-processing transformation as outlined in previous work by the first author.We introduce a new technique for local driving in higher-order positive supercompilation which obliviates the need for memoising other expressions than function unfolding steps, thereby improving efficiency of both the transformation and the generated programs. We exploit the fact, due to the second author in the setting of type-free lambda-calculus that every expression with an infinite sequence of transformation steps not involving function unfolding must have somthing like the term Omega = (lambda x. x x) (lambda x . x x) embedded within it in a certain sense. The technique has proven useful on a host of examples.
Abstractions Before Proofs
Authors: Jones Cliff 
Published: January 2018

Proving that programs satisfy their specifications can benefit enormously from tool support but theorem proving tools can also constrain a user's thinking. This talk argues that, for large or complex programs, it is layers of abstraction that make or break the comprehensibility of developments.However powerful a theorem proving tool is, it will make little long-term contribution to the understanding of programs if the user is forced to bend their steps of development to fit the tool. Abstraction is essential to achieve separation of issues and to help in the understanding of complex systems. The formalism chosen governs the difficulty of completing detailed proofs that can be verified with mechanically checkable rules.This talk will emphasize abstractions and techniques for reasoning about the development of concurrent programs. In conclusion, the argument will turn to positive recommendations for tool developers.
Walker's Cancellation Theorem
Authors: Lubarsky Robert , Richman Fred 
Published: January 2018

Walker's cancellation theorem says that if B + Z isisomorphic to C + Z in the category of abeliangroups, then B is isomorphic to C. We construct an example ina diagram category of abelian groups where the theorem fails. As aconsequence, the original theorem does not have a constructiveproof. In fact, in our example B and C are subgroups ofZ&lt;sup&gt;2&lt;/sup&gt;. Both of these results contrast with a group whoseendomorphism ring has stable range one, which allows aconstructive proof of cancellation and also a proof in any diagramcategory.
SMT-LIB Sequences and Regular Expressions
Authors: Bjorner Nikolaj , Ganesh Vijay , Michel Raphaël , Veanes Margus 
Published: January 2018

Strings are ubiquitous in software. Tools for specification,verification and test-case generation of software rely in various degrees onrepresenting and reasoning about strings. Reasoning about strings isparticularly important in several security critical applications, such asweb sanitizers. Besides a basic representation of strings, applicationsalso use string recognizers and transducers.This paper presents a proposal for an SMT-LIBization of strings and regularexpressions. It introduces a theory of sequences, generalizing strings,and builds a theory of regular experssions on top of sequences.The logic QF_BVRE is designed to capture a common substrate amongexisting tools for string constraint solving.
Things You Can't do With a Vampire
Authors: Sutcliffe Geoff 
Published: January 2018

The Vampire ATP system has been very successful at proving theorems infirst-order logic.Vampire has won the FOF division of CASC for all except one of the last 15years, and many papers highlighting Vampire's strengths have been published.This talk examines the flip side of the Vampire coin ... what kinds ofproblems are difficult or even impossible for the latest incarnation ofVampire.The talk will help users decide when to use Vampire, and when to use anotherATP system, will help the Vampire developers direct their work, and providesthe data required to build a portfolio ATP system with Vampire as a component.
Engineering Theories with Z3
Authors: Bjorner Nikolaj 
Published: January 2018

Modern Satisfiability Modulo Theories (SMT)solvers are fundamental to many programanalysis, verification, design and testing tools. They are a goodfit for the domain of software and hardware engineering becausethey support many domains that are commonly used by the tools.The meaning of domains are captured by theories that can beaxiomatized or supported by efficient &lt;i&gt;theory solvers&lt;/i&gt;.Nevertheless, not all domains are handled by all solvers andmany domains and theories will never be native to any solver.We here explore different theories that extend MicrosoftResearch's SMT solver Z3's basicsupport. Some can be directly encoded or axiomatized,others make use of user theory plug-ins.Plug-ins are a powerful way for tools to supply their custom domains.
Networked Cooperative Platoon of Vehicles for Testing Methods and Verification Tools
Authors: Ben Makhlouf Ibtissem , Kowalewski Stefan 
Published: January 2018

A practical benchmark for testing analysis and verification methods for continuous as well as hybrid systems is suggested. It consists of a platoon of controlled vehicles. The vehicles exchange information via a communication network that is subject to failure of single nodes or a complete loss of communication. The worst case scenario corresponding to the transition from a fully functioning communication between the vehicles to a total loss of communication is considered in particular. The safety properties of the considered networked platoon are investigated. The system is modeled as a hybrid automaton. The continuous part represents the dynamical behavior of the platoon and thediscrete part are spontaneous events related to the switching communication topology. The proposed example is a linear time invariant system.
Uso de la leña y conservación del bosque en el volcán Huitepec, Chiapas, México
Authors: Santos González Arelí , Estrada Lugo Erin Ingrid Jane , Rivas Lechuga Gerardo 
Published: January 2018

Se analiza la dinámica de uso de leña en ocho colonias alrededor del volcán Huitepec, Chiapas, aledañas a dos áreas naturales protegidas de manejo privado (Reserva Huitepec- Pronatura) y colectivo (Reserva Zapatista), así como a una población urbana creciente: San Cristóbal de las Casas. En la zona de estudio es evidente la preocupación de conservar el bosque, sus recursos naturales y servicios ambientales fundamentales. De acuerdo al uso y manejo de la leña, se tipificaron a las colonias en cuatro categorías: atención prioritaria, atención básica, atención significativa y atención media.
Asentamientos arqueológicos del municipio de las Choapas, Veracruz
Authors: Hernández Jiménez María de Lourdes 
Published: January 2018

Los recorridos extensivos que se derivan de la supervisión de obras sísmicas, paradójicamente suelen ser coyunturales para el conocimiento de una región, como es el caso de la obra de exploración de hidrocarburos, en la cuenca media del río Uxpanapa, cuya cobertura nos permitió registrar una serie de asentamientos prehispánicos que datan desde el preclásico olmeca hasta el Posclásico. Esta región, al estar ubicada en el centro del istmo y contener una red hidrológica amplia, permitió el desarrollo y los movimientos poblacionales entre la costa de Golfo y del Pacífico.
Refresco y diabetes entre los mayas de Tenejapa, San Cristóbal de Las Casas y Chamula, Chiapas
Authors: Page Pliego Jaime Tomás 
Published: January 2018

Este trabajo aborda factores asociados a la importancia Del consumo de refresco, específicamente de Coca-Cola, entre los mayas que habitan en las cabeceras municipales de Tenejapa, Chamula y San Cristóbal de Las Casas, Chiapas, en la obesidad y la diabetes. Los datos de campo arrojan cómo la situación de un número considerable de diabéticos y sus familiares sin antecedentes previos de diabetes se vincula a un intenso consumo de refresco previo a la aparición de la sintomatología. Se revisan las representaciones que los mayas construyen en torno a dicha problemática.
Entre apatía y colaboración: actitudes hacia las escuelas rurales federales en la región de San Bartolomé de Los Llanos, Chiapas, 1926-1940
Authors: Barrera Aguilera Óscar Javier 
Published: January 2018

Este estudio permite conocer las particularidades del proyecto de escuelas rurales federales â€”impulsado por la Secretaría de Educación Públicaâ€” en poblaciones ubicadas en las terrazas en el valle central del río Grijalva en el estado de Chiapas. Para ilustrar las adaptaciones, contrastamos las experiencias que el proyecto afrontó en comunidades tseltales, como Amatenango del Valle y Aguacatenango, y poblaciones mestizas, como Teopisca, Tzimol y Socoltenango. Los casos analizados nos permiten preguntarnos por los conflictos de intereses que surgieron entre las comunidades, los maestros y las autoridades a raíz de la implementación de este proyecto educativo.
Video indígena y antropología compartida: una experiencia colaborativa con videastas maya-q'eqchi' de Guatemala
Authors: Flores Carlos Y. 
Published: January 2018

El documento analiza las condiciones subjetivas e históricas que sirvieron de contexto para una producción colaborativa entre videastas locales, sus comunidades y mi propia práctica como antropólogo visual. También evalúa algunas de las implicaciones que este experimento tuvo entre los participantes.
El lugar que ocupa el trabajo en los jóvenes mexicanos
Authors: Leyva Piña Marco Antonio , Rodríguez Lagunas Javier 
Published: January 2018

En este texto se pone el énfasis en una interrogante ¿para los jóvenes mexicanos el trabajo es un referente básico en la organización de su vida en la sociedad? Esta interrogante resultapertinente en el marco de las discusiones respecto al cuestionamiento del trabajo como eje de la construcción de las relaciones sociales. Con base en la Encuesta Nacional de Empleo Urbano y la Encuesta Nacional de la Juventud, se plantea la situación laboral de los jóvenes mexicanos caracterizada por la precarización del empleo.
Mesoamérica o el Proyecto Mesoamérica: la historia como pretexto
Authors: Capdepont Ballina Jorge Luis 
Published: January 2018

Este trabajo se centra en el análisis del contexto histórico en el cual se inserta el Proyecto Mesoamérica, poniendo en duda la versión oficial de que es una propuesta que pretende abatir los índices de rezago económico y social del sur-sureste de México y Centroamérica, cuando todo parece indicar que es uno más de los intentos por aprovechar la ubicación estratégica de la región y sus valiosos recursos naturales en beneficio de las grandes potencias mundiales, sobre todo Estados Unidos.
¿Unión y libertad? El intento de unión de El Petén a Yucatán en 1823
Authors: Caso Barrera Laura 
Published: January 2018

Con el análisis de fuentes documentales, se pretende dar a conocer cómo el distrito de El Petén, bajo la administración política de la Audiencia de Guatemala, intentó en 1823 formar parte de la provincia de Yucatán. Se analizan tanto el discurso original y los argumentos utilizados por la élite petenera para intentar unirse a Yucatán, así como la radical transformación del discurso cuando se inició la rebelión maya conocida como Guerra de Castas. El surgimiento de la rebelión indígena hizo que la élite petenera decidiera poner punto final a la idea de formar parte de Yucatán.
Impacto de descortezadores en el incremento radial de Pinus teocote Schiede. ex Schltdl. & Cham. y Pseudotsuga menziesii (Mirb.) Franco
Authors: López Sánchez Jesús Ángel , Méndez González Jorge , Zermeño González Alejandro , Cerano Paredes Julián , García Aranda Mario Alberto 
Published: January 2018

Los estudios dendrocronológicos permiten datar sucesos importantes que influyen en el crecimiento de un árbol. El objetivo del presente estudio fue comparar, a través de técnicas dendrocronológicas, el impacto de insectos descortezadores sobre el crecimiento radial en Pinus teocote (Pt) y Pseudotsuga menziesii (Pm). Para ello se analizaron núcleos de crecimiento de 52 árboles de Pt (26 sanos y 26 infestados) y 72 de Pm (36 sanos y 36 infestados), de dos sitios ubicados en la Sierra Madre Oriental. Los datos analizados fueron: ancho de anillo e índice del ancho de anillo, de toda la cronología, pero también antes y después de la aparición de la plaga. Mediante pruebas de t de Student se constrastó el ancho de anillo de árboles (sanos e infestados) antes y después del ataque de insectos descortezadores. El incremento radial acumulado en Pt fue mayor en árboles infestados (1.86 mm año-1) que en los individuos sanos (1.30 mm año-1); en Pm, los árboles sanos incrementaron más (3.01 mm año-1) que los infestados (1.81 mm año-1). Se concluye que cada especie responde de forma diferente al ataque de insectos descortezadores, y esto parece ser una forma de preservar la especie. La dendrocronología es una herramienta útil para evaluar la productividad de los bosques, ya que arroja datos precisos de edad e incremento anual de los árboles.
Manejo integral del paisaje para la adaptación al cambio climático en la Sierra Madre de Chiapas, México
Authors: López Báez Walter , Reynoso Santos Roberto 
Published: January 2018

Con el fin de mitigar y mejorar la capacidad de adaptación al cambio climático (CC) de la población y los ecosistemas en la Sierra Madre de Chiapas se implementó una propuesta integrada, que incluye los componentes: (i) la gestión integral del desarrollo; (ii) la cuenca hidrográfica como unidad de planificación; (iii) un proceso de planeación que incluye las necesidades de las familia, los medios de vida, la base de recursos naturales, el suministro de servicios ecosistémicos y los efectos del CC; (iv) el desarrollo de los capitales humano y social; y (v) un mecanismo de financiamiento público y privado. De 2010 hasta el día que se han realizado diagnósticos participativos, talleres de capacitación, acuerdos comunitarios e intercomunitarios de conservación, restauración de bosques, mejoramiento productivo del maíz, frijol y café, pagos por servicios ambientales proteger el bosque natural, zonificación de las zonas con riesgo de desastre, monitoreo de la calidad del agua y se creó el grupo intercomunitario de acción territorial (GIAT). Los resultados confirman que la adaptación al CC debe ser de carácter integral, territorial y construido con la población local. El mecanismo financiero público-privado garantiza oportunidad y continuidad en el desarrollo de las acciones y potencia la acción del gobierno.

El enfoque de cuencas permite una planificación más eficiente y la implementación de las acciones teniendo en cuenta la relación entre las zonas altas y bajas de la cuenca, así como identificar las interacciones entre los servicios de los ecosistemas diferentes que ofrece el territorio.