bluuebunny/crossref_metadata_2025_split huggingface dataset:
Simbol Semiotik dalam Novel Anomie Karya Rilda A. Oe. Taneko
Authors: Wibowo Erwin 
Published: January 2018

The aim of the research is to describe semiotic meanings in the Rilda A.Oe. Taneko’s novel, Anomie. The method used is decriptive method with semiotic approach by Pierce which includes icons, indexes, and symbols. The data source used in this research is the novel Anomie written by Rilda A.Oe. Taneko by investigating the data of symbols reflected in the quotations, and some books which are treated as references in this research. The collecting data technique is conducted by using literary review. The problems which are elaborated in this research are 1)identifying icons, indexes, and symbols semiotic in the novel Anomie written by Rilda A.Oe. Taneko, 2) describing icons, indexes, and symbols semiotic in the Rilda A.Oe. Taneko’s novel, Anomie. The results of this study show the novel Anomie by Rilda A.Oe. Taneko there is a semiotic symbol that includes the icon of educational institutions, social institutions, and entertainment venues. This novel index belongs to the strength, greed, pride and character figures. The symbols of this novel include symbols of wealth, sacrificial symbols, and symbols of love.AbstrakPenelitian ini bertujuan untuk mendeskripsikan makna semiotik yang terdapat dalam novel Anomie karya Rilda A.Oe. Taneko. Metode yang digunakan adalah metode deskriptif, dengan pendekatan semiotic Pierce yang meliputi ikon, indeks dan simbol. Sumber data yang dipakai dalam penelitian ini adalah novel Anomie karya Rilda A.Oe. Taneko dengan mengamati data-data ikon, indeks dan simbol yang tercermin dalam kutipan-kutipan tersebut, dan beberapa buku yang dijadikan referensi dalam penelitian ini. Teknik pengambilan data menggunakan teknik studi pustaka. Permasalahan yang akan dipecahkan dalam penelitian ini adalah (1) mengidentifikasi ikon, indeks dan simbol semiotik yang terdapat dalam novel Anomie karya Rilda A.Oe. Taneko, dan (2) mendeskripsikan ikon, indeks dan simbol semiotik yang terdapat dalam novel Anomie karya Rilda A.Oe. Taneko. Hasil penelitian ini menunjukan bahwa novel Anomie karya Rilda A.Oe. Taneko terdapat simbol semiotik yang meliputi ikon berupa lembaga pendidikan, lembaga sosial, dan tempat hiburan. Indeks dalam novel ini berupa kekuasaan, keserakahan, kesombongan dan kekhawatiran tokoh-tokohnya. Simbol pada novel ini meliputi simbol kekayaan, simbol pengorbanan, dan simbol cinta kasih.
Program Verification as Satisfiability Modulo Theories
Authors: Bjorner Nikolaj , McMillan Kenneth , Rybalchenko Andrey 
Published: January 2018

A key driver of SMT over the past decade has been an interchange format, SMT-LIB,and a growing set of benchmarks sharing this common format.SMT-LIB captures very well an interface that is suitablefor many tasks that reduce to solving first-order formulas modulo theories.Here we propose to extend these benefits into the domain of symbolicsoftware model checking. We make a case that SMT-LIB canbe used, and to a limited extent adapted, for exchanging symbolicsoftware model checking benchmarks. We believe this layer facilitatesdividing innovations in modeling, developing program logics and front-ends,from developing algorithms for solving constraints over recursive predicates.
A rewrite-based computational model for functional logic programming
Authors: Marin Mircea , Kutsia Temur , Dundua Besik 
Published: January 2018

Functional logic programming extends the functional programming style with two important features: the possibility to define nondeterministic operations with overlapping rules, and the usage of logic variables in both defining rules and expressions to evaluate. Conditional constructor-based term rewrite systems (CB-CTRSs) emerged as a suitable model for functional logic programs, because they can be easily transformed into an equivalent program in a core language where computations can be performed more efficiently.We consider a recent proposal by Antoy and Hanus, of translating CB-CTRSs into an equivalent class of programs where computation can be performed by mere rewriting. His computational model has the limitation of computing only ground answer substitutions for equations with strict semantics interpreted as joinability to a value.We propose two adjustments of their computational models, which are capable to compute non-ground answers.
Legal Question Answering System using Neural Attention
Authors: Morimoto Ayaka , Kubo Daiki , Sato Motoki , Shindo Hiroyuki , Matsumoto Yuji 
Published: January 2018

This year’s COLIEE has two tasks called phases 1 and 2. The phase 1 needs to find the relevant article given a query t2, and the phase 2 needs to answer whether the given query t2 is yes or no according to Japan civil law articles.This paper presents our proposals for the phase 2 task. Two methods are presented. The first goes along the standard method taken by many authors, such that the relevant article t1 is selected by the similarity to the query t2 at the requirement (condition) and the effect (conclusion) descriptions of the articles. The second is our new proposal, in which Neural Networks with attention mechanism are applied to all the civil law articles in deciding the truthness of the query t2. This method takes into account all the articles by properly calculating their weighted sum.
Synthesising Graphical Theories
Authors: Kissinger Aleks 
Published: January 2018

In recent years, diagrammatic languages have been shown to be a powerful and expressive tool for reasoning about physical, logical, and semantic processes represented as morphisms in a monoidal category. In particular, categorical quantum mechanics, or "Quantum Picturalism", aims to turn concrete features of quantum theory into abstract structural properties, expressed in the form of diagrammatic identities. One way we search for these properties is to start with a concrete model (e.g. a set of linear maps or finite relations) and start composing generators into diagrams and looking for graphical identities.Naively, we could automate this procedure by enumerating all diagrams up to a given size and check for equalities, but this is intractable in practice because it produces far too many equations. Luckily, many of these identities are not primitive, but rather derivable from simpler ones. In 2010, Johansson, Dixon, and Bundy developed a technique called conjecture synthesis for automatically generating conjectured term equations to feed into an inductive theorem prover. In this extended abstract, we adapt this technique to diagrammatic theories, expressed as graph rewrite systems, and demonstrate its application by synthesising a graphical theory for studying entangled quantum states.
(The Final) Countdown
Authors: Alliot Jean-Marc , Vanaret Charlie 
Published: January 2018

The Countdown game is one of the oldest TV show in theworld. It started broadcasting in 1972 on the french televisionand in 1982 on British channel 4, and it has been running since inboth countries.The game, while extremely popular, never received any seriousscientific attention, probably because it seems too simple at first sight.We present in this article an in-depth analysis of thenumbers round of the countdown game. This includes a complexityanalysis of the game, an analysis of existing algorithms and the presentationof a new algorithm that increases resolution speed by a large factor.It also includes some leads on how to turn the game into amore difficult one, both for a human player and for a computer, andeven to transform it into a possibly undecidable problem.
Anatomy of Alternating Quantifier Satisfiability (Work in progress)
Authors: Phan Anh-Dung , Bjørner Nikolaj , Monniaux David 
Published: January 2018

We report on work in progress to generalize an algorithm recently introduced in [10] for checkingsatisfiability of formulas with quantifier alternation. The algorithm uses two auxiliary procedures:a procedure for producing a candidate formula for quantifier elimination and a procedure for eliminatingor partially eliminating quantifiers. We also apply the algorithm for Presburger Arithmeticformulas and evaluate it on formulas from a model checker for Duration Calculus [8]. We report onexperiments on different variants of the auxiliary procedures. So far, there is an edge to applyingSMT-TEST proposed in [10], while we found that a simpler approach which just eliminates quantifiedvariables per round is almost as good. Both approaches offer drastic improvements to applyingdefault quantifier elimination.
Towards a Logic for Reasoning About Learning in a Changing World
Authors: Panangaden Prakash , Sadrzadeh Mehrnoosh 
Published: January 2018

We develop an algebraic modal logic that combines epistemic and dynamic modalities with a view to modelling information acquisition (learning) by automated agents in a changing world. Unlike most treatments of dynamic epistemic logic, we have transitions that ``change the state'' of the underlying system and not just the state of knowledge of the agents. The key novel feature that emerges is the need to have a way of ``inverting transitions'' and distinguishing between transitions that ``really happen'' and transitions that are possible.Our approach is algebraic, rather than being based on a Kripke-style semantics. The semantics are given in terms of quantales. We introduce a class of quantales with the appropriate inverse operations and use it to model toy robot-navigation problems, which illustrate how an agent learns information by taking actions. We discuss how a sound and complete logic of the algebra may be obtained from the positive fragment of PDL with converse.
Scheme representation for first-order logic
Authors: Awodey Steve , Breiner Spencer 
Published: January 2018

My research concerns a construction of "logical schemes," geometric entitieswhich represent logical theories in much the same way that algebraic schemesrepresent rings. These involve two components: a semantic spectral spaceand a syntactic structure sheaf. As in the algebraic case, we can recover atheory from its scheme representation (up to a conservative completion) andthe structure sheaf is local in a certain logical sense. From these ane pieceswe can build up a 2-category of logical schemes which share some of the niceproperties of algebraic schemes.
Transforming Event B Models into Verified C# Implementations
Authors: Mery Dominique , Monahan Rosemary 
Published: January 2018

The refinement-based approach to developing software is based on thecorrect-by-construction paradigm were software systems are constructed via the step-by-step refinement of an initial high-level specification into a final concrete specification. Proof obligations, generated during this process are discharged to ensure the consistency between refinement levels and hence the system's overall correctness.Here, we are concerned with the refinement of specifications using the Event B modelling language and its associated toolset, the Rodin platform. In particular, we focus on the final steps of the process where the final concrete specification is transformed into an executable algorithm. The transformations involved are (a) the transformation from an Event B specification into a concrete recursive algorithm and (b) the transformation from the recursive algorithm into its equivalent iterative version. We prove both transformations correct and verify the correctness of the final code in a static programme verification environment for C# programs, namely the Spec# programming system.
On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width
Authors: Kovásznai Gergely , Fröhlich Andreas , Biere Armin 
Published: January 2018

Bit-precise reasoning is important for many practical applications ofSatisfiability Modulo Theories (SMT). In recent years efficient approachesfor solving fixed-size bit-vector formulas have been developed. Fromthe theoretical point of view, only few results on the complexity offixed-size bit-vector logics have been published. In this paper we showthat some of these results only hold if unary encoding on the bit-width ofbit-vectors is used. We then consider fixed-size bit-vector logics withbinary encoded bit-width and establish new complexity results. Our proofsshow that binary encoding adds more expressiveness to bit-vector logics,e.g. it makes fixed-size bit-vector logic even without uninterpretedfunctions nor quantication NExpTime-complete. We also show that undercertain restrictions the increase of complexity when using binary encodingcan be avoided.
Proof Assistants and the Dynamic Nature of Formal Theories
Authors: Constable Robert L. 
Published: January 2018

This article shows that theory exploration arises naturally from the need to progressively modify applied formal theories, especially those underpinning deployed systems that change over time or need to be attack-tolerant. Such formal theories require us to explore a problem space with a proof assistant and are naturally dynamic.The examples in this article are from our on-going decade-long effort to formally synthesize critical components of modern distributed systems. Using the Nuprl proof assistant we created event logic and its protocol theories. I also mention the impact over this period of extensions to the constructive type theory implemented by Nuprl. One of them led to our solution of a long standing open problem in constructive logic.Proof exchange among theorem provers is promising for improving the "super tactics" that provide domain specific reasoners for our protocol theories. Both theory exploration and proof exchange illustrate the dynamic nature of applied formal theories built using modern proof assistants. These activities dispel the false impression that formal theories are rigid and brittle artifacts that become less relevant over time in a fast moving field like computer science.
A Genetic Algorithm based Control Strategy for the Energy Management Problem in PHEVs
Authors: Nellen Johanna , Wolters Benedikt , Netz Lukas , Geulen Sascha , Abraham Erika 
Published: January 2018

Genetic algorithms have been applied to various optimization problems in the past. Our library GeneiAL implements a framework for genetic algorithms specially targeted to the area of hybrid electric vehicles. In a parallel hybrid electric vehicle (PHEV), an internal combustion engine and an electrical motor are coupled on the same axis in parallel. In the area of PHEVs, genetic algorithms have been extensively used for the optimization of parameter tuning of control strategies. We use GeneiAL to control the torque distribution between the engines directly. The objective function of this control strategy minimizes the weighted sum of functions that evaluate the fuel consumption, the battery state of charge, and drivability aspects over a prediction horizon of fixed finite length.We analyze the influence of these weights and different configurations for the genetic algorithm on the computation time, the convergence, and the quality of the optimization result. For promising configurations, we compare the results of our control strategy with common control strategies.
Exotic Semi-Ring Constraints
Authors: Codish Michael , Fekete Yoav , Fuhs Carsten , Giesl Jürgen , Waldmann Johannes 
Published: January 2018

Exotic semi-ring constraints arise in a variety of applications andin particular in the context of automated termination analysis.We propose two techniques to solve such constraints: (a) to modelthem using Boolean functions and integer linear arithmetic and solvethem using an SMT solver (QF_LIA, in certain cases also QF_IDL);and (b) to seek finite domain solutions by applying unary bit-blastingand solve them using a SAT solver.In this note, we show the structure of such systems of constraints,and report on the performance of SMT solvers and SAT encodings whensolving them. In particular, we observe that good results areobtained by unary bit-blasting, improving on previous proposals toapply binary bit-blasting. Moreover, our results indicate that, forour benchmarks, unary bit-blasting leads to better results than theones directly obtained by an SMT solver.
A Quantitative Partial Model-Checking Function and Its Optimisation
Authors: Bistarelli Stefano , Martinelli Fabio , Matteucci Ilaria , Santini Francesco 
Published: January 2018

Partial Model-Checking (PMC) is an efficient tool to reduce the combinatorial explosion of a state-space, arising in the verification of loosely-coupled software systems. At the same time, it is useful to consider quantitative temporal-modalities. This allows for checking whether satisfying such a desired modality is too costly, by comparing the final score consisting of how much the system spends to satisfy the policy, to a given threshold. We stir these two ingredients together in order to provide a Quantitative PMC function (QPMC), based on the algebraic structure of semirings. We design a method to extract part of the weight during QPMC, with the purpose to avoid the evaluation of a modality as soon as the threshold is crossed. Moreover, we extend classical heuristics to be quantitative, and we investigate the complexity of QPMC.Keyword: Partial Model Checking, Semirings, Optimisation, Quantitative Modal Logic Quantitative Process Algebra, Quantitative Evaluation of Systems.
Automatic Staging via Partial Evaluation Techniques
Authors: Asai Kenichi , Kameyama Yukiyoshi 
Published: January 2018

Partial evaluation and staging are two of the well-known symbolicmanipulation techniques of programs which generate efficientspecialized code. On one hand, partial evaluation provides us with anautomatic means to separate a program into two (or more) stages butits behavior is perceived as hard to control. On the other hand,staging (or staged calculus) requires us to manually separate aprogram but with full control over its behavior. In the previouswork, the first author introduced a framework to relate the twotechniques, giving a unified view to the two techniques. In thispaper, we extend the framework to handle the cross-stage persistence(CSP) and show that the 2-level staging annotation obtained by theautomatic separation is the best staging annotation in a system whereCSP is allowed for base-type values only. In the presence of CSP forhigher-type values, on the other hand, there is no single annotationthat is better than all the other annotations.
Decision Problems for Linear Recurrence Sequences
Authors: Ouaknine Joel 
Published: January 2018

Linear recurrence sequences (LRS), such as the Fibonacci numbers, permeate vast areas of mathematics and computer science. In this talk, we consider three natural decision problems for LRS, namely the Skolem Problem (does a given LRS have a zero?), the Positivity Problem (are all terms of a given LRS positive?), and the Ultimate Positivity Problem (are all but finitely many terms of a given LRS positive?). Such problems (and assorted variants) have applications in a wide array of scientific areas, such as theoretical biology (analysis of L-systems, population dynamics), economics (stability of supply-and-demand equilibria in cyclical markets, multiplier-accelerator models), software verification (termination of linear programs), probabilistic model checking (reachability and approximation in Markov chains, stochastic logics), quantum computing (threshold problems for quantum automata), discrete linear dynamical systems (reachability and invariance problems), as well as combinatorics, statistical physics, term rewriting, formal languages, cellular automata, generating functions, etc.We shall see that these problems have deep and fascinating connectionsto rich mathematical concepts and conjectures, particularly in thefields of analytic and algebraic number theory, diophantine geometryand approximation, real algebraic geometry, mathematicallogic, and complexity theory.
Playing with Quantified Satisfaction
Authors: Bjorner Nikolaj , Janota Mikolas 
Published: January 2018

We develop an algorithm for satisfiability of quantified formulas.The algorithm is based on recent progress in solving Quantified Boolean Formulas,but it generalizes beyond propositional logic to theories, such as linear arithmeticover integers (Presburger arithmetic), linear arithmetic over reals, algebraic data-types and arrays.Compared with previous algorithms for satisfiability of quantified arithmetical formulasour new implementation outperforms previous implementations in Z3 by a significant margin.
Programming by Composing Filters
Authors: Fischer Jeffrey , Majumdar Rupak 
Published: January 2018

We present a formal model for event-processing pipelines. Event-processing pipelines appear in a large number of domains, from control of cyber-physical systems (CPS), to large scale data analysis, to Internet-of-things applications. These applications are characterized by stateful transformations of event streams, for example, for the purposes of sensing, computation, and actuation of inner control loops in CPS applications, and for data cleaning, analysis, training, and querying in data analytics applications.Our formal model provides two abstractions: streams of data, and stateful, probabilistic, filters, which transform input streams to output streams probabilistically. Programs are compositions of filters. The filters are scheduled and run by an explicit, asynchronous, scheduler.We provide a transition system semantics for such programs based on infinite-state Markov decision processes. We characterize when a program is scheduler-independent, that is, provides the same observable behavior under every scheduler, based on local commutativity.
Mind the Gap: Formal Verification and the Common Criteria (Discussion Paper)
Authors: Beckert Bernhard , Bruns Daniel , Grebing Sarah 
Published: January 2018

It is a common belief that the rise of standardized software certification schemes like the Common Criteria (CC) would give a boost to formal verification, and that software certification may be a killer application for program verification. However, while formal models are indeed used throughout high-assurance certification, verification of the actual implementation is not required by the CC and largely neglected in certification practice - despite the great advances in program verification over the last decade.In this paper we discuss the gap between program verification and CC software certification, and we point out possible uses of code-level program verification in the CC certification process.
El Instituto Nacional Indigenista en el municipio de Oxchuc, 1951-1971
Authors: Corbeil Laurent 
Published: January 2018

Este artículo analiza las relaciones entre el Instituto Nacional Indigenista y los tseltales del municipio de Oxchuc, en el contexto de un intento de integración nacional de los indígenas. El estudio de los informes indigenistas y de las comunicaciones proporciona una perspectiva más abierta y matizada sobre un proyecto que ha sido criticado. Aunque el objetivo de los oxchuqueros de desarrollar su economía no tuvo éxito, se creó una cierta integración institucional, jurídica y educacional. A pesar de los impactos negativos de tal integración, pensamos que la apertura de ambas partes permitió el establecimiento de un diálogo positivo.
Inmigración, emigración y tránsito migratorio en Chiapas: un bosquejo general
Authors: Anguiano Téllez María Eugenia 
Published: January 2018

Se explora la condición actual del estado de Chiapas como territorio de inmigración nacional y extranjera, como entidad expulsora de migrantes al resto del país y Estados Unidos, y como espacio y trayecto de tránsito migratorio de guatemaltecos y migrantes de otras nacionalidades. Para ello, se analiza información que proporcionan el Instituto Nacional de Geografía, Estadística e Informática, el Consejo Nacional de Población, el Instituto Nacional de Migración y dos encuestas de flujos migratorios en las que participa El Colegio de la Frontera Norte.