bluuebunny/crossref_metadata_2025_split huggingface dataset:
A Note on Program Specialization. What Syntactical Properties of Residual Programs Can Reveal?
Authors: Lisitsa Alexei , Nemytykh Andrei 
Published: January 2018

The paper presents two examples of non-traditional using of program specialization by Turchin's supercompilation method.In both cases we are interested in syntactical properties of residual programs produced by supercompilation.In the first example we apply supercompilation to a program encoding a word equation and as a result we obtain a program representing a graphdescribing the solution set of the word equation.The idea of the second example belongs to Alexandr V. Korlyukov. He considered an interpreter simulating the dynamic of the well known missionaries-cannibals puzzle. Supercompilation of the interpreter allows us to solve the puzzle.The interpreter may also be seen as an encoding of a non-deterministic protocol.
Benchmark: Quadrotor Attitude Control
Authors: Da Cunha A. E. C. 
Published: January 2018

We present a case study of attitude control for a quadrotor and propose the application of reachability analysis to enhance the robustness of the control design.The controller is to be implemented and tested using an experimental nano-quadrotor platform, the \emph{CrazyFlie}.We intend to use measured data to improve the models employed in the reachability analysis and, therefore, enhance the reliability of the controller design.
Generating Asymptotically Non-terminant Initial Variable Values for Linear Diagonalizable Programs.
Authors: Rebiha Rachid , Matringe Nadir , Moura Arnaldo Vieira 
Published: January 2018

We present the key notion of "asymptotically non-terminant initial variable values" for non-terminant loop programs. We show that those specific values are directly associated to inital variable values for which the loop program does not terminate.Considering linear diagonalizable programs, we describe powerful computational methods that generate automatically and symbolically a semi-linear space represented by a linear system of equalities and inequalities. Each element of this space provides us with asymptotically non-terminant initial variable values. Our approach is based on linear algebraic methods and results. We obtain conditions using a decomposition on a specific basis, involving the loop condition and the matrix encoding the instructions of the loop.
Making the Evolution of Graphical Models Visible
Authors: Baar Thomas , Bendaas Issam 
Published: January 2018

With adoption of the UML and other graphical languages by software industry,graphical models became a cornerstone in today's software development practice.As other artefacts such as program source code, graphical models evolve overtime and are, thus, put regularily under version control.In order to deeply understand the role an artefact plays within a project, it issometimes helpful to review the history of this artefact. While there arenumerous tools available that make it easy for a user to grasp the evolution oftextual files (or even portions of it), an adequate support for graphical fileshas remained to be an area of niche products.In this paper, we argue that a better support for reviewing the version historyof graphical files can facilitate the work with graphical models. In order tosupport this claim, we implemented a prototypcical tool that can extract anddisplay the version history of any graphical file stored in a GitHub-repository.In addition, users can annotate each version of a file with comments, whatturns our tool into a review tool for software projects. Recently, we started touse the tool is a software engineering course to give students better feedbackon complex UML models they have to develop iteratively.
Enhanced Gaussian Elimination in DPLL-based SAT Solvers
Authors: Soos Mate 
Published: January 2018

When cryptographical problems are treated in SAT solvers, they often contain large set of XOR constraints. Treating these XOR constraints through on-the-fly Gaussian elimination during solving has been shown to be a viable approach by Soos et al. [1]. We describe various enhancements to this scheme which increase the performance and mostly eliminate the need for manual tuning of parameters. With these enhancements, we were able achieve speedups of up to 29% on the Bivium and up to 45% on the Trivium ciphers, contrary to the 1-5% speedup achieved by the original scheme.[1] Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In Kullmann, O., ed.: Theory and Applications of Satisﬁability Testing — SAT 2009. Volume 5584 of Lecture Notes in Computer Science., Springer (2009) 244–257
Breeding Theorem Proving Heuristics with Genetic Algorithms
Authors: Schäfer Simon , Schulz Stephan 
Published: January 2018

First-order theorem provers have to search for proofs in an infinitespace of possible derivations. Proof search heuristics play a vitalrole for the practical performance of these systems. In the currentgeneration of saturation-based theorem provers like SPASS, E,Vampire or Prover~9, one of the most important decisions is theselection of the next clause to process with the given clausealgorithms. Provers offer a wide variety of basic clause evaluationfunctions, which can often be parameterized and combined in manydifferent ways. Finding good strategies is usually left to the usersor developers, often backed by large-scale experimentalevaluations. We describe a way to automatize this process usinggenetic algorithms, evaluating a population of different strategieson a test set, and applying mutation and crossover operators to goodstrategies to create the next generation. We describe the design andexperimental set-up, and report on first promising results.
On the Impact of Information Technologies on Society: an Historical Perspective through the Game of Chess
Authors: Prost Frederic 
Published: January 2018

The game of chess as always been viewed as an iconic representationof intellectual prowess. Since the very beginning of computerscience, the challenge of being able to program a computer capableof playing chess and beating humans has been alive and used both asa mark to measure hardware/software progresses and as an ongoingprogramming challenge leading to numerous discoveries. In the earlydays of computer science it was a topic for specialists. But ascomputers were democratized, and the strength of chess enginesbegan to increase, chess players started to appropriate tothemselves these new tools. We show how these interactions betweenthe world of chess and information technologies have been herald ofbroader social impacts of information technologies. The game ofchess, and more broadly the world of chess (chess players,literature, computer softwares and websites dedicated to chess,etc.), turns out to be a surprisingly and particularly sharpindicator of the changes induced in our everyday life by theinformation technologies. Moreover, in the same way that chess is amodelization of war that captures the raw features of strategicthinking, chess world can be seen as small society making the studyof the information technologies impact easier to analyze and tograsp.
Two-layer modal logics: from fuzzy logics to a general framework
Authors: Cintula Petr , Noguera Carles 
Published: January 2018

The idea of two-layer modal logics is inspired by the treatment of probability inside mathematical fuzzy logic, pioneered by Hajek and recentlystudied by numerous authors in numerous papers. Such logics are used in order to deal with a certain property of formulas of the base logic using a suitable `upper' logic (the seminal example being the probability of classical events formalized inside Lukasiewicz logic). The primary aim of this paper is to provide a new general framework for two-layer modal logics that encompasses the current state of the art and paves the way for future development. Diverting for the area of mathematical fuzzy logic, we show how one can construct such modal logic over an arbitrary non-classical logic (under certain technical requirements) with a modality interpreted by an arbitrary measure. We equip the resulting logics with a semantics of measured Kripke frames and prove corresponding completeness theorems. As an illustration of our results, we reprove Hajek's completeness result for Fuzzy Probability logic over Lukasiewicz logic.
From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry
Authors: Boutry Pierre , Braun Gabriel , Narboux Julien 
Published: January 2018

This paper describes the formalization of the arithmetization of Euclidean geometry in the Coq proof assistant.As a basis for this work, Tarski’s system of geometry was chosen for its well-known metamathematical properties.This work completes our formalization of the two-dimensional results contained in part one of Metamathematische Methoden in der Geometrie.We define the arithmetic operations geometrically and prove that they verify the properties of an ordered field.Then, we introduce cartesian coordinates, and provide an algebraic characterization of the main geometric predicates.In order to prove the characterization of the segment congruence relation, we provide a synthetic formal proof of two crucial theorems in geometry, namely the intercept and Pythagoras' theorems.The arithmetization of geometry justifies the use the algebraic automated deduction methods in geometry.We give an example of the use this formalization by deriving from Tarski's system of geometry a formal proof of theorems of nine points using Gröbner basis.
The computing power of Turing machine based on quantum logic
Authors: Shang Yun , Lu Xian , Lu Ruqian 
Published: January 2018

Turing machines based on quantum logic can solve undecidableproblems. In this paper we will give recursion-theoreticalcharacterization of the computational power of this kind of quantumTuring machines. In detail, for the unsharp case, it is proved that&amp;#931&lt;sup&gt;0&lt;/sup&gt;&lt;sub&gt;1&lt;/sub&gt;&amp;#8746&amp;#928&lt;sup&gt;0&lt;/sup&gt;&lt;sub&gt;1&lt;/sub&gt;&amp;#8838L&lt;sup&gt;T&lt;/sup&gt;&lt;sub&gt;d&lt;/sub&gt;(&amp;#949,&amp;#931)(L&lt;sup&gt;T&lt;/sup&gt;&lt;sub&gt;w&lt;/sub&gt;(&amp;#949,&amp;#931))&amp;#8838&amp;#928&lt;sup&gt;0&lt;/sup&gt;&lt;sub&gt;2&lt;/sub&gt;when the truth value lattice is locally finite and the operation &amp;#8743is computable, whereL&lt;sup&gt;T&lt;/sup&gt;&lt;sub&gt;d&lt;/sub&gt;(&amp;#949,&amp;#931)(L&lt;sup&gt;T&lt;/sup&gt;&lt;sub&gt;w&lt;/sub&gt;(&amp;#949,&amp;#931))denotes theclass of quantum language accepted by these Turing machine indepth-first model (respectively, width-first model);for the sharp case, we can obtain similar results for usual orthomodular lattices.
The Glory of the Past and Geometrical Concurrency
Authors: Prisacariu Cristian 
Published: January 2018

This paper contributes to the general understanding of the "geometrical model of concurrency" that was named higher dimensional automata (HDAs) by Pratt and van Glabbeek. In particular we provide some understanding of the modal logics for such models and their expressive power in terms of the bisimulation that can be captured.The geometric model of concurrency is interesting from two main reasons: its generality and expressiveness, and the natural way in which autoconcurrency and action refinement are captured.Logics for this model, though, are not well investigated, where a simple, yet adequate, modal logic over HDAs was only recently introduced.As this modal logic, with two existential modalities, "during" and "after", captures only split bisimulation, which is rather low in the spectrum of van Glabbeek and Vaandrager, the immediate question was what small extension of this logic could capture the more fine-grained hereditary history preserving bisimulation (hh)?In response, the work in this paper provides several insights. One is the fact that the geometrical aspect of HDAs makes it possible to use for capturing the hh-bisimulation, a standard modal logic that does not employ event variables, opposed to the two logics (over less expressive models) that we compare with. The logic that we investigate here uses standard backward-looking modalities (i.e., past modalities) and extends the previously introduced logic (called HDML) that had only forward, action-labelled, modalities.Since the direct proofs are rather intricate, we try to understand better the above issues by introducing a related model that we call ST-configuration structures, which extend the configuration structures of van Glabbeek and Plotkin. We relate this model to HDAs, and redefine and prove the earlier results in the light of this new model. These offer a different view on why the past modalities and geometrical concurrency capture the hereditary history preserving bisimulation.Additional correlating insights are also gained.
Real Analysis for Complex Systems
Authors: Platzer Andrè 
Published: January 2018

Formal verification techniques are used routinely in finite-state digital circuits. Theorem proving is also used successfully for infinite-state discrete systems. But many safety-critical computers are actually embedded in physical systems. Hybrid systems model complex physical systems as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. They arise frequently in many application domains, including aviation, automotive, railway, and robotics. There is a well-understood theory for proving programs. But what about complex physical systems? How can we prove that a hybrid system works as expected, e.g., an aircraft does not crash into another one?This talk illustrates the complexities and pitfalls of hybrid systems verification. It describes a theoretical and practical foundation for deductive verification of hybrid systems called differential dynamic logic. The proof calculus for this logic is interesting from a theoretical perspective, because it is a complete axiomatization of hybrid systems relative to differential equations. The approach is of considerable practical interest too. Its implementation in the theorem prover KeYmaera has been used successfully to verify collision avoidance properties in the European Train Control System and air traffic control systems. The number of dimensions and nonlinearities in they hybrid dynamics of these systems is surprisingly tricky such that they are still out of scope for other verification tools.
Beating the Productivity Checker Using Embedded Languages
Authors: Danielsson Nils Anders 
Published: January 2018

Some total languages, like Agda and Coq, allow the use of guarded corecursion to construct infinite values and proofs. Guarded corecursion is a form of recursion in which arbitrary recursive calls are allowed, as long as they are guarded by a coinductive constructor. Guardedness ensures that programs are productive, i.e. that every finite prefix of an infinite value can be computed in finite time. However, many productive programs are not guarded, and it can be nontrivial to put them in guarded form.This paper gives a method for turning a productive program into a guarded program. The method amounts to defining a problem-specific language as a data type, writing the program in the problem-specific language, and writing a guarded interpreter for this language.
Pandora's Box
Authors: Middelkoop Ronald , Huizing Cornelis , Kuiper Ruurd , Luit Erik J. 
Published: January 2018

An algebraic specification is viewed as a black box that rewrites input to a ``most basic'' canonical form. We argue that a canonical form should be given for each specific specification, to prevent ``cheating'' in the implementation. Furthermore, we argue that the definition of the canonical form may sometimes require semantic rather than syntactic information.To relate an OO implementation to a specification requires opening the black box to some extent; we assess the choices to be made here.
Laterally complete and projective hulls of semilinear residuated lattices
Authors: Gil-Férez José , Ledda Antonio , Tsinakis Constantine 
Published: January 2018

The existence of lateral completions of ℓ-groups is an old problem that was first solved, for conditionally complete vector lattices, by Nakano. The existence and uniqueness of lateral completions of representable ℓ-groups was first obtained as a consequence of the orthocompletions of Bernau, and later the proofs were simplified by Conrad, who also proved the existence and uniqueness of lateral completions of ℓ-groups with zero radical. Finally, Bernau solved the problem for ℓ-groups in general.In this work, we address the problem of the existence and uniqueness of lateral, projectable, and strongly projectable completions of residuated lattices. In particular, we push the methods of Conrad through to the case of the representable GMV-algebras.The leading idea is to construct, for any given semilinear residuated lattice, an orthocomplete extension such that the former is dense in the latter. This extension is obtained as the direct limit of a family of residuated lattices that are constructed using maximal partitions of the algebra of polars of the original residuated lattice.In order to complete the proof we still need another hypothesis, which is an abstraction of the condition of double negation in which commutativity and integrality have been dropped, and determines the wide class of Generalized MV-algebras. This, together with the density, allows us to obtain the completions of the given residuated lattice.
Satisfiability Checking and Query Answering for Large Ontologies
Authors: Weidenbach Christoph , Wischnewski Patrick 
Published: January 2018

In this paper we develop a sound, complete and terminating superposition calculusplus a query answering calculus for the BSH-Y2 fragment of theBernays-Schoenfinkel Horn class of first-order logic.BSH-Y2 can be used to represent expressive ontologies.In addition to checking consistency, our calculus supports query answeringfor queries with arbitrary quantifier alternations.Experiments on BSH-Y2 (fragments) of several large ontologies show that ourapproach advances the state of the art.
Bit-size reduction of triangular sets in two and three variables
Authors: Yamashita Tetsuro , Dahan Xavier 
Published: January 2018

At ISSAC 2004, Schost and D.introduced a transformation of triangular lexicographic Groebner basesgenerating a radical ideal of dimension zero,which reduces significantly the bit-size of coefficients.The case where the triangular lexicographic Groebner basis does not generate a radical idealis far more complicated. This work treats the case of n=2 variables, andin some extent the case of n=3 variables.It resorts to an extra operation, the squarefree factorization;nevertheless this operation has low complexity cost.But as soon as n&gt;2 variables a lack of simple and efficient gcd-like operationover non-reduced rings prevents to undertake meaningful algorithmic considerations.An implementation in Maple for the case n=2 confirms the expectedreduction of the expected size coefficients.
Priestley duality for (modal) N4-lattices
Authors: Jansana Ramon , Rivieccio Umberto 
Published: January 2018

N4-lattices are the algebraic semantics of paraconsistent Nelson logic, which was introduced as an inconsistency-tolerant counterpart of the better-known logic of Nelson. Paraconsistent Nelson logic combines interesting features of intuitionistic, classical and many-valued logics (e.g., Belnap-Dunn four-valued logic); recent work has shown that it can also be seen as one member of the wide family of substructural logics.The work we present here is a contribution towards a better topological understanding of the algebraic counterpart of paraconsistent Nelson logic, namely a variety of involutive lattices called N4-lattices.
Machine Learner for Automated Reasoning 0.4 and 0.5
Authors: Kaliszyk Cezary , Urban Josef , Vyskocil Jiri 
Published: January 2018

Machine Learner for Automated Reasoning (MaLARea) is a learning andreasoning system for proving in large formal libraries wherethousands of theorems are available when attacking a newconjecture, and a large number of related problems and proofs can be used tolearn specific theorem-proving knowledge. The last version of thesystem has by a large margin won the 2013 CASC LTB competition. Thispaper describes the motivation behind the methods used in MaLARea,discusses the general approach and the issues arising in evaluationof such system, and describes the Mizar@Turing100 and CASC'24versions of MaLARea.
A New Proof of P-time Completeness of Linear Lambda Calculus
Authors: Matsuoka Satoshi 
Published: January 2018

We give a new proof of P-time completeness ofthe Linear Lambda Calculus, which was originally given by H. Mairson in 2003.Our proof uses an essentially different Boolean type from the type that Mairson used.Moreover the correctness of our proof can be machined-checked using an implementation of Standard ML.
Symbolic WS1S
Authors: D'Antoni Loris , Veanes Margus 
Published: January 2018

We extend weak monadic second-order logic of one successor (WS1S) to symbolic alphabets byallowing character predicates to range over decidable first order theories and not just finite alphabets.We call this extension symbolic WS1S (s-WS1S). We then propose two decision procedures for such alogic: 1) we use symbolic automata to extend the classic reduction from WS1S to finite automata toour symbolic logic setting; 2) we show that every s-WS1S formula can be reduced to a WS1S formulathat preserves satisfiability, at the price of an exponential blow-up.
Computing with Metabolic Machines
Authors: Angione Claudio , Carapezza Giovanni , Costanza Jole , Lio Pietro , Nicosia Giuseppe 
Published: January 2018

If Turing were a first-year graduate student interested in computers,he would probably migrate into the field of computational biology. During his studies, he presenteda work about a mathematical and computational model of the morphogenesis process, in which chemical substancesreact together. Moreover, a protein can be thought of as a computational element, i.e. a processing unit, able totransform an input into an output signal. Thus, in a biochemical pathway, an enzyme reads the amount of reactants (substrates)and converts them in products. In this work, we consider the biochemical pathway in unicellular organisms (e.g. bacteria) as a living computer, and we are able to program it in order to obtain desired outputs.The genome sequence is thought of as an executable code specified by a set of commands in a sort of ad-hoc low-level programming language. Each combination of genes is coded as a string of bits $y \in \left \{ 0 , 1 \right \}^L$, each of which represents a gene set. By turning off a gene set, we turn off the chemical reaction associated with it. Through an optimal executable code stored in the ``memory'' of bacteria, we are able to simultaneously maximise the concentration of two or more metabolites of interest.Finally, we use the Robustness Analysis and a new Sensitivity Analysis method to investigate both the fragility of the computation carried out by bacteria and the most important entities in the mathematical relations used to model them.
Alternating Turing machines and the analytical hierarchy
Authors: Leivant Daniel 
Published: January 2018

We use notions originating in Computational Complexity to provide insight into the analogies between computational complexity and Higher Recursion Theory. We consider alternating Turing machines, but with a modified, global, definition of acceptance. We show that a language is accepted by such a machine iff it is Pi-1-1. Moreover, total alternating machines, which either accept or reject each input, accept precisely the hyper-arithmetical (Delta-1-1) languages. Also, bounding the permissible number of alternations we obtain a characterization of the levels of the arithmetical hierarchy..The novelty of these characterizations lies primarily in the use of finite computing devices, with finitary, discrete, computation steps. We thereby elucidate the correspondence between the polynomial-time and the arithmetical hierarchies, as well as that between the computably-enumerable, the inductive (Pi-1-1), and the PSpace languages.