bluuebunny/crossref_metadata_2025 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.
试论建筑企业如何积极应对“营改增”
Authors: 陈 鹭佳
Published: January 2018

随着社会经济的不断发展，中国税改制度逐渐完善，其中最受瞩目的当属“营改增”制度的推行，而建筑企业作为最初的试点行业之一，也面临着需要快速适应的过程。因此，建筑企业该如何应对“营改增”就显得十分重要。论文在对建筑行业进行“营改增”的必要性及增值税的特点进行探讨分析的基础上，分析了建筑行业“营改增”实施后所产生的各方面影响，最后提出了建筑行业应对“营改增”的对策，为建筑企业平稳渡过“营改增”提供参考依据。
探析管理会计在企业应用中存在的问题与对策
Authors: 凌 婵娟 , 赵 婉婷
Published: January 2018

管理会计是伴随着社会经济的发展、科学技术的进步以及企业经营管理的需求而不断发展的。管理会计是现代企业会计中的一个分支，其与财务会计并驾齐驱，是同现代企业内部管理相适应的一门学科。管理会计通常被认为是管理和会计的结合体，它将经济学、管理学、组织行为学等相关学科应用于会计学科，使其在企业内部的运用平台上达到向企业管理者提供有助于其做出科学预测和决策的会计信息的应用目标。通过探究管理会计在企业应用中存在的不足，提出合理的对策，以不断完善企业管理会计体系[1]。
精准扶贫主体行为逻辑与作用机制研究
Authors: 徐 徐立新
Published: January 2018

为了实际解决贫困问题，中国在发展过程中对精准扶贫的历史进程进行了分析，研究出了主要的扶贫主体行为结构和行为动机，同时构建了一些能辅助进行脱贫管理的作用机制。这些作用机制能够较好地让扶贫工作人员找到自己最准确的工作定位，在工作过程中，能根据扶贫工作要求，对自身工作进行完善，找到提升精准扶贫工作质量的好方法。
A PROPRIEDADE RURAL NOS DEBATES DA ASSEMBLEIA NACIONAL CONSTITUINTE
Authors: Sá João Daniel Macedo
Published: January 2018

O presente trabalho procura refletir sobre o processo constitucional brasileiro. Para tanto, se propõe a analisar a proteção da propriedade rural a partir dos debates da Assembleia Nacional Constituinte, que antecederam e delinearam os contornos da Constituição Federal de 1988. Desse modo, procura identificar em que medida, e sob qual contexto político, foi desenhada a fundamentação da proteção conferida à propriedade rural. Ao final, apresenta uma crítica ao resultado do processo legislativo e defende a necessidade de pensar os objetivos das políticas públicas no espaço agrário sob um novo enfoque constitucional, que traduza uma atuação mais eficiente do poder público.
THE IMPACT OF CULTURAL DIMENSIONS ON STUDENTS’ ATTITUDE TOWARDS PROBLEMBASED LEARNING
Authors: Zaduqisti Esti
Published: January 2018

Abstrak: Air adalah sumber daya alam yang vital bagi kehidupan yang merupakan kepemilikan umum. Akhir-akhir ini air menjadi lahan bisnis yang menjanjikan diantaranya adalah produk air minum dalam kemasan (AMDK) yang dikelola swasta. Pengelolaan air yang dikuasai oleh swasta akan menimbulkan masalah karena swasta semata-mata berorientasi profit. Perlunya intervensi pemerintah dalam pengelolaan sumberdaya air mengingat air adalah kebutuhan hajat orang banyak. Tujuan penelitian ini adalah menganalisis pengelolaan AMDK yang dikuasai swasta, pendekatan penelitian dengan metode kualitatif dengan pendekatan studi pustaka. Hasil penelitian menunjukkan perlunya intervensi pemerintah dalam pengelolaan AMDK, dan merekomendasikan BUMDes sebagai media pengelola guna kesejahteraan umat.Abstract.Water is a natural resourcesthatis vital to the life which is public ownership. Recently,water becomes promising business area including a produc to bottle water (AMDK) are privately managed. Water management is controlled by the private sector because the private sector will lead to problems because of their solely profit-oriented. The need forgovernment intervention in themanagement of water resources given of wateras livelihood needs of people. The purpose of this study was to analyze the management of drinking water that is controlled by the private sectorusing qualitativ emethod. The results showed the need for government intervention in the management of drinking water, and recommends BUMDes as media to manage water for the welfare of the people.
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 suitable

for many tasks that reduce to solving first-order formulas modulo theories.

Here we propose to extend these benefits into the domain of symbolic

software model checking. We make a case that SMT-LIB can

be used, and to a limited extent adapted, for exchanging symbolic

software model checking benchmarks. We believe this layer facilitates

dividing innovations in modeling, developing program logics and front-ends,

from developing algorithms for solving constraints over recursive predicates.
Spectral-like duality for Distributive Hilbert Algebras with Infimum
Authors: Celani Sergio A. , Esteban María , Jansana Ramón
Published: January 2018

We present the results of our research on stone-type dualities for certain classes of ordered algebras that do not fall within the scope of extended Priestley-duality. In a forthcoming paper we study a new spectral-like duality for the class of distributive Hilbert algebras with infimum. We explain the main facts of that duality and we outline how the same strategy could be used for getting a Priestley-style duality for the same class of algebras, as well as dualities for other classes of algebras.
Improving Legal Information Retrieval by Distributional Composition with Term Order Probabilities
Authors: S. Carvalho Danilo , Tran Vu , Tran Khanh Van , Le Minh Nguyen
Published: January 2018

Legal professionals worldwide are currently trying to get up-to-pace with the explosive growth in legal document availability through digital means. This drives a need for high efficiency Legal Information Retrieval (IR) and Question Answering (QA) methods. The IR task in particular has a set of unique challenges that invite the use of semantic motivated NLP techniques. In this work, a two-stage method for Legal Information Retrieval is proposed, combining lexical statistics and distributional sentence representations in the context of Competition on Legal Information Extraction/Entailment (COLIEE). The combination is done with the use of disambiguation rules, applied over the rankings obtained through n-gram statistics. After the ranking is done, its results are evaluated for ambiguity, and disambiguation is done if a result is decided to be unreliable for a given query. Competition and experimental results indicate small gains in overall retrieval performance using the proposed approach. Additionally, an analysis of error and improvement cases is presented for a better understanding of the contributions.
A One-Pass Tree-Shaped Tableau for LTL+Past
Authors: Gigante Nicola , Montanari Angelo , Reynolds Mark
Published: January 2018

Linear Temporal Logic (LTL) is a de-facto standard formalism for expressing properties of systems and temporal constraints in formal verification, artificial intelligence, and other areas of computer science. The problem of LTL satisfiability is thus prominently important to check the consistency of these temporal specifications. Although adding past operators to LTL does not increase its expressive power, recently the interest for explicitly handling the past in temporal logics has increased because of the clarity and succinctness that those operators provide. In this work, a recently proposed one-pass tree-shaped tableau system for LTL is extended to support past operators. The modularity of the required changes provides evidence for the claimed ease of extensibility of this tableau system.
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.
Towards Improving the Resource Usage of SAT-solvers
Authors: Manthey Norbert , Saptawijaya Ari
Published: January 2018

The paper presents our work on cache analysis of SAT-solving. The aim is to study how resources are utilized by a SAT-solver and to use this knowledge to improve the resource usage in SAT-solving. The analysis is performed mainly on our CDCL-based SAT-solver and additionally on MiniSAT and PrecoSAT. The measurement is conducted using sample-based profiling on some industrial benchmark from the SAT-competition 2009. During the measurement the following hardware events are traced: total cycles, stall cycles, L2 cache hits and L2 cache misses. From the measurement results, our runtime and implementation analysis unveil that several improvements on resource usage can be done, i.e. on data structures and memory access. These improvements bring about 60% speedup of runtime performance for our solver.
Automated Reasoning for Explainable Artificial Intelligence
Authors: Bonacina Maria Paola
Published: January 2018

Reasoning and learning have been considered fundamental features of intelligence ever since the dawn of the field of artificial intelligence, leading to the development of the research areas of automated reasoning and machine learning. This short paper is a non-technical position statement that aims at prompting a discussion of the relationship between automated reasoning and machine learning, and more generally between automated reasoning and artificial intelligence. We suggest that the emergence of the new paradigm of XAI, that stands for eXplainable Artificial Intelligence, is an opportunity for rethinking these relationships, and that XAI may offer a grand challenge for future research on automated reasoning.
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.
Building an Efficient OWL 2 DL Reasoner
Authors: Motik Boris
Published: January 2018

The Ontology Web Language (OWL) has received considerable traction recently and is used in a number of industrial and practical applications. While decidable, all basic reasoning tasks for OWL are intractable (most of them are N2ExpTime-complete). Thus, in order to obtain a system capable of solving practically-relevant nontrivial problems, a number of theoretical and practical issues need to be resolved. In my talk I will present an overview of the techniques employed in HermiT, a state-of-the-art OWL reasoner developed at Oxford University. I will present the main ideas behind the hypertableau calculus and contrast them with the tableau calculi used in similar systems. Furthermore, I will discuss optimization techniques used in HermiT such as the blocking cache, individual reuse, and core blocking. Finally, I will discuss certain higher-level optimizations implemented on top of the basic calculus, such as the recently-developed optimized classification algorithm.
SMT-Based System Verification with DVF
Authors: Goel Amit , Krstic Sava , Leslie Rebekah , Tuttle Mark
Published: January 2018

We introduce the Deductive Verificaton Framework (DVF), a language and a tool for verifying properties of transition systems. The language is procedural and the system transitions are a selected subset of procedures. The type system and built-in operations are consistent with SMT-LIB, as are the multisorted first-order logical formulas that may occur in DVF programs as pre- and post-conditions, assumptions, assertions, and goals. A template mechanism allows parametric specification of complex types within the confines of this logic. Verification conditions are generated from specified goals and passed to SMT engine(s). A general assume-guarantee scheme supports a thin layer of interactive proving.
A note on first-order reasoning for minimum models
Authors: Rydeheard David , Sánchez Jesús Héctor Domínguez
Published: January 2018

In this note, we consider a notion of minimum model suitable for formulating a semantics of evolvable computing systems using a revision-based logic. We explore a range of proof systems for reasoning in the logic of minimum models and consider their application to the simulation of evolvable systems. Finally, we outline how these proof systems may be implemented in a logical framework.
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.
SAT solving experiments in Vampire
Authors: Biere Armin , Dragan Ioan , Kovács Laura , Voronkov Andrei
Published: January 2018

In order to better understand how well a state of the art SAT solver would behave in the framework of a first-order automated theorem prover we have decided to integrate Lingeling, best performing SAT solver, inside Vampire’s AVATAR framework. In this paper we propose two ways of integrating a SAT solver inside of Vampire and evaluate overall performance of this combination. Our experiments show that by using a state of the art SAT solver in Vampire we manage to solve more problems. Surprisingly though, there are cases where combination of the two solvers does not always prove to generate best results.
A One-Pass Tableau-Based Workflow Verification Framework
Authors: Islam Md Zahidul , Maccaull Wendy
Published: January 2018

Workflow management systems (WfMSs) are useful tools for supporting enterprise information systems. Such systems must ensure compliance with guidelines and regulations. While formal verification techniques can be used in the development stages to help ensure behavioral properties of many systems, these techniques are generally not available in workflow tools. We present a framework which models workflows using Petri nets and translates the model to a tableau style model checker. The model checker uses the recently introduced one-pass tableau algorithm and delivers enhanced performance over traditional two-pass strategies in practical applications. A failed tableau will generate a counter model which can aid in debugging. We present a case study involving a health services delivery program, and verify properties written in Computation Tree Logic (CTL). The algorithm can be easily modified to accomodate other specification languages such as timed CTL, logics of beliefs, desires and intentions, temporal description logic, first order logic, and others.
Open projections do not form a right residuated lattice
Authors: Kruml David
Published: January 2018

The lattice of open projection of a C*-algebra has a partial monoid structure on compatible elements. However, this does not extend to a total right residuated operation.
Howard Barringer: the Man who Invented the Past
Authors: Havelund Klaus
Published: January 2018

This article is an introduction to Professor Howard Barringer, in honor of his 60th birthday on December 20, 2011, which was celebrated by the HOWARD-60 workshop (Higher-Order Workshop on Automated Runtime verification and Debugging), held on the same day at University of Manchester.
(The Final) Countdown
Authors: Alliot Jean-Marc , Vanaret Charlie
Published: January 2018

The Countdown game is one of the oldest TV show in the

world. It started broadcasting in 1972 on the french television

and in 1982 on British channel 4, and it has been running since in

both countries.

The game, while extremely popular, never received any serious

scientific attention, probably because it seems too simple at first sight.

We present in this article an in-depth analysis of the

numbers round of the countdown game. This includes a complexity

analysis of the game, an analysis of existing algorithms and the presentation

of a new algorithm that increases resolution speed by a large factor.

It also includes some leads on how to turn the game into a

more difficult one, both for a human player and for a computer, and

even to transform it into a possibly undecidable problem.
On fuzzification of topological categories
Authors: Solovjovs Sergejs
Published: January 2018

This talk provides a fuzzification procedure for topological categories, i.e., given a topological category A, there exists a topological category B, which contains A as a full concretely coreflective subcategory, and which can be considered as a fuzzification of A.
Representation of the Medial-Like Algebras
Authors: Ehsani Amir
Published: January 2018

In this paper we characterize the regular medial algebras, the paramedial n-ary groupoids with a regular element, the paramedial algebras with a regular element and the regular paramedial algebras. Also, we characterize paramedial, co-medial and co-paramedial pairs of quasigroup operations and paramedial, co-medial and co-paramedial algebras with the quasigroup operations.
Derivational modal logic of real line with difference modality
Authors: Kudinov Andrey
Published: January 2018

We study derivational modal logic of real line with difference modality and prove that it has finite model property but does not have finite axiomatization.
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 checking

satisfiability 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 eliminating

or partially eliminating quantifiers. We also apply the algorithm for Presburger Arithmetic

formulas and evaluate it on formulas from a model checker for Duration Calculus [8]. We report on

experiments on different variants of the auxiliary procedures. So far, there is an edge to applying

SMT-TEST proposed in [10], while we found that a simpler approach which just eliminates quantified

variables per round is almost as good. Both approaches offer drastic improvements to applying

default 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 entities

which represent logical theories in much the same way that algebraic schemes

represent rings. These involve two components: a semantic spectral space

and a syntactic structure sheaf. As in the algebraic case, we can recover a

theory from its scheme representation (up to a conservative completion) and

the structure sheaf is local in a certain logical sense. From these ane pieces

we can build up a 2-category of logical schemes which share some of the nice

properties 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 the

correct-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.
A Modelling Pearl with Sortedness Constraints
Authors: Beldiceanu Nicolas , Carlsson Mats , Flener Pierre , Lorca Xavier , Pearson Justin , Petit Thierry , Prud'Homme Charles
Published: January 2018

Some constraint programming solvers and constraint modelling languages feature the SORT(L,P,S) constraint, which holds if S is a nondecreasing rearrangement of the list L, the permutation being made explicit by the optional list P. However, such sortedness constraints do not seem to be used much in practice. We argue that reasons for this neglect are that it is impossible to require the underlying sort to be stable, so that SORT cannot be guaranteed to be a total-function constraint, and that L cannot contain tuples of variables, some of which form the key for the sort. To overcome these limitations, we introduce the StableKeysort constraint, decompose it using existing constraints, and propose a propagator. This new constraint enables a powerful modelling idiom, which we illustrate by elegant and scalable models of two problems that are otherwise hard to encode as constraint programs.
Gödel logics and the fully boxed fragment of LTL
Authors: Baaz Matthias , Preining Norbert
Published: January 2018

In this paper we show that a very basic fragment of FO-LTL, the monadic fully boxed fragment (all connectives and quantifiers are guarded by P) is not recursively enumerable wrt validity and 1-satisfiability if three predicates are present. This result is obtained by reduction of the fully boxed fragment of FO-LTL to the Gödel logic G↓, the infinitely valued Gödel logic with truth values in [0,1] such that all but 0 are isolated. The result on 1-satisfiability is in no way symmetric to the result on validity as in classical logic: this is demonstrated by the analysis of G↑, the related infinitely-valued Gödel logic with truth values in [0, 1] such that all but 1 are isolated. Validity of the monadic fragment with at least two predicates is not recursively enumerable, 1-satisfiability of the monadic fragment is decidable.
Designing a solver competition: the QBFEVAL'10 case study
Authors: Peschiera Claudia , Pulina Luca , Tacchella Armando
Published: January 2018

In this paper we report about QBFEVAL'10, the seventh in a series of events established with the aim of assessing the advancements in reasoning about quantified Boolean formulas (QBFs). The paper discusses the results obtained and the evaluation setup, from the criteria used to select QBF instances down to the hardware infrastructure. We also discuss the current state-of-the-art in light of past challenges and we envision future research directions that are motivated by the results of QBFEVAL'10.
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 of

Satisfiability Modulo Theories (SMT). In recent years efficient approaches

for solving fixed-size bit-vector formulas have been developed. From

the theoretical point of view, only few results on the complexity of

fixed-size bit-vector logics have been published. In this paper we show

that some of these results only hold if unary encoding on the bit-width of

bit-vectors is used. We then consider fixed-size bit-vector logics with

binary encoded bit-width and establish new complexity results. Our proofs

show that binary encoding adds more expressiveness to bit-vector logics,

e.g. it makes fixed-size bit-vector logic even without uninterpreted

functions nor quantication NExpTime-complete. We also show that under

certain restrictions the increase of complexity when using binary encoding

can 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.
Tableau-Like Automata-Based Axiomatization for Propositional Linear Temporal Logic
Authors: Shilov Nikolay V.
Published: January 2018

Propositional Linear Temporal Logic (PLTL) is a very popular formalism for specification and verification of computer programs and systems. This extended abstract sketches a tableau-like axiomatization for PLTL based on automata-theoretic decision procedure coupled with tableau for local model checking of the propositional μ-Calculus.
Building Portfolios for the Protein Structure Prediction Problem
Authors: Arbelaez Alejandro , Hamadi Youssef , Sebag Michèle
Published: January 2018

This paper, concerned with the protein structure prediction problem, aims at automatically selecting the Constraint Satisfaction algorithm best suited to the problem instance at hand. The contribution is twofold. Firstly, the selection criterion is the quality (minimal cost) in expectation of the solution found after a fixed amount of time, as opposed to the expected runtime. Secondly, the presented approach, based on supervised Machine Learning algorithms, considers the original description of the protein structure problem, as opposed to the features related to the SAT or CSP encoding of the problem.
Quantified Boolean Formulas: Call the Plumber!
Authors: Lindsberger Josef , Maringele Alexander , Moser Georg
Published: January 2018

In this tool paper we describe a variation of Nintendo’s Super Mario World dubbed Super Formula World that creates its game maps based on an input quantified Boolean formula. Thus in Super Formula World, Mario, the plumber not only saves his girlfriend princess Peach, but also acts as a QBF solver as a side. The game is implemented in Java and platform independent. Our implementation rests on abstract frameworks by Aloupis et al. that allow the analysis of the computational complexity of a variety of famous video games. In particular it is a straightforward consequence of these results to provide a reduction from QSAT to Super Mario World. By specifying this reduction in a precise way we obtain the core engine of Super Formula World. Similarly Super Formula World implements a reduction from SAT to Super Mario Bros., yielding significantly simpler game worlds.
Practical Aspects of SAT Solving
Authors: Biere Armin
Published: January 2018

SAT solving techniques are used in many automated reasoning engines. This talk gives an overview on recent developments in practical aspects of SAT solver development. Beside improvements of the basic conflict driven clause learning (CDCL) algorithm, we also discuss improving and integrating advanced preprocessing techniques as inprocessing during search. The talk concludes with a brief overview on current trends in parallelizing SAT.
Integration of a Decentralised Pattern Matching: Venue for a New Paradigm Intermarriage
Authors: Haeri Seyed Hossein , Schupp Sibylle
Published: January 2018

We provide a new technique for pattern matching that is based on components for each match. The set of match statements and their order is open for configuration at the right time and takes place in a feature-oriented fashion. This gives rise to a solution to the Expression Problem in presence of defaults. It takes a lightweight discipline to develop components for our technique. Their use for configuration of the pattern match, however, is virtually automatic.
Implementing Different Proof Calculi for First-order Modal Logics
Authors: Benzmüller Christoph , Otten Jens , Raths Thomas
Published: January 2018

This extended abstract presents several new automated theorem proving systems for first-order modal logics and sketches their calculi and working principles. The abstract also summarizes the results of a recent comparative evaluation of these new provers.
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.
Dynamic sequent calculus for the logic of Epistemic Actions and Knowledge
Authors: Greco Giuseppe , Kurz Alexander , Palmigiano Alessandra
Published: January 2018

We develop a family of display-style, cut-free sequent calculi for dynamic epistemic logics on both an intuitionistic and a classical base. Like the standard display calculi, these calculi are modular: just by modifying the structural rules according to Dosen’s principle, these calculi are generalizable both to different Dynamic Logics (Epistemic, Deontic, etc.) and to different propositional bases (Linear, Relevant, etc.). Moreover, the rules they feature agree with the standard relational semantics for dynamic epistemic logics.
ARCH-COMP17 Category Report: Hybrid Systems with Piecewise Constant Dynamics
Authors: Frehse Goran , Abate Alessandro , Adzkiya Dieky , Bu Lei , Giacobbe Mirco
Published: January 2018

This report presents results of a friendly competition for formal verification of continuous and hybrid systems with piecewise constant dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2017. In its first edition, four tools have been applied to solve five different benchmark problems in the category for piecewise constant dynamics: BACH, Lyse, PHAVer, and VeriSiMPL. The result is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems with piecewise constant dynamics up to this date.
Dynamics of Argumentation Systems: A Basic Theory
Authors: Liao Beishui , Jin Li , Koons Rober
Published: January 2018

The changing of arguments and their attack relation is an intrinsic property of a variety of argumentation systems. So, it is very important to efficiently figure out how the status of arguments in a system evolves when the system is updated. However, unlike other areas of argumentation that have been deeply explored, such as argumentation semantics, proof theories, and algorithms, etc., dynamics of argumentation systems has been comparatively neglected. In this paper, we introduce a general theory (called a division-based method) to cope with this problem based on a new concept: the division of an argumentation framework. When an argumentation framework is updated, it is divided into three parts: an unaffected, an affected, and a conditioning part. The status of arguments in the unaffected sub-framework remains unchanged, while the status of the affected arguments is computed in a special argumentation framework (called a conditioned argumentation framework, or briefly CAF) that is composed of an affected part and a conditioning part. We have proved that under a certain semantics that satisfies the directionality criterion (complete, preferred, ideal, or grounded semantics), the extensions of the updated framework are equal to the result of a combination of the extensions of an unaffected sub-framework and sets of the extensions of a set of assigned CAFs. The theory shows that the complexity of computing the dynamics of argumentation will decrease to a lesser or greater extent, depending on the types of argumentation semantics, the topologies of argumentation frameworks, and the number of affected arguments with respect to an addition or a deletion. As a result, this theory is expected to be very useful in various kinds of argumentation systems where arguments and attacks are dynamics, due to the changing of underlying knowledge and information.
Possession as Linear Knowledge
Authors: Pfenning Frank
Published: January 2018

Epistemic logic analyzes reasoning governing localized knowledge, and is thus fundamental to multi- agent systems. Linear logic treats hypotheses as consumable resources, allowing us to model evolution of state. Combining principles from these two separate traditions into a single coherent logic allows us to represent localized consumable resources and their flow in a distributed system. The slogan “possession is linear knowledge” summarizes the underlying idea. We walk through the design of a linear epistemic logic and discuss its basic metatheoretic properties such as cut elimination. We illustrate its expressive power with several examples drawn from an ongoing effort to design and implement a linear epistemic logic programming language for multi-agent distributed systems.
Funayama's theorem revisited
Authors: Bezhanishvili Guram , Gabelaia David , Jibladze Mamuka
Published: January 2018

We revisit proofs of Funayama's theorem and extend Graetzer's proof to the case of a not necessarily complete lattice.
A Comprehensive Formal Solution for Access Control Policies Management: Defect Detection, Analysis and Risk Assessment
Authors: Jaidi Faouzi , Labbene Ayachi Faten , Bouhoula Adel
Published: January 2018

Nowadays, the access control is becoming increasingly important for open, ubiquitous and criti- cal systems. Nonetheless, efficient Administration, Management, Safety analysis and Risk assessment (AMSR) are recognized as fundamental and crucial challenges in todays access control infrastructures. In untrustworthy environment, the administration of an access control policy, which is a main secu- rity aspect, generally raises a critical analysis problem when the administration is distributed and/or potentially un-trusted users contribute to this process. Consequently, collusions attempts and inner threats may take place to generate crucial and invisible breaches to circumvent the policy. To address this issue, we introduce a rigorous and comprehensive solution for an efficient and secure management of access control policies. Our proposal gives a high visibility on the development process of an access control policy and allows in an elegant manner to detect, analyze and assess the risk associated to the policy defects. The strength of our proposal is that it relies on logic-like formalisms to ensure a high surety by verifying the correctness and the completeness of our formal reasoning. We rely on an example to illustrate the relevance of the proposal.
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 and

in particular in the context of automated termination analysis.

We propose two techniques to solve such constraints: (a) to model

them using Boolean functions and integer linear arithmetic and solve

them using an SMT solver (QF_LIA, in certain cases also QF_IDL);

and (b) to seek finite domain solutions by applying unary bit-blasting

and 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 when

solving them. In particular, we observe that good results are

obtained by unary bit-blasting, improving on previous proposals to

apply binary bit-blasting. Moreover, our results indicate that, for

our benchmarks, unary bit-blasting leads to better results than the

ones directly obtained by an SMT solver.
A Note on Turing’s Three Pioneering Initiatives and on Their Interplays
Authors: Kelemen Jozef
Published: January 2018

The purpose of this article is to remind three fundamental contributions by A. M. Turing to three important fields of contemporary science and engineering (theory of computation, artificial intelligence, and biocomputing), and to emphasize the connections between them. The article reminds and formulates resp., also three hypotheses related to the three initiatives and discuss in short their mutual interrelatedness.
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.
Linear Models of Computation and Program Learning
Authors: Bukatin Michael , Matthews Steve
Published: January 2018

We consider two classes of computations which admit taking linear combinations of execution runs: probabilistic sampling and generalized animation. We argue that the task of program learning should be more tractable for these architectures than for conventional deterministic programs. We look at the recent advances in the "sampling the samplers" paradigm in higher-order probabilistic programming. We also discuss connections between partial inconsistency, non-monotonic inference, and vector semantics.
Automatic Staging via Partial Evaluation Techniques
Authors: Asai Kenichi , Kameyama Yukiyoshi
Published: January 2018

Partial evaluation and staging are two of the well-known symbolic

manipulation techniques of programs which generate efficient

specialized code. On one hand, partial evaluation provides us with an

automatic means to separate a program into two (or more) stages but

its behavior is perceived as hard to control. On the other hand,

staging (or staged calculus) requires us to manually separate a

program but with full control over its behavior. In the previous

work, the first author introduced a framework to relate the two

techniques, giving a unified view to the two techniques. In this

paper, we extend the framework to handle the cross-stage persistence

(CSP) and show that the 2-level staging annotation obtained by the

automatic separation is the best staging annotation in a system where

CSP is allowed for base-type values only. In the presence of CSP for

higher-type values, on the other hand, there is no single annotation

that is better than all the other annotations.
Maximum likelihood pedigree reconstruction using integer programming
Authors: Cussens James
Published: January 2018

Pedigrees are `family trees' relating groups of individuals which can usefully be seen as Bayesian networks. The problem of finding a maximum likelihood pedigree from genotypic data is encoded as an integer linear programming problem. Two methods of ensuring that pedigrees are acyclic are considered. Results on obtaining maximum likelihood pedigrees relating 20, 46 and 59 individuals are presented. Running times for larger pedigrees depend strongly on the data used but generally compare well with those in the literature. Solving is particularly fast when allele frequency is uniform.
On and On the Temporal Way
Authors: Dixon Clare , Fisher Michael
Published: January 2018

"Up and Down the Temporal Way" was a paper published by Howard Barringer in the 1980s that used temporal logics to formally specify a lift system. Based on that temporal specification, we describe some advances and extensions to temporal specification and verification that the authors have been involved with since then.
Program Transformation for Program Verification
Authors: Pettorossi Alberto , Proietti Maurizio
Published: January 2018

We present a transformational approach to program verification and software model checking that uses three main ingredients:

(i) Constraint Logic Programming (CLP),

(ii) metaprogramming and program specialization, and

(iii) proof by transformation.