bluuebunny/crossref_metadata_2025_split huggingface dataset:
Beagle as a HOL4 external ATP method
Authors: Gauthier Thibault , Kaliszyk Cezary , Keller Chantal , Norrish Michael 
Published: January 2018

This paper presents BEAGLE TAC, a HOL4 tactic for using Beagle as an external ATP fordischarging HOL4 goals. We implement a translation of the higher-order goals to the TFAformat of TPTP and add trace output to Beagle to reconstruct the intermediate steps derivedby the ATP in HOL4. Our translation combines the characteristics of existing successfultranslations from HOL to FOL and SMT-LIB, however we needed to adapt certain stagesof the translation in order to benefit form the expressivity of the TFA format and the powerof Beagle. In our initial experiments, we demonstrate that our system can prove, withoutany arithmetic lemmas, 81% of the goals solved by Metis.
Tool Presentation: Isabelle/HOL for Reachability Analysis of Continuous Systems
Authors: Immler Fabian 
Published: January 2018

We present a tool for reachability analysis of continuous systems based onaffine arithmetic and Runge-Kutta methods. The distinctive feature of our toolis its verification in the interactive theorem prover Isabelle/HOL: thealgorithm is guaranteed to compute safe overapproximations, taking into accountall round-off and discretization errors.
Computer algebra investigation of known primitive triangle-free strongly regular graphs
Authors: Ziv-Av Matan , Klin Mikhail 
Published: January 2018

With the aid of computer algebra systems COCO and GAP withits packages we are investigating all seven known primitivetriangle-free strongly regular graphs on 5, 10, 16, 50, 56,77 and 100 vertices. These graphs are rank 3 graphs, havinga rich automorphism group. The embeddings of each graphfrom this family to other ones are described, theautomorphic equitable partitions are classified, allequitable partitions in the graphs on up to 50 vertices areenumerated. Basing on the reported computer aided resultsand using techniques of coherent configurations, a few newmodels of these graphs are suggested, which are relying onknowledge of just a small part of symmetries of a graph inconsideration.
An analogue of Bull's theorem for Hybrid Logic
Authors: Robinson Claudette , Conradie Willem 
Published: January 2018

Hybrid logic extends modal logic with a special sort of variables, called nominals, which are evaluated to singletons in Kripke models by valuations, thus acting as names for states in models. Various syntactic mechanisms for exploiting and enhancing the expressive power gained through the addition of nominals can be included, most characteristically the satisfaction operator, @_ip, allowing one to express that p holds at the world named by a nominal i.R.A. Bull famously proved that each normal extension of S4.3 has the finite modelproperty. In the current paper, we prove a hybrid analogue of Bull's result. Like the proof of Bull's original result, ours is algebraic, and thus our secondary aim with this work is to illustrate the usefulness of algebraic methods within hybrid logic research, a field where such methods have been largely ignored.
Formal Replay of Translation Validation for Highly Optimised C
Authors: Sewell Thomas 
Published: January 2018

In previous work [Sewell, Myreen and Klein, 2013] we have implemented atranslation validation mechanism for checking that a C compiler is adheringto the expected semantics of a verified program. We used this apparatus tocheck the compilation of the seL4 verified operating systemkernel [Klein et.al. 2009] by GCC 4.5.1. To get this result, wecarefully chose a problem representation that worked well with certain highlyoptimised SMT solvers. This raises a question of correctness. While we areconfident the result is correct, we still aim to replay this result with themost dependable tools available.In this work we present a formalisation of the proof rules needed to replaythe translation check within the theorem prover Isabelle/HOL. This is part ofan ongoing effort to bring the entire translation validation result within asingle trusted proof engine and derive a single correctness theorem, thusreaching the gold standard level of trustworthiness for program verification.We had hoped to present the formal rule set in action through a worked example.Unfortunately while we have all the theory we need, the mechanisms forselecting and applying the rules and discharging certain side conditions remaina work in progress, and our example proof is incomplete.
Boolean like algebras
Authors: Ledda Antonio , Kowalski Tomasz , Paoli Francesco , Salibra Antonino 
Published: January 2018

Using Vaggione's concept of central element in a double pointed algebra, weintroduce the notion of Boolean like variety as a generalisation ofBoolean algebras to an arbitrary similarity type. Appropriately relaxing therequirement that every element be central in any member of the variety, weobtain the more general class of semi-Boolean like varieties, whichstill retain many of the pleasing properties of Boolean algebras. We provethat a double pointed variety is discriminator iff it is semi-Boolean like,idempotent, and 0-regular. This theorem yields a new Maltsev-stylecharacterisation of double pointed discriminator varieties.Moreover, we point out the exact relationship between semi-Boolean-likevarieties and the quasi-discriminator varieties, and we providesemi-Boolean-like algebras with an explicit weak Boolean productrepresentation with directly indecomposable factors. Finally, we discuss idempotentsemi-Boolean-like algebras. We consider a noncommutative generalisation of Boolean algebras and prove - along the lines of similar results available for pointed discriminator varieties or for varieties with a commutative ternary deduction term that every idempotent semi-Boolean-like variety is term equivalent to a variety of noncommutative Boolean algebras with additional operations.
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 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 TalmudicShkop extension to an abstract argumentation network (S,R) and compare it with Baroni’sand 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 engineerpoint of view. Thanks to Minisat, their designs are well understood, and mostof their implementations follow the same ideas, with essentially the samecomponents. Same heuristics, fast restarts, same learning mechanism.However, their efficiency has an important drawback: they are more and morelike complex systems and harder and harder to handle. Unfortunately, only afew works are focusing on understanding them rather than improving them. Inmost of the cases, their studies are often based on a generate and testpattern: An idea is added to an existing solver and if it improves itsefficiency 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 aresolution proofs builder, and then we analyze some of the proofcharacteristics on a set of selected unsatisfiable instances, by shuffling each ofthem 200 times. We particularly focus on trying to characterize useless anduseful clauses in the proof as well as proofs shapes. We also show thatdespite their incredible efficiency, roughly 90% of the time spent in aCDCL is useless for producing the final proof.
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 &lt;math&gt;P = NP&lt;/math&gt;.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 &lt;math&gt;k&lt;/math&gt;?") 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.
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.
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.
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 taskbecause 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 controlledplatoon and then decide about the best performing controller.
Running SpaceEx on the ARCH14 Benchmarks
Authors: Minopoli Stefano , Frehse Goran 
Published: January 2018

In this paper, we present experimental results from runningSpaceEx on some of the benchmarks of the ARCH14 workshop. Some ofthe SpaceEx models were obtained from Matlab/Simulink models withthe help of a new translation tool. While some benchmarks could behandled to our satisfaction, several still pose signicant challenges. Wediscuss possible alternatives for handling the problematic cases.
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 notcontain 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 oftruncation 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 adirect 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.
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.
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.
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 underthe OpenWorld Assumption (OWA) for Prob-EL&gt;0;=1 Knowledge Bases(KBs). We have designed a tableau procedure to compute a semi model Mover the given KB which eventually is equivalent to a probabilistic modelto KB. Given a secrecy set S, which is a finite set of assertions, wecompute a function E, called an envelope of S, which assigns a set E() ofassertions 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 probabilisticoperators can be answered eciently while preserving secrecy. Tothe best of our knowledge, this work is first one studying secrecy-preservingreasoning in description logic augmented with probabilistic operators. Whenthe querying agent asks a query q, the reasoner answers “Yes” if informationabout q is available in ME; otherwise, the reasoner answers “Unknown”. Beingable to answer “Unknown” plays a key role in protecting secrecy underOWA. Since we are not computing all the consequences of the knowledgebase, answers to the queries based on just secrecy-preserving semi modelME could be erroneous. To fix this problem, we further augment our algorithmsby providing recursive query decomposition algorithm to make thequery answering procedure foolproof.1
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 setswith an unbounded number of elements. In a first-order setting, twodifferent methods are distinguished: the conventional induction,based on explicit induction schemas, and the implicit induction,based on reductive procedures. We propose a new cycle-basedinduction method that keeps their best features, i.e. i) performslazy induction, ii) naturally fits for mutual induction, and iii) isfree of reductive constraints. The heart of the method is a proofstrategy that identifies in the proof script the subset of formulascontributing to validate the application of induction hypotheses.The conventional and implicit induction are particular cases of ourmethod.
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 representationof 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 betweenthe hypergraph representations of the fixpoint concepts and the TBoxes.
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 tosimple 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.