bluuebunny/crossref_metadata_2025 huggingface dataset:
Modeling Organic Chemistry and Planning Organic Synthesis
Authors: Masoumi Arman , Antoniazzi Megan , Soutchanski Mikhail
Published: January 2018

Organic Synthesis is a computationally challenging practical problem concerned with constructing a target molecule from a set of initially available molecules via chemical reactions. This paper demonstrates how organic synthesis can be formulated as a planning problem in Artificial Intelligence, and how it can be explored using the state-of-the-art domain independent planners.

To this end, we develop a methodology to represent chemical molecules and generic reactions in PDDL 2.2, a version of the standardized Planning Domain Definition Language popular in AI. In our model, derived predicates define common functional groups and chemical classes in chemistry, and actions

correspond to generic chemical reactions. We develop a set of benchmark problems. Since PDDL is supported as an input language by many modern planners, our benchmark can be subsequently useful for

empirical assessment of the performance of various state-of-the-art planners.
SAT-Based Techniques for Integer Linear Constraints
Authors: Nieuwenhuis Robert
Published: January 2018

Conflict-Driven Clause-Learning (CDCL) SAT and SAT Modulo Theories (SMT) solvers are well known as workhorses for, e.g., formal verification applications. Here we discuss ways to go beyond by learning not only clauses, but also much more expressive constraints. We outline techniques for Integer Linear Programming (ILP), going first from SAT to SMT for ILP and then to SMT with on-the-fly bottleneck constraint encoding. Then we illustrate the power of learning full constraints, and the resulting methods for 0-1 ILP (Pseudo-Boolean solvers) and full ILP (Cutsat and IntSat), outlining difficulties and their solutions, giving examples and some intuition on why these techniques work so well.
The Uses of SAT Solvers in Vampire
Authors: Reger Giles , Suda Martin
Published: January 2018

Reasoning in a saturation-based first-order theorem prover is generally expensive involving complex term-indexing data structures and inferences such as subsumption resolution whose (worst case) running time is exponential in the length of the clause. In contrast, SAT solvers are very cheap, being able to solve large problems quickly and with relatively little memory overhead.

Consequently, utilising this cheap power within Vampire to carry out certain tasks has proven highly successful. We give an overview of the different ways that SAT solvers are utilised

within Vampire and discuss further ways in which this usage could be extended
Cuts for circular proofs
Authors: Fortier Jérôme , Santocanale Luigi
Published: January 2018

One of the authors introduced in [1] a calculus of

circular proofs for studying the computability arising from the

following categorical operations: finite products and coproducts,

initial algebras, final coalgebras. The calculus of

[1] is cut-free; yet, even if sound and complete for

provability, it lacks an important property for the semantics of

proofs, namely fullness w.r.t. the class of natural categorical models

called μ-bicomplete category in [2].

We fix, with this work, this problem by adding the cut rule to the

calculus. To this goal, we need to modifying the syntactical

constraints on the cycles of proofs so to ensure soundness of the

calculus and at same time local termination of cut-elimination. The

enhanced proof system fully represents arrows of the intended model, a

free μ-bicomplete category. We also describe a cut-elimination

procedure as a model of computation arising from the above mentioned

categorical operations. The procedure constructs a cut-free

proof-tree with infinite branches out of a finite circular proof with

cuts.

[1] Luigi Santocanale. A calculus of circular proofs and its categorical semantics. In Mogens Nielsen and Uffe Engberg, editors, FoSSaCS, volume 2303 of Lecture Notes in Computer Science, pages 357–371. Springer, 2002.

[2] Luigi Santocanale. μ-bicomplete categories and parity games. Theoretical Informatics and Applications, 36:195–227, September 2002.
Tool Demonstration of the FLATA Counter Automata Toolset
Authors: Bozga Marius , Iosif Radu , Konecny Filip , Vojnar Tomas
Published: January 2018

We demonstrate the FLATA tool for checking reachability in counter automata using techniques which have recently been developed (such as precise acceleration of self-loops labelled by DBMs or octagons) and/or which are still under development. Apart from analysing counter automata, FLATA allows one to also reduce the given counter automata while preserving reachability of designated control locations. For demonstrating the tool, we use counter automata obtained, e.g., by translation from list manipulating programs or hardware components.
Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny
Authors: Grewe Sylvia , Erdweg Sebastian , Mezini Mira
Published: January 2018

\noindent Developing provably sound type systems is a non-trivial task which, as of today, typically requires expert skills in formal methods and a considerable amount of time. Our Veritas~\cite{GreweErdwegWittmannMezini15} project aims at providing support for the development of soundness proofs of type systems and efficient type checker implementations from specifications of type systems. To this end, we investigate how to best automate typical steps within type soundness proofs.

\noindent In this paper, we focus on progress proofs for type systems of domain-specific languages. As a running example for such a type system, we model a subset SQL and augment it with a type system. We compare two different approaches for automating proof steps of the progress proofs for this type system against each other: firstly, our own tool Veritas, which translates proof goals and specifications automatically to TPTP~\cite{Sutcliffe98} and calls Vampire~\cite{KovacsV13} on them, and secondly, the programming language Dafny~\cite{Leino2010}, which translates proof goals and specifications to the intermediate verification language Boogie 2~\cite{Leino2008} and calls the SMT solver Z3~\cite{DeMoura2008} on them. We find that Vampire and Dafny are equally well-suited for automatically proving simple steps within progress proofs.
A Mathematica module for Conformal Geometric Algebra and Origami Folding
Authors: Kondo Mitsuhiro , Matsuo Takuya , Mizoguchi Yoshihiro , Ochiai Hiroyuki
Published: January 2018

We implemented a Mathematica module of CGA which includes functions to denote CGA elements and compute several operations in CGA. We can draw the figure in 3D space which is corresponding to a CGA element. Our draw function is using Gr\"{o}bner Basis for simplifying equations of figures. It can be used for any dimensional figures. One of our motivations is to realize 3D origami system using our own CGA Library. We follow the 2D computational origami system E-Origami-System developed by Ida et.al. and formulated simple fold operations in 3D by using CGA points and motions. Then, we proved some geometric theorems about origami properties by computing CGA equation formulas.
On Conditionals
Authors: Dietz Emmanuelle-Anna , Hölldobler Steffen , Pereira Luís Moniz
Published: January 2018

We discuss the evaluation of conditionals. Under classical logic a conditional of the form "A implies B" is semantically equivalent to "not A or B". However, psychological experiments have repeatedly shown that this is not how humans understand and use conditionals.

We introduce an innovative abstract reduction system under the three-valued Łukasiewicz logic and the weak completion semantics, that allows us to reason abductively and by revision with respect to conditionals, in three values. We discuss the strategy of minimal revision followed by abduction and discuss two notions of relevance.

Psychological experiments will need to ascertain if these strategies and notions, or a variant of them, correspond to how humans reason with conditionals.
Anemic Status Prediction using Multilayer Perceptron Neural Network Model
Authors: Yu Ching Hao , Bhatnagar Manas , Hogen Rachel , Mao Dilin , Farzindar Atefeh , Dhanireddy Kiran
Published: January 2018

Artificial Neural Network (ANN) has been well recognized as an effective tool in medical science. Medical data is complex, and currently collected data does not flow in a standardized way. Data complexity makes the outcomes associated with intra- operative blood management difficult to assess. Reliable evidence is needed to selectively define areas that can be improved and establish standard protocols across healthcare service lines to substantiate best practice in blood product utilization. The ANN is able to provide this evidence using automatic learning techniques to mine the hidden information under the medical data and come to conclusions.

Blood transfusions can be lifesaving and are used commonly in complex surgical cases. Blood transfusions come with associated risks and are costly. Anemia and clinical symptoms are currently used to determine whether a packed red blood cell transfusion is necessary. In this paper, we worked with unique datasets of intra- operative blood management collected from the electronic medical record of the Keck Medical Center of USC. We apply Multilayer Perceptron Neural Network to estimate missing values and predict the degree of post-operative anemia. Successful predictions of postoperative anemia may help inform medical practitioners whether there is a need for a further packed red blood cell transfusion.
Improving Statistical Linguistic Algorithms for Parsing Mathematics
Authors: Kaliszyk Cezary , Urban Josef , Vyskocil Jiri
Published: January 2018

In this paper we describe our combined statistical/semantic parsing method based on the CYK chart-parsing algorithm augmented with limited internal typechecking and external ATP filtering. This method was previously evaluated on parsing ambiguous mathematical expressions over the informalized Flyspeck corpus of 20000 theorems. We first discuss the motivation and drawbacks of the first version of the CYK-based component of the algorithm, and then we propose and implement a more sophisticated approach based on better statistical model of mathematical data structures.
Deep Network Guided Proof Search
Authors: Loos Sarah , Irving Geoffrey , Szegedy Christian , Kaliszyk Cezary
Published: January 2018

Deep learning techniques lie at the heart of several significant AI advances in recent years including object recognition and detection, image captioning, machine translation, speech recognition and synthesis, and playing the game of Go.

Automated first-order theorem provers can aid in the formalization and verification of mathematical theorems and play a crucial role in program analysis, theory reasoning, security, interpolation, and system verification.

Here we suggest deep learning based guidance in the proof search of the theorem prover E. We train and compare several deep neural network models on the traces of existing ATP proofs of Mizar statements and use them to select processed clauses during proof search. We give experimental evidence that with a hybrid, two-phase approach, deep learning based guidance can significantly reduce the average number of proof search steps while increasing the number of theorems proved.

Using a few proof guidance strategies that leverage deep neural networks, we have found first-order proofs of 7.36% of the first-order logic translations of the Mizar Mathematical Library theorems that did not previously have ATP generated proofs. This increases the ratio of statements in the corpus with ATP generated proofs from 56% to 59%.
Multiple Ant Colony Optimization for Single Depot Multiple Trip Vehicle Routing Problems
Authors: Ye Zhengmao , Mohamadian Habib
Published: January 2018

The multiple trip vehicle routing problem involves several sequences of routes. Working shift of single vehicle can be scheduled in multiple trips. It is suitable for urban areas where the vehicle has very limited size and capacity over short travel distances. The size and capacity limit also requires the vehicle should be vacated frequently. As a result, the vehicle could be used in different trips as long as the total time or distance is not exceeded. Various approaches are developed to solve the vehicle routing problem (VRP). Except for the simplest cases, VRP is always a computationally complex issue in order to optimize the objective function in terms or both time and expense. Ant colony optimization (ACO) has been introduced to solve the vehicle routing problem. The multiple ant colony system is proposed to search for alternative trails between the source and destination so as to minimize (fuel consumption, distance, time) among numerous geographically scattered routes. The objective is to design adaptive routing so as to balance loads among congesting city networks and to be adaptable to connection failures. As the route number increases, each route becomes less densely packed. It can be viewed as the vehicle scheduling problem with capacity constraints. The proposed scheme is applied to typical cases of vehicle routing problems with a single depot and flexible trip numbers. Results show feasibility and effectiveness of the approach.
Compass-free Navigation of Mazes
Authors: Scott Phil , Fleuriot Jacques
Published: January 2018

If you find yourself in a corridor of a standard maze, a sure and easy way to escape

is to simply pick the left (or right) wall, and then follow it along its twists and

turns and around the dead-ends till you eventually arrive at the exit. But what

happens when you cannot tell left from right? What if you cannot tell North from

South? What if you cannot judge distances, and have no idea what it means to follow

a wall in a given direction?

The possibility of escape in these circumstances is suggested in the statement of an

unproven theorem given in David Hilbert's celebrated /Foundations of Geometry/, in

which he effectively claimed that a standard maze could be fully navigated using

axioms and concepts based /solely/ on the relations of points lying on lines in a

specified order.

We discuss our algorithm for this surprisingly challenging version of the maze

navigation problem, and our HOL Light verification of its correctness from Hilbert's

axioms.
A Benchmark for Component-based Hybrid Systems Safety Verification
Authors: Müller Andreas , Mitsch Stefan , Retschitzegger Werner , Schwinger Wieland , Platzer André
Published: January 2018

At scale, formal verification of hybrid systems is challenging, but a potential remedy is the observation that systems often come with a number of natural components with certain local responsibilities. Ideally, such a compartmentalization into more manageable components also translates to hybrid systems verification, so that safety properties about the whole system can be derived from local verification results. We propose a benchmark consisting of a sequence of three case studies, where components interact to achieve system safety. The baseline for the benchmark is the verification effort from a monolithic fashion (i.e., the entire system without splitting it into components). We describe how to split the system models used in these case studies into components with local responsibilities, and what is expected about their interaction to guarantee system safety. The benchmark can be used to assess the performance, automation, and verification features of component-based verification approaches.
The Info-Computation Turn in Physics
Authors: Belfer Israel
Published: January 2018

Modern Computation and Information theories have had significant impact on science in the 20th century - in theory and application. This influence is tracked (through a generalized, Information-laden scientific Style of Reasoning denoting the Information-theoretical and Computational turn in science), with a focus on the information processing and transfer metaphors and descriptive tools prevalent in current physics. Implementation of Information-Theoretical concepts produces such mathematical physical developments as Black-Hole Thermodynamics (BHTD) and the Black-Hole Wars (Suskind, 2008). The treatment of physical systems as information processing systems drives such branches of physics as Quantum Information Theory (QIT). The common Informational basis of computation and communication brings about a foundational shift in scientific reasoning with deep – potentially problematic as well as intriguing – philosophical ramifications. Models of computation and of physics
Automated analysis of Stateflow models
Authors: Bourbouh Hamza , Garoche Pierre-Loic , Garion Christophe , Gurfinkel Arie , Kahsai Temesghen , Thirioux Xavier
Published: January 2018

Stateflow is a widely used modeling framework for embedded and cyberphysical systems where control software interacts with physical processes. In this work, we present a framework and a fully automated safety verification technique for Stateflow models. Our approach is two-folded: (i) we faithfully compile Stateflow models into hierarchical state machines, and (ii) we use automated logic-based verification engine to decide the validity of safety properties. The starting point of our approach is a denotational semantics of Stateflow. We propose a compilation process using continuation-passing style (CPS) denotational semantics. Our compilation technique preserves the structural and modal behavior of the system. The overall approach is implemented as an open source toolbox that can be integrated into the existing Mathworks Simulink/Stateflow modeling framework. We present preliminary experimental evaluations that illustrate the effectiveness of our approach in code generation and safety verification of industrial scale Stateflow models.
New CNF Features and Formula Classification
Authors: Alfonso Enrique , Manthey Norbert
Published: January 2018

In this paper we first present three new features for classifying CNF formulas. These features are based on the structural information of the formula and consider AND-gates as well as exactly-one constraints. Next, we use these features to construct a machine learning approach to select a SAT solver configuration for CNF formulas with random decision forests. Based on this classification task we can show that our new features are useful compared to existing features. Since the computation time for these features is small, the constructed classifier improves the performance of the SAT solvers on application and hand crafted benchmarks. On the other hand, the comparison shows that the set of new features also results in a better classification.
A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories
Authors: Bax Joshua
Published: January 2018

Generalised Model Finding (GMF) is a quantifier instantiation heuristic for the superposition calculus in the presence of interpreted theories with arbitrarily quantified free function symbols ranging into theory sorts.

The free function symbols are approximated by finite partial function graphs along with some simplifying assumptions which are iteratively refined.

Here we present an outline of the GMF approach, give an improvement

that addresses some of these and then present some

ideas for extending it with concepts from instantiation based theorem proving.
Conflict Resolution in Structured Argumentation
Authors: Baláž Martin , Frtús Jozef , Homola Martin
Published: January 2018

While several interesting argumentation-based semantics for

defeasible logic programs have been proposed, to our best

knowledge, none of these approaches is able to fully handle the

closure under strict rules in a sufficient manner: they are either

not closed, or they use workarounds such as transposition of rules

which violates the desired directionality of logic programming

rules.

We propose a novel argumentation-based semantics, in which the

status of arguments is determined by attacks between newly

introduced conflict resolutions instead of attacks between

arguments. We show that the semantics is closed w.r.t. strict

rules and respects the directionality of inference rules, as well

as other desired properties previously published in the

literature.
Towards a Practical Decision Procedure for Uniform Interpolants of EL-TBoxes - a Proof-Theoretic Approach
Authors: Ludwig Michel , Walther Dirk
Published: January 2018

We show how the problem of deciding the existence of uniform interpolants of TBoxes formulated in the Description Logic \EL can be divided into three subproblems based on a characterisation of the logical difference between \EL-TBoxes. We propose a proof-theoretic decision procedure for subsumer interpolants of general TBoxes formulated in the Description Logic \EL, solving one of these subproblems. A subsumer interpolant of a TBox depends on a signature and on a concept name. It is a TBox formulated using symbols from the signature only such that, both, it follows from the original TBox and it exactly entails the subsumers formulated in the signature that follow from the concept name \wrt~the original TBox. Our decision procedure first constructs a graph that exactly represents the part of original TBox that is describable using signature symbols only. Subsequently, it is checked whether a graph-representation of the original TBox can be simulated by the constructed graph, in which case a subsumer interpolant exists. We also evaluate our procedure by applying a prototype implementation on several biomedical ontologies.
Spectra of finitely presented lattice-ordered Abelian groups and MV-algebras, part 2
Authors: Marra Vincenzo , Mcneill Daniel , Pedrini Andrea
Published: January 2018

This is the second part of a series of two abstracts, the first being by Andrea Pedrini. For background and notation on lattice-ordered Abelian groups, vector lattices and Q-vector lattices, and their spectral spaces, please see her submission.

We consider the tools of Stone duality and the absolute applied to lattice-ordered Abelian groups, vector lattices and Q-vector lattices. Given a lattice-ordered Abelian group or Q-vector lattice, G, this leads to an interesting parallel between Min(G) and the absolute of Max(G).
Reasoning about Translation Lookaside Buffers
Authors: Syeda Hira , Klein Gerwin
Published: January 2018

The main security mechanism for enforcing memory isolation in operating systems is provided by page tables. The hardware-implemented Translation Lookaside Buffer (TLB) caches these, and therefore the TLB and its consistency with memory are security crit- ical for OS kernels, including formally verified kernels such as seL4. If performance is paramount, this consistency can be subtle to achieve; yet, all major formally verified ker- nels currently leave the TLB as an assumption.

In this paper, we present a formal model of the Memory Management Unit (MMU) for the ARM architecture which includes the TLB, its maintenance operations, and its derived properties. We integrate this specification into the Cambridge ARM model. We derive sufficient conditions for TLB consistency, and we abstract away the functional details of the MMU for simpler reasoning about executions in the presence of cached address translation, including complete and partial walks.
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
Authors: Doligez Damien , Kriener Jael , Lamport Leslie , Libal Tomer , Merz Stephan
Published: January 2018

We present a syntactic abstraction method to reason about first-order modal logics by using theorem provers for standard first-order logic and for propositional modal logic.
A Survey of Elementary Object Systems
Authors: Köhler-Bußmeier Michael
Published: January 2018

This contribution presents the formalism of ElementaryObjectSystems (Eos). Object nets are Petri nets which have Petri nets as tokens – an approach known as the nets-within-nets paradigm. One central aim of this contribution is to compile all our previous works ded- icated to certain aspects of Eos together with recent yet unpublished results within one self-contained presentation. Since object nets in general are immediately Turing complete, we introduce the restricted class of elementary object nets which restrict the nesting of nets to the depth of two. In this work we study the relationship of Eos to existing Petri net formalisms. It turns out that Eos are more powerful than classical p/t nets which is demonstrated by the fact that e.g. reachability and liveness become undecidable problems for Eos. Despite these undecidability results other properties can be extended to Eos using a monotonicity argument similar to that for p/t nets. Also linear algebraic techniques, especially the theory of linear invariants and semiflows, can be extended in an appropriate way. The invariant calculus for Eos even enjoys the property of compositionality, i.e. invariants of the whole system can be composed of invariants of the object nets, which reduces the computational effort. To obtain a finer level of insight we also studied several classes like pure, minimal, or semi-bounded Eos. Among these variants the subclass of generalised state machines is worth mentioning since it combines the decidability of many theoretically interesting properties with a quite rich practical modelling expressiveness.
Progress in Automating Higher-Order Ontology Reasoning
Authors: Benzmüller Christoph , Pease Adam
Published: January 2018

We report on the application of higher-order automated theorem proving in ontology reasoning. Concretely, we have integrated the Sigma knowledge engineering environment and the Suggested Upper-Level Ontology SUMO with the higher-order theorem prover LEO-II. The basis for this integration is a translation from SUMO representations into the new typed higher-order form representation language TPTP THF. We illustrate the benefits of our integration with examples, report on experiments and analyze open challenges.
An Operational Semantics for Network Datalog
Authors: Nigam Vivek , Jia Limin , Wang Anduo , Thau Loo Boon , Scedrov Andre
Published: January 2018

Network Datalog (NDlog) is a recursive query language that extends Datalog by allowing programs to be distributed in a network. In our initial efforts to formally specify NDlog's operational semantics, we have found several problems with the current evaluation algorithm being used, including unsound results, unintended multiple derivations of the same table entry, and divergence. In this paper, we make a first step towards correcting these problems by formally specifying a new operational semantics for NDlog and proving its correctness for the fragment of non-recursive programs. We also argue that if termination is guaranteed, then the results also extend to recursive programs. Finally, we identify a number of potential implementation improvements to NDlog.
CDCL with Less Destructive Backtracking through Partial Ordering
Authors: Monnet Anthony , Villemaire Roger
Published: January 2018

Conflict-driven clause learning is currently the most efficient complete algorithm for satisfiability solving. However, a conflict-directed backtrack deletes potentially large portions of the current assignment that have no direct relation with the conflict. In this paper, we show that the CDCL algorithm can be generalized with a partial ordering on decision levels. This allows keeping levels that would otherwise be undone during backtracking under the usual total ordering. We implement partial ordering CDCL in a state-of-the-art CDCL solver and show that it significantly ameliorates satisfiability solving on some series of benchmarks.
Overview of COLIEE 2017
Authors: Kano Yoshinobu , Kim Mi-Young , Goebel Randy , Satoh Ken
Published: January 2018

We present the evaluation of the legal question answering Competition on Legal Information Extraction/Entailment (COLIEE) 2017. The COLIEE 2017 Task consists of two sub-Tasks: legal information retrieval (Task 1), and recognizing entailment between articles and queries (Task 2). Participation was open to any group based on any approach, and the tasks attracted 10 teams. We received 9 submissions to Task 1 (for a total of 17 runs), and 8 submissions to Task 2 (for a total of 20 runs).
An Automated Framework for Exploitable Fault Identification in Block Ciphers – A Data Mining Approach
Authors: Saha Sayandeep , Kumar Ujjawal , Mukhopadhyay Debdeep , Dasgupta Pallab
Published: January 2018

Characterization of all possible faults in a cryptosystem exploitable for fault attacks is a problem which is of both theoretical and practical interest for the cryptographic community. The complete knowledge of exploitable fault space is desirable while designing optimal countermeasures for any given crypto-

implementation. In this paper, we address the exploitable fault characterization problem in the context of Differential Fault Analysis (DFA) attacks on block ciphers. The formidable size of the fault spaces demands an automated albeit fast mechanism for verifying each individual fault instance and neither the

traditional, cipher-specific, manual DFA techniques nor the generic and automated Algebraic Fault Attacks (AFA) [10] fulfill these criteria. Further, the diversified structures of different block ciphers suggest that such an automation should be equally applicable to any block cipher. This work presents an automated

framework for DFA identification, fulfilling all aforementioned criteria, which, instead of performing the attack just estimates the attack complexity for each individual fault instance. A generic and extendable data-mining assisted dynamic analysis framework capable of capturing a large class of DFA distinguishers

is devised, along with a graph-based complexity analysis scheme. The framework significantly outperforms another recently proposed one [6], in terms of attack class coverage and automation effort. Experimental evaluation on AES and PRESENT establishes the effectiveness of the proposed framework in detecting

most of the known DFAs, which eventually enables the characterization of the exploitable fault space.
QWeS2T for Type-Safe Web Programming
Authors: Sans Thierry , Cervesato Iliano
Published: January 2018

Web applications (webapps) are very popular because they are easy to prototype and they can make use of other webapps, supplied by third parties, as building blocks. Yet, writing correct webapps is complex because developers are required to reason about distributed computation and to write code using heterogeneous languages, often not originally designed with distributed computing in mind. Testing is the common way to catch bugs as current technologies provide limited support. There are doubts this can scale up to meet the expectations of more sophisticated web applications. In this paper, we propose an abstraction that provides simple primitives to manage the two main forms of distributed computation found on the web: remote procedure calls (code executed on a server on behalf of a client) and mobile code (server code executed on a client). We embody this abstraction in a type-safe language with localized static typechecking that we call QWeSST and for which we have implemented a working prototype. We use it to express interaction patterns commonly found on the Web as well more sophisticated forms that are beyond current web technologies.
C2PDLS: A Combination of Combinatory and Converse PDL with Substitutions
Authors: Brenas Jon Hael , Echahed Rachid , Strecker Martin
Published: January 2018

We introduce a logic called C2PDLS, motivated by some reasoning

about graph rewriting systems. C2PDLS is an extension of both

combinatory propositional dynamic logic, usually written CPDL,

and converse propositional dynamic logic, usually written CPDL

too. In addition to the existing features of both CPDLs, the

introduced logic offers the possibility to use the notion of

substitutions à la Hoare within its formulae. Such substitutions

reflect the effect of some actions on graph structures such as

addition or deletion of edges or nodes. These last features led

us to introduce restricted universal roles over subsets of the

universe. We propose a sound and complete deductive system for

C2PDLS and show that its validity problem is decidable.
Unranked Anti-Unification with Hedge and Context Variables
Authors: Baumgartner Alexander , Kutsia Temur
Published: January 2018

In this work we study anti-unification for unranked terms and hedges, permitting context and hedge variables.

Hedges are sequences of unranked terms.

The anti-unification problem of two hedges s and q is concerned with finding their generalization, a hedge g such that both s and q are instances of g under some substitutions.

Context variables are used to abstract vertical differences in the input hedges,

and hedge variables are used to abstract horizontal differences.

A rule based system in Huet's style will be presented, which computes a set of

generalizations of input hedges and records all the differences.

The computed generalizations are least general among a certain class of generalizations.
Symbolic Approach for Side-Channel Resistance Analysis of Masked Assembly Codes
Authors: Ben El Ouahma Inès , Meunier Quentin , Heydemann Karine , Encrenaz Emmanuelle
Published: January 2018

Masking is a popular countermeasure against side-channel attacks, that randomizes secret data with random and uniform variables called masks. At software level, masking is usually added in the source code and its effectiveness needs to be verified. In this paper, we propose a symbolic method to verify side-channel robustness of masked programs. The analysis is performed at the assembly level since compilation and optimizations may alter the added protections. Our proposed method aims to verify that intermediate computations are statistically independent from secret variables using defined distribution inference rules. We verify the first round of a masked AES in 22s and show that some secure algorithms or source codes are not leakage-free in their assembly implementations.
A Modular Approach of Decision-Making in the Context of Robot Navigation in Domestic Environments
Authors: Kirsch Alexandra
Published: January 2018

Decision processes in Artificial Intelligence are often organized hierarchically. One example is robot navigation with a global path planner and a local executor. This paper examines whether a shift from optimizing the two typical modules in navigation towards a dynamic interaction of more, not necessarily hierarchically linked, modules leads to robust navigation behavior. We empirically evaluate different organizations of modules for navigation in a simulated household with a simulated PR2 robot.
Experiments on the feasibility of using a floating-point simplex in an SMT solver
Authors: Caminha Barbosa de Oliveira Diego , Monniaux David
Published: January 2018

SMT solvers use simplex-based decision procedures to solve decision problems whose formulas are quantifier-free and atoms are linear constraints over the rationals. State-of-art SMT solvers use rational (exact) simplex implementations, which have shown good performance for typical software, hardware or protocol verification problems over the years.

Yet, most other scientific and technical fields use (inexact) floating-point computations, which are deemed far more efficient than exact ones.

It is therefore tempting to use a floating-point simplex implementation inside an SMT solver, though special precautions must be taken to avoid unsoundness.

In this work, we describe experimental results, over common benchmarks (SMT-LIB) of the integration of a mature floating-point implementation of the simplex algorithm (GLPK) into an existing SMT solver (OpenSMT).

We investigate whether commonly cited reasons for and against the use of floating-point truly apply to real cases from verification problems.
A Sparse Representation of High-Dimensional Input Spaces Based on an Augmented Growing Neural Gas
Authors: Kerdels Jochen , Peters Gabriele
Published: January 2018

\noindent The growing neural gas (GNG) algorithm is an unsupervised learning method that is able to approximate the structure of its input space with a network of prototypes. Each prototype represents a local input space region and neighboring prototypes in the GNG network correspond to neighboring regions in input space. Here we address two problems that can arise when using the GNG algorithm. First, the GNG network structure becomes less and less meaningful with increasing dimensionality of the input space as typical distance measures like the Euclidean distance loose their expressiveness in higher dimensions. Second, the GNG itself does not provide a form of output that retains the discovered neighborhood relations when compared with common distance measures. We show that a GNG augmented with {\em local input space histograms} can mitigate both of these problems. We define a sparse vector representation as output of the augmented GNG that preserves important neighborhood relations while pruning erroneous relations that were introduced due to effects of high dimensionality.
Automated Reasoning in the Simulation of Evolvable Systems
Authors: Afifi Djihed , Rydeheard David , Barringer Howard
Published: January 2018

We present a novel application of automated theorem proving for the simulation of computational systems. The computational systems we consider are evolvable, i.e. may reconfigure their structure and programs at run-time. In [1], a logical framework for describing such systems is introduced. The underlying logic of this framework allows us to build a simulation engine for executing system specifications. This engine makes intensive use of automated theorem proving – when running a simulation, almost all computational steps are those of a theorem prover. In this paper, we present this novel combination of a logical setting involving meta-level logics and large sets of formulae for system description, together with theorem proving requirements which involve often slowly changing specifications with the need for rapid assessment of deducibility and consistency. We will evaluate the suitability of several theorem provers for this application.
Harmony Search Approach for Patient Scheduling in Emergency Laboratories
Authors: Boudali Imen , Mokhtar Nihel
Published: January 2018

This paper deals with the problem of scheduling prioritized patient in emergency department laboratories according to a triage factor. The problem is considered as a flexible open shop scheduling problem with the objective of minimizing the total completion time of prioritized patients. In this research, patient scheduling is addressed with a harmony search algorithm with wheel-roulette selection technique. Then, a comparative study is performed by considering results of genetic algorithm. Simulations on real data from emergency department show that the proposed approach improves significantly the total completion time of patients especially those with severe conditions.
Feasibility as a gradual notion
Authors: Behounek Libor
Published: January 2018

The notion of feasibility, applicable in various areas related to logic, is arguably of gradual nature---some tasks are more feasible than others. The possibility of modeling a gradual notion of feasibility in t-norm logics is brought forward and illustrated on the gradual notions of feasible number, feasible knowledge, feasible formula, and feasible computability.
Automated Higher-order Reasoning about Quantales
Authors: Dang Han-Hing , Höfner Peter
Published: January 2018

Originally developed as an algebraic characterisation for quantum mechanics, the algebraic structure of quantales nowadays finds widespread applications ranging from (non-commutative) logics to hybrid systems. We present an approach to bring reasoning about quantales into the realm of (fully) automated theorem proving. This will yield automation in various (new) fields of applications in the future. To achieve this goal and to receive a general approach (independent of any particular theorem prover), we use the TPTP Problem Library for higher-order logic. In particular, we give an encoding of quantales in the typed higher-order form (THF) and present some theorems about quantales which can be proved fully automatically. We further present prospective applications for our approach and discuss practical experiences using THF.
Implementing a stepper using delimited continuations
Authors: Cong Youyou , Asai Kenichi
Published: January 2018

A stepper is a tool that displays all the steps of a program's execution. To implement a stepper, we need to reconstruct each intermediate program from the current redex and the evaluation context. We regard evaluation contexts as delimited continuations and capture them using the control operators shift and reset. This enables us to implement a stepper concisely by writing an evaluator that is close to the standard big-step interpreter. Our implementation is a non-trivial application of shift and reset.
The use of types in designing unification algorithms: two case studies
Authors: Erbatur Serdar , Escobar Santiago , Narendran Paliath
Published: January 2018

We discuss the use of type systems in a non-strict sense

when designing unification algorithms. We first give a

new (rule-based) algorithm for an equational theory which represents

a property of El-Gamal signature schemes and show how

a type system can be used to prove termination of the algorithm.

Lastly, we reproduce termination result for theory of partial

exponentiation given earlier.
Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4
Authors: Kumar Ramana
Published: January 2018

OpenTheory is being used for the first time (in work to be described at ITP 2013) as a tool in a larger project, as opposed to in an example demonstrating OpenTheory's capability. The tool works, demonstrating its viability. But it does not work completely smoothly, because the use case is somewhat at odds with OpenTheory's primary design goals. In this extended abstract, we explore the tensions between the goals that OpenTheory-like systems might have, and question the relative importance of various kinds of use. My hope is that describing issues arising from work in progress will stimulate fruitful discussion relevant to the development of proof exchange systems.
Implied Constraints for Automaton Constraints
Authors: Francisco Maria Andreina , Flener Pierre , Pearson Justin
Published: January 2018

Automata allow many constraints on sequences of variables to be specified in a high-level way for constraint programming solvers. An automaton with accumulators induces a decomposition of the specified constraint into a conjunction of constraints with existing inference algorithms, called propagators. Towards improving propagation, we design a fully automated tool that selects, in an off-line process, constraints that are implied by such a decomposition. We show that a suitable problem-specific choice among the tool-selected implied constraints can considerably improve solving time and propagation, both on a decomposition in isolation and on entire constraint problems containing the decomposition.
SMT-Based CPS Parameter Synthesis
Authors: Riener Heinz , Koenighofer Robert , Fey Goerschwin , Bloem Roderick
Published: January 2018

We present a simple, yet flexible parameter synthesis and repair approach for Cyber-Physical Systems (CPS). The user defines the behavior of a CPS, a set of (un)safe states, and a generic template for an inductive invariant using Satisfiability Modulo Theories (SMT) formulas. Counterexample-Guided Inductive Synthesis (CEGIS) is then used to compute values for open parameters and a concrete invariant to prove that all unsafe states are unreachable. Using templates for expressions, the approach can also be used for CPS repair. We present a proof-of-concept tool, optimizations, and first experiments.
Replaceability and the Substitutability Hierarchy for Constraint Satisfaction Problems
Authors: Freuder Eugene , Wallace Richard
Published: January 2018

Problem simplification is a topic of continuing interest in the field of constraint satisfaction. In this paper we examine properties associated with the basic idea of substitutability and show how certain forms of substitutability

can be organized into a strict hierarchy. One of these properties, here called replaceability, has been identified by other authors as being of special interest. In this work we confirm these earlier claims and show that replaceability is significant because it is the most general property in the hierarchy that allows inferences from local to global versions of this property. To make use of this discovery, we introduce two algorithms for establishing neighbourhood replaceability, and we present an initial experimental examination of these algorithms including ways to improve their performance through ordering heuristics and various kinds of inference.
Application-Independent and Integration-Friendly Natural Language Understanding
Authors: Eppe Manfred , Trott Sean , Raghuram Vivek , Feldman Jerome , Janin Adam
Published: January 2018

Natural Language Understanding (NLU) has been a long-standing goal of AI and many related fields, but it is often dismissed as very hard to solve. NLU is required complex flexible systems that take action without further human intervention. This inherently involves strong semantic (meaning) capabilities to parse queries and commands correctly and with high confidence, because an error by a robot or automated vehicle could be disastrous. We describe an implemented general framework, the ECG2 system, that supports the deployment of NLU systems over a wide range of application domains. The framework is based on decades of research on embodied action-oriented semantics and efficient computational realization of a deep semantic analyzer (parser). This makes it linguistically much more flexible, general and reliable than existing shallow approaches that process language without considering its deeper semantics. In this paper we describe our work from a Computer Science perspective of system integration, and show why our particular architecture requires considerably less effort to connect the system to new applications compared to other language processing tools.
Challenges for Safe Autonomous Flight
Authors: Scherer Sebastian
Published: January 2018

Autonomy holds a great promise by improving the applications, safety, and efficiency of flight. If little operator input is necessary, unmanned rotorcraft have a wide range of applications ranging from cargo delivery to inspection. Currently unmanned rotorcraft are underutilized because they either have to fly on preplanned missions at high altitude or require careful teleoperation. A capable autonomous rotorcraft will have to react quickly to previously unknown obstacles, land at unprepared sites, and fly with semantic information to enable long-term autonomy in cluttered environments.

In this talk we give an overview of how autonomy systems are currently designed and how pushing the performance and safety of these systems challenges current verification paradigms. In particular we will address how a supervisory layer in the motion planning system can improve safety, a sensor steering system enables us to optimize coverage for safe trajectories, and how semantic information can help us guide the rotorcraft.