bluuebunny/crossref_metadata_2025 huggingface dataset:
LexiPers: An ontology based sentiment lexicon for Persian
Authors: Sabeti Behnam , Hosseini Pedram , Ghassem-Sani Gholamreza , Mirroshandel Sَeyed Abolghasem
Published: January 2018

Sentiment analysis refers to the use of natural language processing to identify and extract subjective information from textual resources. One approach for sentiment extraction is using a sentiment lexicon. A sentiment lexicon is a set of words associated with the sentiment orientation that they express. In this paper, we describe the process of generating a general purpose sentiment lexicon for Persian. A new graph-based method is introduced for seed selection and expansion based on an ontology. Sentiment lexicon generation is then mapped to a document classification problem. We used the K-nearest neighbors and nearest centroid methods for classification. These classifiers have been evaluated based on a set of hand labeled synsets. The final sentiment lexicon has been generated by the best classifier. The results show an acceptable performance in terms of accuracy and F-measure in the generated sentiment lexicon.
A Semidefinite Programming Approach to Control Synthesis for Stochastic Reach-Avoid Problems
Authors: Drzajic Dalibor , Kariotoglou Nikolaos , Kamgarpour Maryam , Lygeros John
Published: January 2018

We propose a computational approach to approximate the value function and control policies for a finite horizon stochastic reach-avoid problem as follows. First, we formulate an infinite dimensional linear program whose solution characterizes the optimal value function of the stochastic reach-avoid. Next, we introduce sum-of-squares polynomials to approximate the solution of this linear program through a semidefinite program. We compare our proposed tool to alternative numerical approaches via several case studies.
Antifounded Coinduction in Type Theory
Authors: Uustalu Tarmo
Published: January 2018

Venanzio Capretta, Varmo Vene and I have previously studied antifounded algebras as a a category-theoretic formulation of antifounded coinduction. These are the dual of wellfounded coalgebras, a category theorist's take on wellfounded induction, closely related to the Bove-Capretta method for justifying function definitions by general recursion in type theory.

In this talk, we discuss one possible type-theoretic approach to antifounded coinduction.
The 2012 SMT Competition
Authors: Cok David , Griggio Alberto , Bruttomesso Roberto , Deters Morgan
Published: January 2018

The 2012 SMT Competition was held in conjunction with the SMT workshop at IJCAR 2012. Eleven solvers participated, showing improvements over 2011 in some but not all divisions. The competition featured a new unsat-core-generation track and encouraged the demonstration of proof-generation solvers. The series of competitions is expected to be continued at SAT 2013.
The Handling of Loops in Talmudic Logic, with Application to Odd and Even Loops in Argumentation
Authors: Abraham Michael , Gabbay Dov , Schild Uri J.
Published: January 2018

In this paper we present the notion of the Talmudic

Shkop extension to an abstract argumentation network (S,R) and compare it with Baroni’s

and his colleagues CF2 extensions and with Gabbay’s Equational approach to CF2 semantics.

We also offer tableaux methods as well as discuss temporal stamping of arguments and their use in resolving loops
Post Mortem Analysis of SAT Solver Proofs
Authors: Simon Laurent
Published: January 2018

Conflict-Driven Clause Learning algorithms are well known from an engineer

point of view. Thanks to Minisat, their designs are well understood, and most

of their implementations follow the same ideas, with essentially the same

components. Same heuristics, fast restarts, same learning mechanism.

However, their efficiency has an important drawback: they are more and more

like complex systems and harder and harder to handle. Unfortunately, only a

few works are focusing on understanding them rather than improving them. In

most of the cases, their studies are often based on a generate and test

pattern: An idea is added to an existing solver and if it improves its

efficiency the idea is published and kept. In this paper, we analyse

``post-mortem'' the proofs given by one typical CDCL solver,

Glucose. The originality of our approach is that we only consider it as a

resolution proofs builder, and then we analyze some of the proof

characteristics on a set of selected unsatisfiable instances, by shuffling each of

them 200 times. We particularly focus on trying to characterize useless and

useful clauses in the proof as well as proofs shapes. We also show that

despite their incredible efficiency, roughly 90% of the time spent in a

CDCL is useless for producing the final proof.
Finite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol
Authors: Lisitsa Alexei
Published: January 2018

We present a case study of the verification of parameterized mutual exclusion protocol using finite model finder Mace4. Thhe verification follows an approach based on modeling of reachability between states of the protocol as deducibility between appropriate encodings of states by first-order predicate logic formulae. The result of successful verification is a finite countermodel, a witness of non-deducibility, which represents a system invariant.
Cayley and Holland Theorems for Residuated Lattices
Authors: Galatos Nikolaos , Horcik Rostislav
Published: January 2018

We obtain representation theorems for residuated lattices. The representing structure consists of special self maps on an ordered set. We prove two types of theorems; one that generalizes Cayley's theorem for groups/monoids and one (for special residuated lattices) that generalizes Holland's theorem for lattice-ordered groups. Our results are presented in the language of idempotent semirings and semimodules, and they are first established for these types of structures.
Graph Symmetry Detection and Canonical Labeling: Differences and Synergies
Authors: Katebi Hadi , Sakallah Karem A. , Markov Igor L.
Published: January 2018

Symmetries of combinatorial objects are known to complicate search algorithms, but such obstacles can often be removed by detecting symmetries early and discarding symmetric subproblems. Canonical labeling of combinatorial objects facilitates easy equivalence checking through quick matching. All existing canonical labeling software also finds symmetries, but the fastest symmetry-finding software does not perform canonical labeling. In this work, we contrast the two problems and dissect typical algorithms to identify their similarities and differences. Based on this analysis, we develop a novel approach to canonical labeling where symmetries are found first and then used to speed up the canonical labeling algorithms. Empirical results show that this approach outperforms state-of-the-art canonical labelers.
Compositional Verification of Security Properties for Embedded Execution Platforms
Authors: Baumann Christoph , Schwarz Oliver , Dam Mads
Published: January 2018

The security of embedded systems can be dramatically improved through the use of formally verified isolation mechanisms such as separation kernels, hypervisors, or microkernels. For trustworthiness, particularly for system level behaviour, the verifications need precise models of the underlying hardware. Such models are hard to attain, highly complex, and proofs of their security properties may not easily apply to similar but different platforms. This may render verification economically infeasible.

To address these issues, we propose a compositional top-down approach to embedded system specification and verification, where the system-on-chip is modeled as a network of distributed automata communicating via paired synchronous message passing. Using abstract specifications for each component allows to delay the development of detailed models for cores, devices, etc., while still being able to verify high level security properties like integrity and confidentiality, and soundly refine the result for different instantiations of the abstract components at a later stage.

As a case study, we apply this methodology to the verification of information flow security for an industry scale security-oriented hypervisor on the ARMv8-A platform. The hypervisor statically assigns (multiple) cores to each guest system and implements a rudimentary, but usable, inter guest communication discipline. We have completed a pen-and-paper security proof for the hypervisor down to state transition level and report on a partially completed verification of guest mode security in the HOL4 theorem prover.
Optimizing the AES S-Box using SAT
Authors: Fuhs Carsten , Schneider-Kamp Peter
Published: January 2018

Non-trivial linear straight-line programs over the Galois field of two elements occur frequently in applications such as encryption or high-performance computing. Finding the shortest linear straight-line program for a given set of linear forms is known to be MaxSNP-complete, i.e., there is no ε-approximation for the problem unless P = NP.

This paper reiterates a non-approximative approach for finding the shortest linear straight-line program. After showing how to search for a circuit of XOR gates with the minimal number of such gates by a reduction of the associated decision problem ("Is there a program of length k?") to satisfiability of propositional logic, we show that using modern SAT solvers, provably optimal solutions to interesting problem instances from cryptography can be obtained. We substantiate this claim by a case study on optimizing the AES S-Box.
Exploring Predictability of SAT/SMT Solvers
Authors: Brummayer Robert , Oe Duckki , Stump Aaron
Published: January 2018

This paper seeks to explore the predictability of SAT and SMT solvers in response to different kinds of changes to benchmarks. We consider both semantics-preserving and possibly semantics-modifying transformations, and provide preliminary data about solver predictability. We also propose carrying learned theory lemmas over from an original run to runs on similar benchmarks, and show the benefits of this idea as a heuristic for improving predictability of SMT solvers.
Asynchronous testing of real-time systems
Authors: Bhateja Puneet
Published: January 2018

Conformance testing is an operational way of determining whether an implementation conforms to the specification or not. It has a rich underlying theory wherein the specification and the implemen- tation under test (IUT) are each modeled by a timed automaton with inputs and outputs (TAIO), a variant of the classical timed automaton [1]. Test cases generated from the specification TAIO are symbolically executed against the implementation TAIO. Depending upon how test cases interact with the IUT, testing can be synchronous or asynchronous. In synchronous testing a test case interacts with the IUT directly, whereas in asynchronous testing a test case interacts with the IUT through a pair of first-in-first-out (FIFO) channels. Different approaches for synchronous testing of real-time systems have already been proposed [5],[7],[4],[8]. In this paper we propose an approach which is aimed at testing real-time systems asynchronously (i.e., remotely through some medium)
GridTPT: a distributed platform for Theorem Prover Testing
Authors: Bouton Thomas , Caminha Diego , Déharbe David , Fontaine Pascal
Published: January 2018

Programming provers is a complex task; completeness or even soundness may often be broken by apparently harmless bugs. A good testing platform can contribute in detecting problems early and helping development. This paper presents GridTPT, the distributed platform for testing the verit SMT solver. Its features are fairly standard, but it allows to easily distribute the task in a cluster.

We plan to make this platform available as an open source tool for the community of developers of automated theorem provers. This presentation to PAAR'2010 will provide the opportunity to discuss the need for such a tool and the necessary features in a broader context. We would like to extract a requirement specification from this discussion, that would be useful to get dedicated implementation resources for distribution, maintenance and future development of GridTPT.
Evaluating Automated Theorem Provers Using Adimen-SUMO
Authors: Álvez Javier , Lucio Paqui , Rigau German
Published: January 2018

We report on the results of evaluating the performance automated theorem provers using \ADIMENSUMO{}. The evaluation follows the adaptation of the methodology based on competency questions \cite{GrF95} to the framework of first-order logic, which is presented in \cite{ALR15}, and is applied to \ADIMENSUMO{} \cite{ALR12}. The set of competency questions used for this evaluation has been semi-automatically generated from a small set of semantic patterns and the mapping of \WORDNET{} to \SUMO{}, also introduced in \cite{ALR15}. Our experimental results demonstrate that improved versions of the proposed set of competency questions could be really valuable for the development of automated theorem provers.
A Sufficient Condition for the Observational Equivalence of Processes
Authors: Mironov Andrew
Published: January 2018

The article deals with the problem of proving observational equivalence for the class of computational processes called processes with message passing. These processes can execute actions of the following forms: sending or receiving of messages, checking logical conditions and updating values of internal variables of processes. Our main result is a theorem that reduces the problem of proving observational equivalence of a pair of processes with message passing to the problem of finding formulas associated with pairs of states of these processes, satisfying certain conditions that are associated with transitions of these processes. This reduction is a generalization of Floyd's method of flowchart verification, which reduces the problem of verification of flowcharts to the problem of finding formulas (called intermediate assertions) associated with points in the flowcharts and satisfying conditions, corresponding to transitions in the flowcharts. The above method of proving observational equivalence of processes with message passing is illustrated by a sliding window protocol verification
24 Challenges in Deductive Software Verification
Authors: Hähnle Reiner , Huisman Marieke
Published: January 2018

Deductive software verification aims at formally verifying that all possible behaviors of a given program satisfy formally defined, complex properties, where the verification process is based on logical inference. We list the most important challenges for the further development of the field.
Lingeling Essentials, A Tutorial on Design and Implementation Aspects of the the SAT Solver Lingeling
Authors: Biere Armin
Published: January 2018

One of the design principles of the state-of-the-art SAT solver Lingeling is to use as compact data structures as possible. These reduce memory usage, increase cache efficiency and thus improve run-time, particularly, when using multiple solver instances on multi-core machines, as in our parallel portfolio solver Plingeling and our cube and conquer solver Treengeling. The scheduler of a dozen inprocessing algorithms is an important aspect of Lingeling as well. In this talk we explain these design and implementation aspects of Lingeling and discuss new direction of solver design.
Conflicts, Models and Heuristics for Quantifier Instantiation in SMT
Authors: Reynolds Andrew
Published: January 2018

Satisfiability Modulo Theories (SMT) solvers have emerged as prominent tools in formal methods applications. While originally targeted towards quantifier-free inputs, SMT solvers are now often used for handling quantified formulas in automated theorem proving and software verification applications. The most common technique for handling quantified formulas in modern SMT solvers in quantifier instantiation. This paper gives an overview of recent advances in quantifier instantiation in SMT. In addition to the well-known technique known as E-matching, we discuss the use of conflicts and models for accelerating the search for (un)satisfiably. We further mention new instantiation-based techniques that are specialized to background theories such as linear real and integer arithmetic, and future work in this direction.
Space Analysis of a Predicate Logic Fragment for the Specification of Stream Monitors
Authors: Cerna David , Schreiner Wolfgang , Kutsia Temur
Published: January 2018

We analyze the space complexity of monitoring streams of messages whose expected behavior is specified in a fragment of predicate logic; this fragment is the core of the LogicGuard specification language that has been developed in industrial context for the runtime monitoring of network traffic. The execution of the monitors is defined by an operational semantics for the step-wise evaluation of formulas, of which require the preservation of instances of the formulas in memory until their truth value can be determined. In the presented work, we analyze the number of instances that have to be preserved over time for a significant fragment of the core language that involves only “future looking quantifiers” which lays the foundations for the space analysis of the entire core language.
Theorem Provers For Every Normal Modal Logic
Authors: Gleißner Tobias , Steen Alexander , Benzmüller Christoph
Published: January 2018

We present a procedure for algorithmically embedding problems formulated in higher- order modal logic into classical higher-order logic. The procedure was implemented as a stand-alone tool and can be used as a preprocessor for turning TPTP THF-compliant the- orem provers into provers for various modal logics. The choice of the concrete modal logic is thereby specified within the problem as a meta-logical statement. This specification for- mat as well as the underlying semantics parameters are discussed, and the implementation and the operation of the tool are outlined.

By combining our tool with one or more THF-compliant theorem provers we accomplish the most widely applicable modal logic theorem prover available to date, i.e. no other available prover covers more variants of propositional and quantified modal logics. Despite this generality, our approach remains competitive, at least for quantified modal logics, as our experiments demonstrate.
A Method to Simplify Expressions: Intuition and Preliminary Experimental Results
Authors: Le Charlier Baudouin , Atindehou Mêton Mêton
Published: January 2018

We present a method to simplify expressions in the context of a formal, axiomatically defined, theory. In this paper, equality axioms are typically used but the method is more generally applicable. The key idea of the method is to represent large, even infinite, sets of expressions\footnote{We use the words ``term'' and ``expression'' as synonymous.} by means of a special data structure that allows us to apply axioms to the sets as a whole, not to single individual expressions. We then propose a bottom-up algorithm to finitely compute theories with a finite number of equivalence classes of equal terms. In that case, expressions can be simplified (i.e., minimized) in linear time by ``folding'' them on the computed representation of the theory. We demonstrate the method for boolean expressions with a small number of variables. Finally, we propose a ``goal oriented'' algorithm that computes only small parts of the underlying theory, in order to simplify a given particular expression. We show that the algorithm is able to simplify boolean expressions with many more variables but optimality cannot be certified anymore.
formalSpec - Semi-Automatic Formalization of System Requirements for Formal Verification
Authors: Busboom Axel , Schuler Simone , Walsch Alexander
Published: January 2018

We present the proof-of-concept tool formalSpec for semi-automatic translation of system requirements from controlled natural language into hybrid automata. These can be automatically integrated as monitor automata with an existing SpaceEx system model.
AVATAR Modulo Theories
Authors: Reger Giles , Bjorner Nikolaj , Suda Martin , Voronkov Andrei
Published: January 2018

This paper introduces a new technique for reasoning with quantifiers and theories. Traditionally, first-order theorem provers (ATPs) are well suited to reasoning with first-order problems containing many quantifiers and satisfiability modulo theories (SMT) solvers are well suited to reasoning with first-order problems in ground theories such as arithmetic. A recent development in first-order theorem proving has been the AVATAR architecture which uses a SAT solver to guide proof search based on a propositional abstraction of the first-order clause space. The approach turns a single proof search into a sequence of proof searches on (much) smaller sub-problems. This work extends the AVATAR approach to use a SMT solver in place of the SAT solver, with the effect that the first-order solver only needs to consider ground-theory-consistent sub-problems. The new architecture has been implemented using the Vampire theorem prover and Z3 SMT solver. Our experimental results, and the results of recent competitions, show that such a combination can be highly effective.
Optimizing Safe Control of a Networked Platoon of Trucks Using Reachability
Authors: Ben Makhlouf Ibtissem , Kowalewski Stefan
Published: January 2018

The problem of conceiving a controller for networked systems is a challenging task

because of the complex interaction of its different components with each other and also with the environment around them. The design process becomes more difficult if large-scaled systems are involved. We propose reachability analysis of continuous systems to guarantee control requirements which because of the complexity of the problem could not be taken into account during the control design. As example we suggest a large-scalable platoon of trucks. We use our own support function implementation to assess the performances of the obtained controlled

platoon and then decide about the best performing controller.
Capacity Visual Attention Networks
Authors: Edel Marcus , Lausch Joscha
Published: January 2018

Inspired by recent work in machine translation and object detection, we introduce an attention-based model that automatically learns to extract information from an image by adaptively assigning its capacity across different portions of the input data and only processing the selected regions of different sizes at high resolution. This is achieved by combining two modules: an attention sub-network which uses a mechanism to model a human-like counting process and a capacity sub-network. This sub-network efficiently identifies input regions for which the attention model output is most sensitive and to which we should devote more capacity and dynamically adapt the size of the region. We focus our evaluation on the Cluttered MNIST, SVHN, and Cluttered GTSRB image datasets. Our findings indicate that the proposed model is able to drastically reduce the number of computations, compared with traditional convolutional neural networks, while maintaining similar or better performance.
Machine Learning of Coq Proof Guidance: First Experiments
Authors: Kaliszyk Cezary , Mamane Lionel , Urban Josef
Published: January 2018

We report the results of the first experiments with learning proof dependencies from the formalizations done with the Coq system. We explain the process of obtaining the dependencies from the Coq proofs, the characterization of formulas that is used for the learning, and the evaluation method. Various machine learning methods are compared on a dataset of 5021 toplevel Coq proofs coming from the CoRN repository. The best resulting method covers on average 75% of the needed proof dependencies among the first 100 predictions, which is a comparable performance of such initial experiments on other large-theory corpora.
Proceedings of the 6th IJCAR ATP System Competition (CASC-J6)
Authors: Sutcliffe Geoff
Published: January 2018

The CADE ATP System Competition (CASC) evaluates the performance of sound, fully automatic, classical logic, ATP systems. The evaluation is in terms of the number of problems solved, the number of acceptable proofs and models produced, and the average runtime for problems solved, in the context of a bounded number of eligible problems chosen from the TPTP problem library, and specified time limits on solution attempts. The 6th IJCAR ATP System Competition (CASC-J6) was held on 24th and 28th June 2012. The design of the competition and its rules, and information regarding the competing systems, are provided in this report.
Running SpaceEx on the ARCH14 Benchmarks
Authors: Minopoli Stefano , Frehse Goran
Published: January 2018

In this paper, we present experimental results from running

SpaceEx on some of the benchmarks of the ARCH14 workshop. Some of

the SpaceEx models were obtained from Matlab/Simulink models with

the help of a new translation tool. While some benchmarks could be

handled to our satisfaction, several still pose signicant challenges. We

discuss possible alternatives for handling the problematic cases.
ProbReach: A Tool for Guaranteed Reachability Analysis of Stochastic Hybrid Systems
Authors: Shmarov Fedor , Zuliani Paolo
Published: January 2018

In this paper we present a summary of our work on probability reachability in stochastic hybrid systems (SHS). In particular, we give an overview of ProbReach, a tool for computing probabilistic reachability in SHS which we introduced in our HSCC 2015 paper. We also present and an overview of our recent theoretical extensions and modification of the tool.
Problem Libraries for Non-Classical Logics
Authors: Otten Jens , Raths Thomas
Published: January 2018

Problem libraries for automated theorem proving (ATP) systems play a crucial role when developing, testing, benchmarking and evaluating ATP systems for classical and non-classical logics. We provide an overview of existing problem libraries for some important non-classical logics, namely first-order intuitionistic and first-order modal logics. We suggest future plans to extend these existing libraries and discuss ideas for a general problem library platform for non-classical logics.
Truncated Vector Lattices
Authors: Ball Richard
Published: January 2018

In analysis, truncation is the operation of replacing a nonnegative real-valued function a (x) by its pointwise meet a (x) ∧ 1 with the constant $1$ function. A vector lattice A is said to be closed under truncation if a ∧ 1 ∈ A for all a ∈ A+. Note that A need not

contain 1 itself.

Truncation is fundamental to analysis. To give only one example, Lebesgue integration generalizes beautifully to any vector lattice of real-valued functions on a set X, provided the vector lattice is closed under truncation. But vector lattices lacking this property may have integrals which cannot be represented by any measure on X. Nevertheless, when the integral is formulated in a context broader than RX, for example in pointfree analysis, the question of

truncation inevitably arises.

What is truncation, or more properly, what are its essential properties? In this paper we answer this question by providing the appropriate axiomatization, and then go on to present several representation theorems. The first is a

direct generalization of the classical Yosida representation of an archimedean vector lattice with order unit. The second is a direct generalization of Madden's pointfree representation of archimedean vector lattices. If time permits, we briefly discuss a third sheaf representation which has no direct antecedent in the literature.

However, in all three representations the lack of a unit forces a crucial distinction from the corresponding unital representation theorem. The universal object in each case is some sort of family of continuous real-valued functions. The difference is that these functions must vanish at a specified point of the underlying space or locale or sheaf space. With that adjustment, the generalization from units to truncations goes remarkably smoothly.
Detecting Modular ACU Structural Symmetries
Authors: Alpuente María , Escobar Santiago , Espert Javier
Published: January 2018

We present an efficient encoding of order-sorted modular ACU terms into colored directed graphs. Then, by computing the automorphism groups of the encoded graphs, we are able to extract ACU structural symmetries both inside a term and across a set of terms. Finally, we show how the computed symmetries can be applied to the optimization of the equational generalization algorithms for modular ACU theories.
A Genetic Algorithm for Truck Dispatching in Mining
Authors: Cox Wesley , French Tim , Reynolds Mark , While Lyndon
Published: January 2018

We apply genetic algorithms (GAs) to evolve cyclic finite automata for scheduling the dispatch of trucks in mines. The GA performs well generally, and on problems which include one-lane roads, the GA was able to find solutions that utilised shovels very well, with low contention and using fewer trucks than both the widely-used linear programming DISPATCH algorithm, and commonly-used greedy heuristics. The GA provides significant cost-savings, or production increases, on problems where alternative algorithms do not adapt well.
Termination Checking in the Presence of Nested Inductive and Coinductive Types
Authors: Altenkirch Thorsten , Danielsson Nils Anders
Published: January 2018

In the dependently typed functional programming language Agda one can easily mix induction and coinduction. The implementation of the termination/productivity checker is based on a simple extension of a termination checker for a language with inductive types. However, this simplicity comes at a price: only types of the form νX.μY.F X Y can be handled directly, not types of the form μY.νX.F X Y. We explain the implementation of the termination checker and the ensuing problem.
Making Automatic Theorem Provers more Versatile
Authors: Cruanes Simon
Published: January 2018

We argue that automatic theorem provers should become more versatile and should be able to tackle problems expressed in richer input formats. Salient research directions include (i) developing tight combinations of SMT solvers and first-order provers; (ii) adding better handling of theories in first-order provers; (iii) adding support for inductive proving; (iv) adding support for user-defined theories and functions; and (v) bringing to the provers some basic abilities to deal with logics beyond first-order, such as higher-order logic.
We know (nearly) nothing!l But can we learn?
Authors: Schulz Stephan
Published: January 2018

The greatest source of progress in automated theorem proving in the last 30 years has been the development of better search heuristics, usually based on developer experience and empirical evaluation, but increasingly also using automated optimization techniques. Despite this progress, we still know very little about proof search. We have mostly failed to identify good features for characterizing homogeneous problem classes, or for identifying interesting and relevant clauses and formulas.

I propose the challenge of bringing together inductive techniques (generalization and learning) and deductive techniques to attack this problem. Hardware and software have finally evolved to a point that we can reasonably represent and analyze large proof searches and search decisions, and where we can hope to achieve order-of-magnitude improvements in the efficiency of the proof search.
Learning from Multiple Proofs: First Experiments
Authors: Kuehlwein Daniel , Urban Josef
Published: January 2018

Mathematical textbooks typically present only one proof for most of the theorems. However, there are infinitely many proofs for each theorem in first-order logic, and mathematicians are often aware of (and even invent new) important alternative proofs and use such knowledge for (lateral) thinking about new problems.

In this paper we start exploring how the explicit knowledge of multiple (human and ATP) proofs of the same theorem can be used in learning-based premise selection algorithms in large-theory mathematics.

Several methods and their combinations are defined, and their effect on the ATP performance is evaluated on the MPTP2078 large-theory benchmark.

Our first findings are that the proofs used for learning significantly influence the number of problems solved, and that the quality of the proofs is more important than the quantity.
Proving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing
Authors: Wasserrab Daniel , Lohner Denis
Published: January 2018

We present a machine-checked correctness proof for information flow noninterference based on interprocedural slicing. It reuses a correctness proof of the context-sensitive interprocedural slicing algorithm of Horwitz, Reps, and Binkley. The underlying slicing framework is modular in the programming language used; by instantiating this framework the correctness proofs hold for the respective language, without reproving anything in the correctness proofs for slicing and noninterference. We present instantiations with two different languages to show the applicability of the framework, and thus a verified noninterference algorithm for these languages. The formalization and proofs are conducted in the proof assistant Isabelle/HOL.
Secrecy-Preserving Reasoning and Query Answering in Probabilistic Description Logic Knowledge Bases
Authors: Krishnasamy Sivaprakasam Gopalakrishnan , Raglin Adrienne , Summers-Stay Douglas , Slutzki Giora
Published: January 2018

In this paper we study Secrecy-Preserving Query Answering problem under

the OpenWorld Assumption (OWA) for Prob-EL>0;=1 Knowledge Bases

(KBs). We have designed a tableau procedure to compute a semi model M

over the given KB which eventually is equivalent to a probabilistic model

to KB. Given a secrecy set S, which is a finite set of assertions, we

compute a function E, called an envelope of S, which assigns a set E() of

assertions to each world in the semi modal M. E provides logical protection to the secrecy set S against the reasoning of a querying agent. Once the semi model M and an envelope E are computed, we define the secrecy-preserving semi model ME.

Based on the information available in ME, assertional queries with probabilistic

operators can be answered eciently while preserving secrecy. To

the best of our knowledge, this work is first one studying secrecy-preserving

reasoning in description logic augmented with probabilistic operators. When

the querying agent asks a query q, the reasoner answers “Yes” if information

about q is available in ME; otherwise, the reasoner answers “Unknown”. Being

able to answer “Unknown” plays a key role in protecting secrecy under

OWA. Since we are not computing all the consequences of the knowledge

base, answers to the queries based on just secrecy-preserving semi model

ME could be erroneous. To fix this problem, we further augment our algorithms

by providing recursive query decomposition algorithm to make the

query answering procedure foolproof.

1
Automated Invariant Generation for the Verification of Real-Time Systems
Authors: Badban Bahareh , Leue Stefan , Smaus Jan-Georg
Published: January 2018

We present an approach to automatically generating invariants for timed automata models. The CIPM algorithm that we propose first computes new invariants for timed automata control locations taking their originally defined invariants as well as the constrains on clock variables imposed by incoming state transitions into account. In doing so the CIPM algorithm also prunes idle transitions, which are transitions that can never be taken, from the automaton. We discsuss a prototype implementation of the CIPM algorithm as well as some initial experimental results.
A Unified View of Induction Reasoning for First-Order Logic
Authors: Stratulat Sorin
Published: January 2018

Induction is a powerful proof technique adapted to reason on sets

with an unbounded number of elements. In a first-order setting, two

different methods are distinguished: the conventional induction,

based on explicit induction schemas, and the implicit induction,

based on reductive procedures. We propose a new cycle-based

induction method that keeps their best features, i.e. i) performs

lazy induction, ii) naturally fits for mutual induction, and iii) is

free of reductive constraints. The heart of the method is a proof

strategy that identifies in the proof script the subset of formulas

contributing to validate the application of induction hypotheses.

The conventional and implicit induction are particular cases of our

method.
TacticToe: Learning to Reason with HOL4 Tactics
Authors: Gauthier Thibault , Kaliszyk Cezary , Urban Josef
Published: January 2018

Techniques combining machine learning with translation to automated reasoning have recently become an important component of formal proof assistants. Such “hammer” techniques complement traditional proof assistant automation as implemented by tactics and decision procedures. In this paper we present a unified proof assistant automation approach which attempts to automate the selection of appropriate tactics and tactic-sequences combined with an optimized small-scale hammering approach. We implement the technique as a tactic-level automation for HOL4: TacticToe. It implements a modified A*-algorithm directly in HOL4 that explores different tactic-level proof paths, guiding their selection by learning from a large number of previous tactic-level proofs. Unlike the existing hammer methods, TacticToe avoids translation to FOL, working directly on the HOL level. By combining tactic prediction and premise selection, TacticToe is able to re-prove 39% of 7902 HOL4 theorems in 5 seconds whereas the best single HOL(y)Hammer strategy solves 32% in the same amount of time.
User-friendly Support for Common Mathematical Concepts in a Lightweight Verifier
Authors: Lapets Andrei
Published: January 2018

Machine verification of formal arguments can only increase our confidence in the correctness of those arguments, but the costs of employing machine verification still outweigh the benefits for some common kinds of formal reasoning activities. As a result, usability is becoming increasingly important in the design of formal verification tools. We describe the ``aartifact" lightweight verification system, designed for processing formal arguments involving basic, ubiquitous mathematical concepts. The system is a prototype for investigating potential techniques for improving the usability of formal verification systems. It leverages techniques drawn both from existing work and from our own efforts. In addition to a parser for a familiar concrete syntax and a mechanism for automated syntax lookup, the system integrates (1) a basic logical inference algorithm, (2) a database of propositions governing common mathematical concepts, and (3) a data structure that computes congruence closures of relations found in this database. Together, these components allow the system to better accommodate the expectations of users interested in verifying typical formal arguments involving algebraic manipulations of numbers, sets, vectors, and related operators and predicates. We demonstrate the reasonable performance of this system on typical formal arguments and briefly discuss how the system's design contributes to its usability in two use cases.
Dcpo models of T1 spaces
Authors: Dongsheng Zhao , Xiaoyong Xi
Published: January 2018

A poset model of a topological space X is a poset P such that the subspace Max(P) of the Scott space ΣP consisting of all maximal points of P is homeomorphic to X. Every T1 space has a (bounded complete algebraic) poset model. It is, however, not known whether every T1 space has a dcpo model and whether every sober T1 space has a dcpo model whose Scott topology is sober. In this paper we give a positive answer to these two problems. For each T1 space X we shall construct a dcpo A that is a model of X, and prove that X is sober if and only if the Scott topology of A is sober. One useful by-product is a method that can be used to construct more non-sober dcpos.
Foundations for the Logical Difference of EL-TBoxes
Authors: Feng Shasha , Ludwig Michel , Walther Dirk
Published: January 2018

We investigate the logical difference problem between general EL-TBoxes. The logical difference is the set of concept subsumptions that are logically entailed by a first TBox but not by a second one.

We show how the logical difference between two EL-TBoxes can be reduced to fixpoint reasoning wrt. EL-TBoxes. Entailments of the first TBox can be represented by subsumptions of least fixpoint concepts by greatest fixpoint concepts, which can then be checked wrt. the second TBox.

We present the foundations for a dedicated procedure based on a hypergraph representation

of the fixpoint concepts without the use of automata-theoretic techniques,

avoiding possible complexity issues of a reduction to modal mu-calculus reasoning.

The subsumption checks are based on checking for the existence of simulations between

the hypergraph representations of the fixpoint concepts and the TBoxes.
A Semantic Framework for Program Debugging
Authors: Li Wei
Published: January 2018

This work aims to build a semantic framework for automated debugging. A debugging process consists of tracing, locating, and fixing processes consecutively. The first two processes are accomplished by a tracing procedure and a locating procedure, respectively. The tracing procedure reproduces the execution of a failed test case with well-designed data structures and saves necessary information for locating bugs. The locating procedure will use the information obtained from the tracing procedure to locate ill-designed statements and to generate a fix-equation, the solution of which is a function that will be used to fix the bugs. A structural operational semantics is given to define the functions of the tracing and locating procedure. Both procedures are proved to terminate and produces one fix-equation. The main task of fixing process is to solve the fix-equation. It turns out that for a given failed test case, there exist three different types of solutions: 1. the bug is solvable, there exists a solution of the fix-equation, and the program can be repaired. 2. There exists a non-linear error in the program, the fix-equation generated at each round of the locating procedure is solvable, but a new bug will arise when the old bug is being fixed. 3. There exists a logical design error and the fix-equation is not solvable.
Automatic Generation of HCCA Resistant Scalar Multiplication Algorithm by Proper Sequencing of Field Multiplier Operands
Authors: Das Poulami , Basu Roy Debapriya , Mukhopadhyay Debdeep
Published: January 2018

Horizontal collision correlation analysis (HCCA) imposes a serious threat to

simple power analysis resistant elliptic curve cryptosystems involving unified algorithms, for e.g. Edward curve unified formula. This attack can be mounted even in presence of differential power analysis resistant randomization schemes. In this paper we have designed an effective countermeasure for HCCA protection, where the dependency of side-channel leakage from a school-book multiplication with the underling multiplier operands is investigated. We have shown how changing the sequence in which the operands are passed to the multiplication algorithm introduces dissimilarity in the information leakage. This disparity has been utilized in constructing a zero-cost countermeasure against HCCA. This countermeasure has been shown to help in HCCA resistivity. Additionally we provide experimental validation for our proposed countermeasure technique on a SASEBO platform. To the best of our knowledge, this is the first time that asymmetry in information leakage has been utilized in designing a side channel countermeasure and successfully applied in an ECC-based crypto-module.
Optimal haplotype reconstruction in half-sib families
Authors: Favier Aurélie , Elsen Jean-Michel , de Givry Simon , Legarra Andrés
Published: January 2018

In the goal of genetic improvement of livestock by marker assisted selection, we aim at reconstructing the haplotypes of sires from their offspring. We reformulate this problem into a weighted binary constraint satisfaction problem with only equality and disequality soft constraints. Our results show these problems have a small treewidth and can be solved optimally, improving haplotype reconstruction compared to previous approaches especially for small families (<10 descendants).
Escape to Mizar from ATPs
Authors: Alama Jesse
Published: January 2018

We announce a tool for mapping derivations produced by the E theorem

prover to Mizar proofs. Our mapping complements earlier work that

generates problems for automated theorem provers from Mizar inference

checking problems. We describe the tool, explain the mapping, and

show how we solved some of the difficulties that arise in mapping

proofs between different logical formalisms, even when they are based

on the same notion of logical consequence, as Mizar and E are (namely,

first-order classical logic with identity).
An elementary proof of the completeness of the Lukasiewicz axioms
Authors: Botur Michal , Paseka Jan
Published: January 2018

The main aim of this talk is twofold. Firstly, to present an elementary

method based on Farkas' lemma for rationals how to embed any finite partial subalgebra

of a linearly ordered MV-algebra into Q \ [0; 1] and then to establish a new elementary

proof of the completeness of the Lukasiewicz axioms for which the MV-algebras community

has been looking for a long time. Secondly, to present a direct proof of Di Nola's

representation Theorem for MV-algebras and to extend his results to the restriction of

the standard MV-algebra on rational numbers.
MCMT in the Land of Parametrized Timed Automata
Authors: Carioni Alessandro , Ghilardi Silvio , Ranise Silvio
Published: January 2018

Timed networks are parametrized systems of timed au\-to\-ma\-ta. Solving reachability problems (e.g., whether a set of unsafe states can ever be reached from the set of initial states) for this class of systems allows one to prove safety properties regardless of the number of processes in the network. The difficulty in solving this kind of verification problems is two-fold. First, each process has (at least one) clock variable ranging over an infinite set, such as the reals or the integers. Second, every system is parameterized with respect to the number of processes and to the topology of the network. Reachability problem for some restricted classes of parameterized timed networks is decidable under suitable assumptions by a backward reachability procedure. Despite these theoretical results, there are few systems capable of automatically solving such problems. Instead, the number $n$ of processes in the network is fixed and a tool for timed automata (like Uppaal) is used to check the desired property for the given $n$.

In this paper, we explain how to attack fully parameteric and timed reachability problems by translation to the declarative input language of \textsc{mcmt}, a model checker for infinite state systems based on Satisfiability Modulo Theories techniques. We show the success of our approach on a number of standard algorithms, such as the Fischer protocol. Preliminary experiments show that fully parametric problems can be more easily solved by \textsc{mcmt} than their instances for a fixed (and large) number of processes by other systems.