bluuebunny/crossref_metadata_2025_split huggingface dataset:
Escape to Mizar from ATPs
Authors: Alama Jesse 
Published: January 2018

We announce a tool for mapping derivations produced by the E theoremprover to Mizar proofs. Our mapping complements earlier work thatgenerates problems for automated theorem provers from Mizar inferencechecking problems. We describe the tool, explain the mapping, andshow how we solved some of the difficulties that arise in mappingproofs between different logical formalisms, even when they are basedon the same notion of logical consequence, as Mizar and E are (namely,first-order classical logic with identity).
An elementary proof of the completeness of the Lukasiewicz axioms
Authors: Botur Michal , Paseka Jan 
Published: January 2018

The main aim of this talk is twofold. Firstly, to present an elementarymethod based on Farkas' lemma for rationals how to embed any finite partial subalgebraof a linearly ordered MV-algebra into Q \ [0; 1] and then to establish a new elementaryproof of the completeness of the Lukasiewicz axioms for which the MV-algebras communityhas been looking for a long time. Secondly, to present a direct proof of Di Nola'srepresentation Theorem for MV-algebras and to extend his results to the restriction ofthe standard MV-algebra on rational numbers.
MCMT in the Land of Parametrized Timed Automata
Authors: Carioni Alessandro , Ghilardi Silvio , Ranise Silvio 
Published: January 2018

Timed networks are parametrized systems of timed au\-to\-ma\-ta. Solving reachability problems (e.g., whether a set of unsafe states can ever be reached from the set of initial states) for this class of systems allows one to prove safety properties regardless of the number of processes in the network. The difficulty in solving this kind of verification problems is two-fold. First, each process has (at least one) clock variable ranging over an infinite set, such as the reals or the integers. Second, every system is parameterized with respect to the number of processes and to the topology of the network. Reachability problem for some restricted classes of parameterized timed networks is decidable under suitable assumptions by a backward reachability procedure. Despite these theoretical results, there are few systems capable of automatically solving such problems. Instead, the number $n$ of processes in the network is fixed and a tool for timed automata (like Uppaal) is used to check the desired property for the given $n$.In this paper, we explain how to attack fully parameteric and timed reachability problems by translation to the declarative input language of \textsc{mcmt}, a model checker for infinite state systems based on Satisfiability Modulo Theories techniques. We show the success of our approach on a number of standard algorithms, such as the Fischer protocol. Preliminary experiments show that fully parametric problems can be more easily solved by \textsc{mcmt} than their instances for a fixed (and large) number of processes by other systems.
EPR-based k-induction with Counterexample Guided Abstraction Refinement
Authors: Khasidashvili Zurab , Korovin Konstantin , Tsarkov Dmitry 
Published: January 2018

In recent years it was proposed to encode bounded model checking (BMC) into the effectively propositional fragment of first-order logic (EPR). The EPR fragment can provide for a succinct representation of the problem and facilitate reasoning at a higher level.In this paper we present an extension of the EPR-based bounded model checkingwith k-induction which can be used to prove safety properties of systems overunbounded runs. We present a novel abstraction-refinement approach based onunsatisfiable cores and models (UCM) for BMC and k-induction in the EPR setting.We have implemented UCM refinements for EPR-based BMC and k-induction in a first-order automated theorem prover iProver. We also extended iProver with the AIGER format and evaluated it over the HWMCC'14 competition benchmarks. The experimental results are encouraging. We show that a number of AIG problems can be verified until deeper bounds with the EPR-based model checking.
Clausal Proof Compression
Authors: Heule Marijn , Biere Armin 
Published: January 2018

Although clausal propositional proofs are significantly smaller comparedto resolution proofs, their size is still too large for severalapplications. In this paper we present several methods to compressclausal proofs. These methods are based on a two phase approach. Thefirst phase consists of a light-weight compression algorithm that caneasily be added to satisfiability solvers that support the emissionof clausal proofs. In the second phase, we propose to use a powerfuloff-the-shelf general-purpose compression tool, such as bzip2 and7z. Sorting literals before compression facilitates a delta encoding,which combined with variable-byte encoding improves the quality of thecompression. We show that clausal proofs can be compressed by one orderof magnitude by applying both phases.
Application of Adaptive Neural Networks for the Filtration of Spam
Authors: Besiashvili Gela , Bliadze Tamar , Kochladze Zurab 
Published: January 2018

The application of e-mail is the most widespread communication method. The increased email number includes permanently increased amount of unwanted notifications (spam). The statistics claims that 80% of the traffic is spam that lags the internet traffic, consumes space on hard disc, and reduces the capacity of the network, not to mention time spent for email’s classification. The advanced E-mail service packs contain spam filtration program. Nevertheless, to classify the e-mails as spam fully depends on the consumers, as information acceptable (or vital) for one consumer, may be a spam for other. Hence, it is crucial to have automatic spam filtration system for every individual consumer.The paper discuss the solution, a learning system that filters emails through consumers’ parameters and gradually learn how to filter them accordingly. The system based on multi-layer neural network, which uses logistic activation function, learns via tutor and counter-spread algorithm of mistakes
Stone duality for first-order logic: a nominal approach to logic and topology
Authors: Gabbay Murdoch J. 
Published: January 2018

What are variables, and what is universal quantification over a variable?Nominal sets are a notion of `sets with names', and using equational axioms in nominal algebra these names can be given substitution and quantification actions.So we can axiomatise first-order logic as a nominal logical theory.We can then seek a nominal sets representation theorem in which predicates are interpreted as sets; logical conjunction is interpreted as sets intersection; negation as complement.Now what about substitution; what is it for substitution to act on a predicate-interpreted-as-a-set, in which case universal quantification becomes an infinite sets intersection?Given answers to these questions, we can seek notions of topology.What is the general notion of topological space of which our sets representation of predicates makes predicates into `open sets'; and what specific class of topological spaces corresponds to the image of nominal algebras for first-order logic?The classic Stone duality answers these questions for Boolean algebras, representing them as Stone spaces.Nominal algebra lets us extend Boolean algebras to `FOL-algebras', and nominal sets let us correspondingly extend Stone spaces to `∀-Stone spaces'.These extensions reveal a wealth of structure, and we obtain an attractive and self-contained account of logic and topology in which variables directly populate the denotation, and open predicates are interpreted as sets rather than functions from valuations to sets.
Hierarchical Combination of Unication Algorithms (Extended Abstract)
Authors: Erbatur Serdar , Kapur Deepak , Marshall Andrew M , Narendran Paliath , Ringeissen Christophe 
Published: January 2018

A critical question in unification theory is how to obtaina unification algorithm for the combination of non-disjointequational theories when there exists unification algorithmsfor the constituent theories. The problem is known to bedifficult and can easily be seen to be undecidable in thegeneral case. Therefore, previous work has focused onidentifying specific conditions and methods in which theproblem is decidable.We continue the investigation in this paper, building onprevious combination results and our own work.We are able to develop a novel approach to the non-disjointcombination problem. The approach is based on a new set ofrestrictions and combination method such that if the restrictionsare satisfied the method produces an algorithm for the unificationproblem in the union of non-disjoint equational theories.
Data Conversion Method between a Natural Number and a Binary Tree for an Inductive Proof and Its Application
Authors: Takahashi Kazuko , Yoshimaru Shizuo , Goto Mizuki 
Published: January 2018

This paper presents modeling ofa binary tree that represents a natural numberand gives an inductive proof for its propertiesusing theorem provers.We define a function for converting data from a natural numberinto a binary treeand give an inductive proof for its well-definedness.We formalize this method, develop a computational model based on it,and apply it to an electronic cash protocol.We also define the payment function on the binary treeand go on to prove the divisibility of electronic cashusing the theorem provers Isabelle/HOL and Coq, respectively.Furthermore, we discuss the effectiveness of this method.
Projectivity and unification in the varieties of locally finite monadic MV-algebras
Authors: Di Nola Antonio , Grigolia Revaz , Lenzi Giacomo 
Published: January 2018

A description of finitely generated free monadic MV-algebras anda characterization of projective monadic MV-algebras in locally finitevarieties is given. It is shown that unification type of locally finitevarieties is unitary.
Acceleration-based safety decision procedure for programs with arrays
Authors: Alberti Francesco , Ghilardi Silvio , Sharygina Natasha 
Published: January 2018

Reachability analysis of programs with arrays is a well-known challenging problem and many existing approaches are bound to incomplete solutions.In this paper we identify a class of programs with arrays for which safety is fully decidable.The completeness result we provide is built up from acceleration techniques for arrays and the decision procedure for the Array Property Fragment class.
Industrial Examples of Formal Specifications for Test Case Generation
Authors: Roehm Hendrik , Gmehlich Rainer , Heinz Thomas , Oehlerking Jens , Woehrle Matthias 
Published: January 2018

While requirements engineering has received considerable attention inacademia over the past years, formalization of requirements for physicallyinfluenced systems is still a difficult task in practice. In this paper, we giveformal representations of some typical requirement classes arising in theautomotive industry. We divide these patterns into three main classes:those mostly referring to properties of continuous signals, those mostlyreferring to discrete events and those referring to similarity to a referencesignal. We discuss these patterns on concrete examples from automotiveembedded systems, where specifications are used for test case generation.
Contactless Surgery Light Control based on 3D Gesture Recognition
Authors: Dietz Armin , Schröder Stephan , Pösch Andreas , Frank Klaus , Reithmeier Eduard 
Published: January 2018

Surgery lighting systems (SLS) aim to provide optimal lighting conditions for the surgeon in an operating room. To visually differentiate between only marginally different looking tissues, SLS offer settings for the level of illumination, color temperature and size of the illuminated field. By today’s standards, SLS are controlled with control panels that are situated at the lamp housings. The operation of the control panel is handled in an ergonomically unfavorable position with the hands above the operator’s head. On top, the region above the operator’s shoulder is considered as not sterile and causes a potential safety risk. To secure asepsis, it is required to extensively sterilize all equipment that the operator comes in contact with.In this paper, a contactless gesture control for a SLS is developed with the intention to offer the surgeon a sterile and ergonomically comfortable operation. A Microsoft Kinect 3D-sensor is used. The gesture control offers control of the level of illumination, the color temperature and functions of a camera for documentation requirements like zooming, rotating and taking a picture. A sophisticated procedure to logon and logoff the system prevents unintentional operation.The gesture control system and the conventional control panel were tested and compared in a usability study. The participating subjects rated the usability of the gesture control to be good to very good according to the System Usability Scale by Broke. 94% of the subjects perceived the gesture control to be ergonomically more comfortable. After simultaneous operation of the surgery light and execution of a cognitive task, 82% stated that the gesture control is less likely to distract them from that task. This data indicates that the concept of a gesture control with a 3D-sensor for a SLS is feasible and that it has a potential to receive a high degree of acceptance.
El fundamento de una nación en el sureste Novohispano: A propósito de Votán, sacerdote fundador de Palenque, (1773-1994)
Authors: Díaz Perera Miguel Ángel 
Published: January 2018

Partiendo de los desacuerdos en la discusión sobre el origen del hombre americano entre los siglos XVI y XVIII, el autor muestra cómo nociones involucradas se insertaron en el nacionalismo criollo de finales del siglo XVIII, alimentadad por la obtención deobjetos prehispánicos. Ello sustentó argumentos históricos preindependentistas en el sureste de la Nueva España. En este contexto, tomó relevancia Votán, un supuesto sacerdote fundador que, a pesar de su olvido a raíz de la consolidación del centralismo mexicano a partir de 1994, volvió a reaparecer para poner en entredicho la acción epicéntrica del Estado mexicano.
De cómo la identidad étnica se vive en un contexto de migración: la presencia de migrantes chiapanecos en Los Altos de Jalisco
Authors: Hernández López Rafael Alonso 
Published: January 2018

El presente escrito tiene la finalidad de poner de manifiesto cómo se ha conformado la identidad étnica en un municipio de Jalisco con la presencia de migrantes procedentes de Chiapas para trabajar en la agroindustria del tequila . Para ello, mediante análisis documental, discursivo y etnográfico, se rastrean momentos que, a juicio del autor, terminan por poner de manifiesto un "proceso de destilación étnica", metáfora que sirve para explicitar los procesos y dinámicas surgidas de las relaciones étnicas entre dos grupos supuestamente diferenciados cultural y racialmente: los indígenas migrantes y los alteños.
El teatro como intervención feminista antirracista. Reflexiones en torno a las obras de teatro Raíz de ébano y Flores amarillas
Authors: Cuero Montenegro Astrid Yulieth 
Published: January 2018

Se reflexiona sobre la relación entre cultura, arte y política feminista antirracista a partir de mi participación en el Teatro-Foro Género y Racismo (Bogotá, 2011). A través del análisis de dos obras de teatro y de reflexiones teóricas sobre las articulaciones entre sexismo y racismo, sugiero la posibilidad de pensar el teatro como una forma de intervención feminista antirracista, como una forma de crear conciencia sobre el racismo que experimentamos como mujeres y como cuerpos racializados. Sitúo el teatro como un acto estético y político, con potencial para cuestionar las relaciones de poder y los mecanismos de opresión.
Cambio político-religioso en una localidad tojolabal del municipio de Las Margaritas, Chiapas
Authors: Escalona Victoria José Luis 
Published: January 2018

Desde las últimas décadas del siglo XX algunas regiones de Chiapas han sido el escenario de cambios de adscripción religiosa y de conflictos que han derivado en expulsiones y enfrentamientos violentos. En este trabajo se explora una línea de análisis sobre el conflicto religioso en Chiapas, a partir de un acercamiento etnográfico a una localidad rural del municipio de Las Margaritas. En ella conviven miembros de distintas iglesias, a pesar de haber vivido un enfrentamiento y amenaza de expulsión en 1985 y de las experiencias cercanas de conflicto y expulsión que han ocurrido en poblados vecinos.
El más acá de la modernidad. Los usos de la modernidad como temporalidad retórica
Authors: Ayora Díaz Steffan Igor , Vargas Cetina Gabriela 
Published: January 2018

En este ensayo proponemos que es necesario repensar los modelos que actualmente utilizamos para pensar en modernidad, posmodernidad y tradición. Queremos argumentar que la familia de conceptos posmodernidad, posmodernismo y posmodernización tiene sentido como equivalente a otras familias en las que el eje puede ser constituido sea por modernidad, modernidad reflexiva, modernidad tardía, alta modernidad, hipermodernidad o supermodernidad.
MigracIón internacIonal indígena y vulnerabIlIdad ante el VIH-sida. Los chamulas entre barras y estrellas
Authors: García Sosa Juan Carlos , Meneses Navarro Sergio , Palé Pérez Sebastiana 
Published: January 2018

Este artículo presenta testimonios de la experiencia de indígenas chamulas en relación con el proceso migratorio hacia los Estados Unidos. El propósito es identificar las condiciones y las prácticas que colocan a los migrantes y a sus familias ante el peligro de contraer infecciones de transmisión sexual, particularmente el VIH-SIDA. El marco de referencia propuesto se basa en los conceptos de vulnerabilidad y prácticas de riesgo, los cuales sirven para ordenar la relexión acerca del impacto de la migración sobre la salud sexual de los chamulas.
Acciones políticas y proyectos económicos en Guanajuato frente al conflicto de la Sierra Gorda 1847-1852
Authors: Preciado de Alba Carlos Armando 
Published: January 2018

Las revoluciones europeas de 1848 inquietaron a grandes sectores de la clase política mexicana pues fueron percibidas como un peligro para el orden social. Asimismo, en esos años, conflictos regionales como la Guerra de Castas y la rebelión en la Sierra Gorda amenazaban con trascender al ámbito nacional. Las autoridades guanajuatenses trataron de impulsar acciones políticas y económicas para controlar a la población. El artículo aborda el proyecto para la construcción de un presidio en la población serrana de Atargea, el cual, además de desincentivar potenciales brotes de violencia, buscaría reactivar la industria minera de la región.
Población indígena y etnohistoria en el extremo oriental de Venezuela
Authors: Velázquez Nelly 
Published: January 2018

El presente artículo tiene como propósito estudiar las características socioculturales y la historia de la población indígena del extremo oriental de Venezuela, específicamente del golfo de Paria, con la cual Colón entró en contacto en su tercer viaje. Para ello se utilizan tres fuentes fundamentales, como la información etnológica contenida en el relato colombino, los estudios de etnología basados en los relatos de los colonizadores realizados en la zona del oriente venezolano y las Antillas, a las que se añaden las fuentes arqueológicas.
El impacto de la variable de género en la migración Honduras-México: el caso de las Hondureñas en Frontera Comalapa
Authors: Madueño Haon Nicanor 
Published: January 2018

Este artículo se basa en dos estudios de campo realizados en Frontera Comalapa en agosto de 2008 y abril de 2009. Pretende participar en la inclusión de variables de género y de etnificación al análisis de las trayectorias migratorias. Se concluye que la migración femenina no genera cambios sustanciales en las relaciones de dominación que pueden existir en el país de origen. Al contrario, esas relaciones se acentúan durante la migración y se imponen como base de las estrategias de sobrevivencia o de evolución en el país de llegada.
Cultura, identidades y transculturalidad. Apuntes sobre la construcción identitaria de las juventudes indígenas
Authors: Zebadúa Carbonell Juan Pablo 
Published: January 2018

Este trabajo analiza conceptualmente la construcción de identidades juveniles indígenas a partir de su inserción en los contextos globales. Se analizan críticamente las identidades desde la cultura, y la transculturalidad, como un proceso social mediante el cual se construyen las identidades juveniles de la actualidad, particularmente las indígenas. Se observan directrices analíticas para entender la aparición de grupos de jóvenes indígenas con nuevas formas de agregación identitaria.
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 â€”forestales, minerales e hídricosâ€”, en beneficio de las grandes potencias mundiales, sobre todo Estados Unidos.
Análisis de rentabilidad de una empresa integradora de aprovechamiento de madera de pino
Authors: Vásquez-García Adela Vásquez-García , Arturo Matus-Gardea Jaime , Cetina-Alcalá Víctor Manuel , Sangerman-Jarquín Dora Ma. , Rendón Sánchez Gilberto , Caamal Cauich Ignacio 
Published: January 2018

Las pequeñas y medianas empresas tienen que buscar la forma de mantenerse, compitiendo con las grandes empresas, pues han avanzado sus mercados provocando la desaparición de muchas de estas y las empresas integradoras surgen con la finalidad de agrupar a pequeñas y medianas empresas con el propósito de que a través de esta unión se obtengan ventajas de rentabilidad y competitividad para ellas. Se evaluó la rentabilidad financiera del aprovechamiento de madera de pino de una empresa integradora ubicada en Ixtlán de Juárez, Oaxaca utilizando encuestas para recopilar información y realizar la evaluación de rentabilidad financiera como empresa integradora mediante el cálculo de indicadores valor actual neto (VAN), tasa interna de retorno (TIR), relación beneficio costo. Los resultados obtenidos fueron: VAN= 481 952.4, TIR= 33% y relación beneficio costo= 1.01. Con los cuales se encontró que durante la vida útil del proyecto a una tasa de actualización de 31%, se va obtener una utilidad neta de 481 952.4 pesos. Con respecto a la relación beneficio/ costo a una actualización de 31%, por cada peso invertido se tendrá 1.01 centavos de beneficios y durante la vida útil del proyecto y de acuerdo a los resultados de la TIR se recupera la inversión y se obtiene una rentabilidad en promedio de 33%. Estos indicadores muestran que la empresa tiene una rentabilidad financiera positiva.
Identidad, organización y estrategia en dos movimientos que pugnan por la soberanía alimentaria en México
Authors: Pardo Núñez Joaliné 
Published: January 2018

Analizo y comparo dos movimientos por la soberanía alimentaria en México a partir de las identidades colectivas que integran cada uno, las formas en que se organizan para trabajar y decidir, así como las decisiones estratégicas que toman para orientar su acción y movilizarse. Ambos contribuyen al debate por la construcción de un nuevo proyecto alimentario en México y estudian problemas similares desde perspectivas diferentes para revisar el papel del campo. Los actores colectivos de cada caso comparten un pasado común anclado en el movimiento campesino, pero se reconstituyen como dos proyectos separados a partir de evaluaciones diferenciadas de la acción y sus resultados, para dar lugar a dos movimientos distintos en su configuración, organización y postura ante el Estado.