bluuebunny/crossref_metadata_2025 huggingface dataset:
Matching Jobs and Resumes: a Deep Collaborative Filtering Task
Authors: Schmitt Thomas , Caillou Phillipe , Sebag Michele
Published: January 2018

This paper tackles the automatic matching of job seekers and recruiters, based on the logs of a recruitment agency (CVs, job announcements and application clicks). Preliminary experiments reveal that good recommendation performances in collaborative filtering mode (emitting recommendations for a known recruiter using the click history) co-exist with poor performances in cold start mode (emitting recommendations based on the job announcement only). A tentative interpretation for these results is proposed, claiming that job seekers and recruiters $-$ whose mother tongue is French $-$ yet do not speak the same language. As first contribution, this paper shows that the information inferred from their interactions differs from the information contained in the CVs and job announcements.

The second contribution is the hybrid system \XX (MAtching JObs and REsumes), where a deep neural net is trained to match the collaborative filtering representation properties. The experimental validation demonstrates \XX merits, with good matching performances in cold start mode.
A Syntactic Characterization of the Gabbay-de Jongh Logics
Authors: Goudsmit Jeroen
Published: January 2018

Skura syntactically characterised intuitionistic propositional logic among all intermediate logics by means of a Łukasiewicz-style refutation system. Another such syntactic characterisation is given by Iemhoff in terms of admissible rules. Here we offer a bridge between these results. That is to say, we provide sufficient conditions under which admissible rules yield a refutation system fully characterising the logic. In particular, we give a characterisation of the Gabbay–de Jongh logics by means of refutation systems employing ideas from admissibility.
The Architecture of Inference from SMT to ETB
Authors: Shankar Natarajan
Published: January 2018

Modularity plays a central role in logical reasoning. We want to be

able to reuse proofs, proof patterns, theories, and specialized

reasoning procedures. Architectures that support modularity have been

developed at all levels of inference: SAT solvers, theory solvers,

combination solvers and rewriters, SMT solvers, simplifiers, rewriters,

and tactics-based interactive theorem provers. Prior work has mostly

focused on fine-grained modular inference. However, with the

availability of a diverse range of high-quality inference tools, it has

become important to systematically integrate these big components into

robust toolchains. At SRI, we have been developing a framework called

the Evidential Tool Bus (ETB) as a distributed platform for the

coarse-grained integration of inference components into flexible,

scriptable workflows. The talk describes the architecture of ETB along

with some motivating applications.
Higher order interpretation for higher order complexity
Authors: Hainry Emmanuel , Péchoux Romain
Published: January 2018

We design an interpretation-based theory of higher-order functions that is well-suited for the complexity analysis of a standard higher- order functional language a` la ml. We manage to express the interpretation of a given program in terms of a least fixpoint and we show that when restricted to functions bounded by higher-order polynomials, they characterize exactly classes of tractable functions known as Basic Feasible Functions at any order.
Temporal Query Answering in DL-Lite with Negation
Authors: Borgwardt Stefan , Thost Veronika
Published: January 2018

Ontology-based query answering augments classical query answering in databases by adopting the open-world assumption and by including domain knowledge provided by an ontology. We investigate temporal query answering w.r.t. ontologies formulated in DL-Lite, a family of description logics that captures the conceptual features of relational databases and was tailored for efficient query answering. We consider a recently proposed temporal query language that combines conjunctive queries with the operators of propositional linear temporal logic (LTL). In particular, we consider negation in the ontology and query language, and study both data and combined complexity of query entailment.
MiniAgda: Integrating Sized and Dependent Types
Authors: Abel Andreas
Published: January 2018

Sized types are a modular and theoretically well-understood tool for checking termination of recursive and productivity of corecursive definitions. The essential idea is to track structural descent and guardedness in the type system to make termination checking robust and suitable for strong abstractions like higher-order functions and polymorphism.

To study the application of sized types to proof assistants and programming languages based on dependent type theory, we have implemented a core language with explicit handling of sizes. New considerations were necessary to soundly integrate sized types with dependencies and pattern matching, which was made possible by modern concepts such as inaccessible patterns and parametric function spaces.
Entropic Hopf algebras
Authors: Romanowska Anna , Smith Jonathan
Published: January 2018

Classically, Hopf algebras are defined on the basis of modules over commutative rings. The present study seeks to extend the Hopf algebra formalism to a more general universal-algebraic setting, entropic varieties, including (pointed) sets, barycentric algebras, semilattices, and commutative monoids. The concept of a setlike (or grouplike) element may be defined, and group algebras constructed, in any such variety. In particular, group algebras within the variety of barycentric algebras consist precisely of finitely supported probability distributions on groups. For primitive elements and group quantum doubles, the natural universal-algebraic classes are entropic Jónsson-Tarski varieties (such as semilattices or commutative monoids). There, the tensor algebra on any algebra is a bialgebra, and the set of primitive elements of a Hopf algebra forms an abelian group. Coalgebra congruences on comonoids in entropic varieties are also studied.
Incorporating Hypothetical Views and Extended Recursion into SQL Database Systems
Authors: Aranda Gabriel , Nieva Susana , Saenz-Perez Fernando , Sánchez-Hernández Jaime
Published: January 2018

Current database systems supporting recursive SQL impose

restrictions on queries such as linearity, and do not implement mutual

recursion. In a previous work we presented the language and prototype

R-SQL to overcome those drawbacks. Now we introduce a formalization

and an implementation of the database system HR-SQL that, in addition to extended recursion, incorporates hypothetical reasoning in a novel

way which cannot be found in any other SQL system, allowing both positive and negative assumptions. The formalization extends the fixpoint

semantics of R-SQL. The implementation improves the eciency of the

previous prototype and is integrated in a commercial DBMS.
Towards Constraint-Solving over Higher-Order Unbounded Datatypes using Formal Methods Tools
Authors: Leuschel Michael
Published: January 2018

We argue that formal methods such as B can be used to conveniently express a wide

range of constraint satisfaction problems. We also show that some problems can be solved

quite eectively by existing formal methods tools such as Alloy or ProB. We illustrate our

claim on several examples. Our approach is particularly interesting when a high assurance

of correctness is required. Indeed, validation and double checking of solutions is available

for certain formal methods tools and formal proof can be applied to establish important

properties or provide unambiguous semantics to problem specications. The experiments

also provide interesting insights about the eectiveness of existing formal method tools,

and highlight interesting avenues for future improvement.

1
Distributed Control Synthesis
Authors: Peled Doron , Schewe Sven
Published: January 2018

Synthesis of control for distributed systems is considered to be undecidable problem, under the assumption that control is performed by supervisors syncrhonizing with the original processes and selectively blocking or supporting the enabled transitions. We describe a decidable distributed control problem, where additional communications are allowed between supervisors. In this way, we synthesize control for invariants, reachability, repeated reachability and parity conditions. Special attention is given to reducing the number of added communications.
Quantification and Analysis of the Resilience of Two Swarm Intelligent Algorithms
Authors: Varughese Joshua Cherian , Thenius Ronald , Schmickl Thomas , Wotawa Franz
Published: January 2018

Nature showcases swarms of animals and insects performing various complex tasks efficiently where capabilities of individuals alone in the swarm are often quite limited. Swarm intelligence is observed when agents in the swarm follow simple rules which enable the swarm to perform certain complex tasks. This decentralized approach of nature has inspired the artificial intelligence community to apply this approach to engineered systems. Such systems are said to have no single point of failure and thus tend be more resilient. The aim of this paper is to put this notion of resilience to the test and quantify the robustness of two swarm algorithms, namely ¸"swarmtaxis" and "FSTaxis". The first simulation results of the effects of introducing an impairment in agent-to-agent interactions in these two swarm algorithms are presented in this paper. While the FSTaxis algorithm shows a much higher resilience to agent-to-agent communication failure, both the FSTaxis and swarmtaxis algorithms are found to have a non-zero tolerance towards such failures.
An SMT-based approach to automated configuration
Authors: Michel Raphaël , Hubaux Arnaud , Ganesh Vijay , Heymans Patrick
Published: January 2018

We present a novel use of SMT solvers: configuration problems. Configuration problems are everywhere and particularly in product lines, where different yet similar products can be built from a common set of assets, which are then chosen, specialized and combined to form a product. Designing a product line boils down to enumerate the different parts of the products and the rules for combining them. These rules are often expressed as constraints. Various categories of constraint solvers exist, but SMT-solvers appear to be a solution of choice for configuration problem. In this paper, we present the configuration problem, we briefly introduce how we represent this type of problem and we map this representation to the input language of an STP solver able to support the various types of constraints found in configuration problems.
Unsatisfiability Proofs for Parallel SAT Solver Portfolios with Clause Sharing and Inprocessing
Authors: Philipp Tobias
Published: January 2018

State-of-the-art SAT solvers are highly tuned systematic-search procedures augmented with formula simplification techniques. They emit unsatisfiability proofs in the DRAT format to guarantee correctness of their answers. However, the DRAT format is inadequate to model some parallel SAT solvers such as the award-winning system \plingeling. In \plingeling, each solver in the portfolio applies clause addition and elimination techniques. Clause sharing is restricted to clauses that do not contain melted literals. In this paper, we develop a transition system that models the computation of such parallel portfolio solvers. The transition system allows us to formally reason about portfolio solvers, and we show that the formalism is sound and complete. Based on the formalism, we derive a new proof format, called parallel DRAT, which can be used to certify UNSAT answers.
Towards Formal Reliability Analysis of Logistics Service Supply Chains using Theorem Proving
Authors: Ahmed Waqar , Hasan Osman , Tahar Sofiene
Published: January 2018

Logistics service supply chains (LSSCs) are composed of several nodes, with distinct behaviors, that ensure moving a product or service from a producer to consumer. Given the usage of LSSC in many safety-critical applications, such as hospitals, it is very important to ensure their reliable operation. For this purpose, many LSSC structures are modelled using Reliability Block Diagrams (RBDs) and their reliability is assessed using paper-and-pencil proofs or computer simulations. Due to their inherent incompleteness, these analysis techniques cannot ensure accurate reliability analysis results. In order to overcome this limitation, we propose to use higher-order-logic (HOL) theorem proving to conduct the RBD-based reliability analysis of LSSCs in this paper. In particular, we present the higher-order-logic formalizations of LSSNs with different and same types of capacities. As an illustrative example, we also present the formal reliability analysis of a simple three-node corporation.
Residuated Lattices, Regular Languages, and Burnside Problem
Authors: Horcik Rostislav
Published: January 2018

In this talk we are going to explore an interesting connection between the famous Burnside problem for groups, regular languages, and residuated lattices.
Reconciling Population and Agent Models for Crowd Dynamics
Authors: Bracciali Andrea , Hillston Jane , Latella Diego , Massink Mieke
Published: January 2018

We propose an approach to the quantitative modelling of crowd dy- namics, viz. the behaviour of systems of large numbers of mobile agents. The approach relies on a stochastic process algebra as specification lan- guage (BioPEPA), and combines stochastic simulation techniques and continuous fluid flow approximation. The approach encompasses the agent modelling viewpoint, as system behaviour emerges from the specified agent interaction, and the population modelling viewpoint, when continu- ous analysis is used. The result is expressive, as we will show by discussing a few examples, and efficient, by the adoption of the fluid flow analysis techniques, which approximate system dynamics as continuous variations of population.
The Thousands of Models for Theorem Provers (TMTP) Model Library - First Steps
Authors: Sutcliffe Geoff , Schulz Stephan
Published: January 2018

The TPTP World is a well established infrastructure that supports research,

development, and deployment of Automated Theorem Proving (ATP) systems for

classical logics.

The TPTP world includes the TPTP problem library, the TSTP solution library,

standards for writing ATP problems and reporting ATP solutions, and it

provides tools and services for processing ATP problems and solutions.

This work describes a new component of the TPTP world - the Thousands of

Models for Theorem Provers (TMTP) Model Library.

This is a library of models for identified axiomatizations built from

axiom sets in the TPTP problem library, along with functions for efficiently

evaluating formulae wrt models, and tools for examining and processing

the models.

The TMTP supports the development of semantically guided theorem proving

ATP systems, provide examples for developers of model finding ATP systems,

and provides insights into the semantics of axiomatizations.
Evaluation Opportunities in Mechanized Theories
Authors: Hurd Joe
Published: January 2018

This invited talk will look at logic solvers through the application lens of constructing and processing a theory library of mechanized mathematics. In fact, constructing and processing theories are two distinct applications, and each will be considered in turn. Construction is carried out by formalizing a mathematical theory using an interactive theorem prover, and logic solvers can remove much of the drudgery by automating common reasoning tasks. At the theory library level, logic solvers can provide assistance with theory engineering tasks such as compressing theories, managing dependencies, and constructing new theories from reusable theory components.
Generic CDCL -- A Formalization of Modern Propositional Satisfiability Solvers
Authors: Hölldobler Steffen , Manthey Norbert , Philipp Tobias , Steinke Peter
Published: January 2018

Modern propositional satisfiability (or SAT) solvers are very powerful due to recent developments on the underlying data structures, the used heuristics to guide the search, the deduction techniques to infer knowledge, and the formula simplification techniques that are used during pre- and inprocessing. However, when all these techniques are put together, the soundness of the combined algorithm is not guaranteed any more, and understanding the complex dependencies becomes non-trivial.

In this paper we present a small set of rules that allows to model modern SAT solvers in terms of a state transition system. With these rules all techniques which are applied in modern SAT solvers can be modeled adequately. Furthermore, we show that this set of rules results is sound, complete and confluent. Finnaly, we compare the proposed transition system to related systems, and show how widely used solving techniques can be modeled.
HyReach: A Reachability Tool for Linear Hybrid Systems Based on Support Functions
Authors: Ben Makhlouf Ibtissem , Hansen Norman , Kowalewski Stefan
Published: January 2018

We present HyReach, a MATLAB-based toolbox for reachability

analysis of linear hybrid systems based on support functions. The

main goal of HyReach is to provide a single graphical user interface for

easily configurable reachability analysis on different systems. HyReach

offers a number of known algorithms for the computation of reachable

sets within modes. These are combined with various approaches of handling

mode invariants, guard intersection computations and transition

strategies. Furthermore, plug-ins like the MPT and CVX toolboxes complement

the existing MATLAB optimization toolbox to increase the variety

of optimization algorithms for the computation of support functions.

HyReach supports both textual and graphical inputs and outputs, allowing

for flexibility and seamlessness in workflow and processing of data.

We illustrate these features with examples in this paper.
On (finite) distributive lattices with antitone involutions
Authors: Kühr Jan , Botur Michal
Published: January 2018

Finite distributive lattices with antitone involutions (= basic algebras) are studied; it is proved that their underlying lattices are isomorphic to direct products of finite chains, and hence finite distributive basic algebras can be constructed by “perturbing” finite MV-algebras, and moreover, under certain natural conditions, they even coincide with finite MV-algebras.
Implementing Connection Calculi for First-order Modal Logics
Authors: Otten Jens
Published: January 2018

An implementation of an automated theorem prover for first-order modal logic is presented that works for the constant, cumulative and varying domains of the modal logics D, T, S4 and S5. It is based on the (classical) connection calculus and uses prefixes (or world paths) and a prefix unification algorithm to capture the restrictions given by the Kripke semantics of the standard modal logics. This permits a modular and elegant treatment of the considered modal logics and yields an efficient implementation. Details of the calculus, the implementation and performance results on the QMLTP problem library are presented.
Proof rules for the dialogical logic N
Authors: Alama Jesse , Uckelman Sara L.
Published: January 2018

We outline the beginnings of a proof-theory for the dialogical logic N introduced in [Alama & Uckelman, 2010].
BDI: A New Decidable First-order Clause Class
Authors: Lamotte-Schubert Manuel , Weidenbach Christoph
Published: January 2018

BDI (Bounded Depth Increase) is a new decidable

first-order clause class. It strictly includes

known classes such as PVD. The arity

of function and predicate symbols as well as the

shape of atoms is not restricted in BDI. Instead

the shape of "cycles" in resolution inferences is

restricted such that the depth of generated clauses

may increase but is still finitely bound.

The BDI class is motivated by real world problems

where function terms are used to represent record structures.

We show that the hyper-resolution calculus modulo

redundancy elimination terminates on BDI clause sets.

Employing this result to the ordered resolution calculus,

we can also prove termination of ordered resolution on BDI,

yielding a more efficient decision procedure.
Formal Development of Distributed Enumeration Algorithms By Refinement-Based Techniques
Authors: Boussabbeh Maha , Tounsi Mohamed , Hadj Kacem Ahmed , Mosbah Mohamed
Published: January 2018

The enumeration problem addresses a collection of important algorithmic issues related to distributed computations. Among existing solutions, we are interested on the seminal algorithm of Mazurkiewicz, based on local computations. Our paper contributes to the design of a correct-by-construction enumeration algorithm. The main idea relies upon the development of the problem following a top/down approach

that can be supported by an incremental process controlled by the refinement of models. Event-B modelling language is supporting our methodological. Our main objective is to provide a verified component for distributed enumeration in

order to be used and extended for solving other problems of distributed algorithms.
From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction
Authors: Brown Chad E. , Rizkallah Christine
Published: January 2018

We define a translation that maps higher-order formulas provable in a classical extensional setting to semantically equivalent formulas provable in an intuitionistic intensional setting. For the classical extensional higher-order proof system we define a Henkin-complete tableau calculus. For the intuitionistic intensional higher-order proof system we give a natural deduction calculus. We prove that tableau provability of a formula implies provability of a translated formula in the natural deduction calculus. Implicit in this proof is a method for translating classical extensional tableau refutations into intuitionistic intensional natural deduction proofs.
Polymorphic+Typeclass Superposition
Authors: Wand Daniel
Published: January 2018

We present an extension of superposition that natively handles a polymorphic type system extended with type classes, thus eliminating the need for type encodings when used by an interactive theorem prover like Isabelle/HOL. We describe syntax, typing rules, semantics, the polymorphic superposition calculus and an evaluation on a problem set that is generated from Isabelle/HOL theories. Our evaluation shows that native polymorphic+typeclass performance compares favorably to monomorphisation, a highly efficient but incomplete way of dealing with polymorphism.
Constraint-Based Modeling in Systems Biology
Authors: Bockmayr Alexander
Published: January 2018

The idea of constraint-based modeling in systems biology is to describe a biological system by a set of constraints, i.e., by pieces of partial information about its structure and dynamics. Using constraint-based reasoning one may then draw conclusions about the possible system behaviors.

In this talk, we will focus on constraint-based modeling techniques for regulatory networks starting from the discrete logical formalism of René Thomas. In this framework, logic and constraints arise at two different levels. On the one hand, Boolean or multi-valued logic formulae provide a natural way to represent the structure of a regulatory network, which is given by positive and negative interactions (i.e., activation and inhibition) between the network components. On the other hand, temporal logic formulae (e.g. CTL) may be used to reason about the dynamics of the system, represented by a state transition graph or Kripke model.
A modified parallel F4 algorithm for shared and distributed memory architectures
Authors: Neumann Severin
Published: January 2018

In applications of symbolic computation an often required but complex procedure is the computation of Gröbner bases and hence it is obvious

to realize parallel algorithms to compute them. There are parallel flavours of the F4 algorithm using the special structure of the occurring matrices

to speed up the reduction. In this paper we start from this and present modifications allowing efficient computations of Gröbner bases on parallel architectures

using shared as well as distributed memory. To achieve this we concentrate on one objective: reducing the memory consumption and avoiding communication overhead.

We remove unrequired steps of the reduction, split the columns of the matrix in blocks for distribution and review the effectiveness of the SIMPLIFY function.

Finally we provide benchmarks with up to 256 distributed threads of an implementation which will be available at https://github.com/svrnm/parallelGBC.
On the constant domains principle and its weakened versions in the Kripke sheaf semantics
Authors: Skvortsov Dmitry
Published: January 2018

Two weakened versions of the constant domains principle D are considered.

The Kripke sheaf incompleteness of superintuitionistic predicate logics,

obtained by adding these weakened principles to predicate versions

of superintuitionistic propositional logics of finite slices, is claimed.

So a difference between these principles and the principle D is shown.

The incompleteness proof uses the functor semantics.
On Reducing Clause DataBase in Glucose
Authors: Li Chu Min , Xiao Fan , Xu Ruchu
Published: January 2018

Modern CDCL SAT solvers generally save the variable value when backtracking. We propose a new measure called nbSAT based on the saved assignment to predict the usefulness of a learnt clause when reducing clause database in Glucose 3.0. Roughly speaking, The nbSAT value of a learnt clause is equal to the number of literals satised by the current partial assignment plus the number of other literals that would be satised by the saved assignment. We study the nbSAT measure by empirically show that it may be more accurate than the LBD measure originally used in Glucose. Based on this study, we implement an improvement in Glucose 3.0 to remove half of learnt clauses with large nbSAT values instead of half of clauses with large LBD values. This improvement, together with a resolution method to keep the learnt clauses or resolvents produced using a learnt clause that subsume an original clause, makes Glucose 3.0 more eective for the application and crafted instances from the SAT 2014 competition.
The chess example in Turing's Mind paper is really about ambiguity
Authors: Fokker Jeroen
Published: January 2018

In his paper `Computing machinery and intelligence',

Turing introduces a rather trivial chess problem as a

conversation piece in an example Turing test.

The example is about much more than computers playing chess:

it has a hidden message that is about resolving ambiguity

and knowledge representation,

probably inserted by Turing as an easter egg for us to find.
Blocked Clauses in First-Order Logic
Authors: Kiesl Benjamin , Suda Martin , Seidl Martina , Tompits Hans , Biere Armin
Published: January 2018

Blocked clauses provide the basis for powerful reasoning techniques used in SAT, QBF, and DQBF solving. Their definition, which relies on a simple syntactic criterion, guarantees that they are both redundant and easy to find. In this paper, we lift the notion of blocked clauses to first-order logic. We introduce two types of blocked clauses, one for first-order logic with equality and the other for first-order logic without equality, and prove their redundancy. In addition, we give a polynomial algorithm for checking whether a clause is blocked. Based on our new notions of blocking, we implemented a novel first-order preprocessing tool. Our experiments showed that many first-order problems in the TPTP library contain a large number of blocked clauses whose elimination can improve the performance of modern theorem provers, especially on satisfiable problem instances.
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 graph

describing 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.
Temporal Patterns for Document Verification
Authors: Jaksic Mirjana , Freitag Burkhard
Published: January 2018

In this paper we present a novel user-friendly high-level approach to the specification of temporal properties of web documents which can be used for verification purposes. The method described is based on specification patterns supporting an incremental construction of commonly used consistency criteria. We show that our approach fills the gap between a temporal logic such as CTL as a powerful tool for specifying consistency criteria for web documents and users that maintain documents but have no or very limited knowledge about the specification formalism. An empiric assessment of the usability of specification patterns for web documents confirms that a pattern based specification shows significantly better results than the direct specification with CTL.
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.
Reachability Modulo Theory Library
Authors: Alberti Francesco , Bruttomesso Roberto , Ghilardi Silvio , Ranise Silvio , Sharygina Natasha
Published: January 2018

Reachability analysis of infinite-state systems plays a central role in many verification tasks. In the last decade, SMT-Solvers have been exploited within many verification tools to discharge proof obligations arising from reachability analysis. Despite this, as of today there is no standard language to deal with transition systems specified in the SMT-LIB format. This paper is a first proposal for a new SMT-based verification language that is suitable for defining transition systems and safety properties.
Alignnment of RNA with Structures of Unlimited Complexity
Authors: Dal Palù Alessandro , Möhl Mathias , Will Sebastian
Published: January 2018

Sequence-structure alignment of RNAs with arbitrary secondary structures is Max-SNP-hard. Therefore, the problem of RNA alignment is commonly restricted to nested structure, where dynamic programming yields efficient solutions. However, nested structure cannot model pseudoknots or even more complex structural dependencies. Nevertheless those dependencies are essential and conserved features of many RNAs. Only few existing approaches deal with crossings of limited complexity or arbitrary crossing structures. Here, we present a constraint approach for alignment of structures in the even more general class of structures with unlimited complexity. Our central contribution is a new RNA alignment propagator. It is based on an efficient O(n2) relaxation of the RNA alignment problem. Specifically, our approach Carna solves the alignment problem for sequences with given input structure of unlimited complexity. Carna is implemented using Gecode.
Automated Theorem Proving using the TPTP Process Instruction Language
Authors: Nassar Muhammad , Sutcliffe Geoff
Published: January 2018

The TPTP (Thousands of Problems for Theorem Provers) World is a well established infrastructure for Automated Theorem Proving (ATP). In the context of the TPTP World, the TPTP Process Instruction (TPI) language provides capabilities to input, output and organize logical formulae, and control the execution of ATP systems. This paper reviews the TPI language, describes a shell interpreter for the language, and demonstrates their use in theorem proving.
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 over

time and are, thus, put regularily under version control.

In order to deeply understand the role an artefact plays within a project, it is

sometimes helpful to review the history of this artefact. While there are

numerous tools available that make it easy for a user to grasp the evolution of

textual files (or even portions of it), an adequate support for graphical files

has remained to be an area of niche products.

In this paper, we argue that a better support for reviewing the version history

of graphical files can facilitate the work with graphical models. In order to

support this claim, we implemented a prototypcical tool that can extract and

display the version history of any graphical file stored in a GitHub-repository.

In addition, users can annotate each version of a file with comments, what

turns our tool into a review tool for software projects. Recently, we started to

use the tool is a software engineering course to give students better feedback

on 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 infinite

space of possible derivations. Proof search heuristics play a vital

role for the practical performance of these systems. In the current

generation of saturation-based theorem provers like SPASS, E,

Vampire or Prover~9, one of the most important decisions is the

selection of the next clause to process with the given clause

algorithms. Provers offer a wide variety of basic clause evaluation

functions, which can often be parameterized and combined in many

different ways. Finding good strategies is usually left to the users

or developers, often backed by large-scale experimental

evaluations. We describe a way to automatize this process using

genetic algorithms, evaluating a population of different strategies

on a test set, and applying mutation and crossover operators to good

strategies to create the next generation. We describe the design and

experimental set-up, and report on first promising results.
Recognizing entailments in legal texts using sentence encoding-based and decomposable attention models
Authors: Truong Son Nguyen , Viet Anh Phan , Le Minh Nguyen
Published: January 2018

This paper presents an end-to-end question answering system for legal texts. This system includes two main phases. In the first phase, our system will retrieve articles from Japanese Civil Code that are relevant with the given question using the cosine distance after the given question and articles are converted into vectors using TF-IDF weighting scheme. Then, a ranking model can be applied to re-rank these retrieved articles using a learning to rank algorithm and annotated corpus. In the second phase, we adapted two deep learning models, which has been proposed for the Natural language inference task, to check the entailment relationship between a question and its related articles including a sentence encoding-based model and a decomposable attention model. Experimental results show that our approaches can be a promising approach for information extraction/entailment in legal texts.
Synchronizing Constrained Horn Clauses
Authors: Mordvinov Dmitry , Fedyukovich Grigory
Published: January 2018

Simultaneous occurrences of multiple recurrence relations in a system of non-linear constrained Horn clauses are crucial for proving its satis ability. A solution of such system is often inexpressible in the constraint language. We propose to synchronize recurrent computations, thus increasing the chances for a solution to be found. We introduce a notion of CHC product allowing to formulate a lightweight iterative algorithm of merging recurrent computations into groups and prove its soundness. The evaluation over a set of systems handling lists and linear integer arithmetic confirms that the transformed systems are drastically more simple to solve than the original ones.
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 representation

of intellectual prowess. Since the very beginning of computer

science, the challenge of being able to program a computer capable

of playing chess and beating humans has been alive and used both as

a mark to measure hardware/software progresses and as an ongoing

programming challenge leading to numerous discoveries. In the early

days of computer science it was a topic for specialists. But as

computers were democratized, and the strength of chess engines

began to increase, chess players started to appropriate to

themselves these new tools. We show how these interactions between

the world of chess and information technologies have been herald of

broader social impacts of information technologies. The game of

chess, 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 sharp

indicator of the changes induced in our everyday life by the

information technologies. Moreover, in the same way that chess is a

modelization of war that captures the raw features of strategic

thinking, chess world can be seen as small society making the study

of the information technologies impact easier to analyze and to

grasp.
Canonical formulas via locally finite reducts and generalized dualities
Authors: Bezhanishvili Nick
Published: January 2018

The method of canonical formulas is a powerful tool for investigating intuitionistic and modal logics. In this talk I will discuss an algebraic approach to this method. I will mostly concentrate on the case of intuitionistic logic. But I will also review the case of modal logic and possible generalizations to substructural logic.
General Recursion and Formal Topology
Authors: Sacerdoti Coen Claudio , Valentini Silvio
Published: January 2018

It is well known that general recursion cannot be expressed within Martin-Löf's type theory and that various approaches have been proposed to overcome this problem still maintaining the termination of the computation of the typable terms. In this work we propose a new approach to this problem based on the use of inductively generated formal topologies.
Complexity of LTL Model-Checking for Safe Object Nets
Authors: Köhler-Bußmeier Michael , Heitmann Frank
Published: January 2018

In this paper we discuss the complexity of LTL model checking of safe Elementary Object Nets (Eos). Object nets are Petri nets which have Petri nets as tokens – an approach known as the nets-withinnets paradigm. Object nets are called elementary if the net system has a two levelled structure. The well known p/t nets can be considered as a special case of Eos. For p/t nets the concept of safeness means that there is at most one token on each place. Since object nets have nested markings there are different possibilities to generalise this idea for Eos. In this paper we concentrate on the variant of Eos safeness that guarantees the finiteness of state spaces and show that for safe Eos the LTL model checking problem is PSpace-complete.
Dolius: A Distributed Parallel SAT Solving Framework
Authors: Audemard Gilles , Hoessen Benoît , Jabbour Saïd , Piette Cédric
Published: January 2018

Over the years, parallel SAT solving becomes more and more important. However, most of state-of-the-art parallel SAT solvers are portfolio-based ones. They aim at running several times the same solver with different parameters. In this paper, we propose a tool called Dolius, mainly based on the divide and conquer paradigm. In contrast to most current parallel efficient engines, Dolius does not need shared memory, can be distributed, and scales well when a large number of computing units is available. Furthermore, our tool contains an API allowing to plug any SAT solver in a simple way.
Effect algebras with state operator
Authors: Pulmannova Silvia
Published: January 2018

A state operator on effect algebras is introduced as an additive, idempotent and unital mapping from the effect algebra into itself. The definition is inspired by the definition of an internal state on MV-algebras, recently introduced by Flaminio and Montagna. We study state operators on convex effect algebras, and show their relations with conditional expectations on operator algebras.
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 recently

studied 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.
Seminator: A Tool for Semi-Determinization of Omega-Automata
Authors: Blahoudek František , Duret-Lutz Alexandre , Klokočka Mikuláš , Křetínský Mojmír , Strejček Jan
Published: January 2018

We present a tool that transforms nondeterministic ω-automata to semi-deterministic ω-automata. The tool Seminator accepts transition-based generalized Bu ̈chi automata (TGBA) as an input and produces automata with two kinds of semi-determinism. The implemented procedure performs degeneralization and semi-determinization simultaneously and employs several other optimizations. We experimentally evaluate Seminator in the context of LTL to semi-deterministic automata translation.
Reducts and Modal Operators on Residuated Lattices
Authors: Young William
Published: January 2018

We review and collect some results on reducts and modal operators on residuated lattices.
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 undecidable

problems. In this paper we will give recursion-theoretical

characterization of the computational power of this kind of quantum

Turing machines. In detail, for the unsharp case, it is proved that

Σ01

∪Π01⊆

LTd(ε,Σ)(LTw(ε,Σ))⊆Π02

when the truth value lattice is locally finite and the operation ∧

is computable, where

LTd(ε,Σ)(LTw(ε,Σ))denotes the

class of quantum language accepted by these Turing machine in

depth-first model (respectively, width-first model);

for the sharp case, we can obtain similar results for usual orthomodular lattices.