LPAR-20: Papers with Abstracts

Papers
Automated Theorem Proving by Translation to Description Logic Negin Arhami and Geoff Sutcliffe Abstract. Many Automated Theorem Proving (ATP) systems for different logics, and translators for translating different logics from one to another, have been developed and are now available. Some logics are more expressive than others, and it is easier to express problems in those logics. However, their ATP systems are relatively newer, and need more development and testing in order to solve more problems in a reasonable time. To benefit from the available tools to solve more problems in more expressive logics, different ATP systems and translators can be combined. Problems in logics more expressive than CNF can be translated directly to CNF, or indirectly by translation via intermediate logics. Description Logic (DL) sits between CNF and propositional logic. Saffron a CNF to DL translator, has been developed, which fills the gap between CNF and DL. ATP by translation to DL is now an alternative way of solving problems expressed in logics more expressive than DL, by combining necessary translators from those logics to CNF, Saffron, and a DL ATP system.
Playing with Quantified Satisfaction Nikolaj Bjorner and Mikolas Janota Abstract. We develop an algorithm for satisfiability of quantified formulas. The algorithm is based on recent progress in solving Quantified Boolean Formulas, but it generalizes beyond propositional logic to theories, such as linear arithmetic over integers (Presburger arithmetic), linear arithmetic over reals, algebraic data-types and arrays. Compared with previous algorithms for satisfiability of quantified arithmetical formulas our new implementation outperforms previous implementations in Z3 by a significant margin.
On Conflicts and Strategies in QBF Nikolaj Bjorner, Mikolas Janota and William Klieber Abstract. QBF solving techniques can be divided into the DPLL-based and expansion-based. In this paper we look at how these two techniques can be combined while using strategy extraction as a means of interaction between the two. Once propagation derives a conflict for one of the players, we analyse the proof of such and devise a strategy for the opponent. Subsequently, this strategy is used to constrain the losing player. The implemented prototype shows feasibility of the approach. A number of avenues for future research can be envisioned. Can strategies be employed in a different fashion? Can better strategy be constructed? Do the presented techniques generalize beyond QBF?
Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo Guillaume Bury, David Delahaye, Damien Doligez, Pierre Halmagrand and Olivier Hermant Abstract. We introduce an encoding of the set theory of the B method using polymorphic types and deduction modulo, which is used for the automated verification of proof obligations in the framework of the BWare project. Deduction modulo is an extension of predicate calculus with rewriting both on terms and propositions. It is well suited for proof search in theories because it turns many axioms into rewrite rules. We also present the associated automated theorem prover Zenon Modulo, an extension of Zenon to polymorphic types and deduction modulo, along with its backend to the Dedukti universal proof checker, which also relies on types and deduction modulo, and which allows us to verify the proofs produced by Zenon Modulo. Finally, we assess our approach over the proof obligation benchmark provided by the BWare project.
Symbolic WS1S Loris D'Antoni and Margus Veanes Abstract. We extend weak monadic second-order logic of one successor (WS1S) to symbolic alphabets by allowing character predicates to range over decidable first order theories and not just finite alphabets. We call this extension symbolic WS1S (s-WS1S). We then propose two decision procedures for such a logic: 1) we use symbolic automata to extend the classic reduction from WS1S to finite automata to our symbolic logic setting; 2) we show that every s-WS1S formula can be reduced to a WS1S formula that preserves satisfiability, at the price of an exponential blow-up.
Reasoning in the presence of inconsistency through Preferential ALC Graham Deane, Krysia Broda and Alessandra Russo Abstract. This paper presents an inconsistency tolerant semantics for the Description Logic ALC called Preferential ALC (p-ALC). A p-ALC knowledge base is comprised of defeasible and non-defeasible axioms. The defeasible ABox and TBox are labelled with confidence weights that could reflect an axiom's provenance. Entailment is defined through the notion of preferred interpretations which minimise the total weight of the inconsistent axioms. We introduce a modified ALC tableau algorithm in which the open branches give rise to the preferred interpretations, and show that it can compute p-ALC entailment by refutation. The modified algorithm is implemented as an incremental answer set program (ASP) that exploits optimisation to capture preferred interpretations of p-ALC.
A Lightweight Double-negation Translation Frederic Gilbert Abstract. Deciding whether a classical theorem can be proved constructively is a well-known undecidable problem. As a consequence, any computable double-negation translation inserts some unnecessary double negations. This paper shows that most of these unnecessary insertions can be avoided without any use of constructive proof search techniques. For this purpose, we restrict the analysis to syntax-directed double-negation translations, which translate a proposition through a single traversal -- and include most of the usual translations such as Kolmogorov's, Gödel-Gentzen's, and Kuroda's. A partial order among translations are presented to select translations avoiding as many double negations as possible. This order admits a unique minimal syntax-directed translation with noticeable properties.
Application of Trace-Based Subjective Logic to User Preferences Modeling Hoang Nam Ho, Mourad Rabah, Samuel Nowakowski and Pascal Estraillier Abstract. A good way to help users make decisions in an interactive application consists in suggesting choices in accordance with their preferences. This decision problem faces challenging tasks, mainly in choosing a good solution that satisfies users and reaches the defined goal. Classical decision methods take into account the goal, but not all the obtained decisions can satisfy users’ preferences. The originality of our explorative research is to associate Subjective Logic (SL) to system’s traces (historical information) in order to model the user preferences that improve the decision process. Following JØsang, SL provides a suitable framework for modeling and formally describing users’ preferences. We propose to connect data collected in past executions, called traces, to the user intuition in order to support subjective reasoning. Based on this result, we can choose a reasonable decision according to users’ preferences. A Tamagotchi system will be presented to validate our result.
Compiling Hilbert's epsilon operator Rustan Leino Abstract. Hilbert's epsilon operator is a binder that picks an arbitrary element from a nonempty set. The operator is typically used in logics and proof engines. This paper contributes a discussion of considerations in supporting this operator in a programming language. More specifically, the paper presents the design choices made around supporting this operator in the verification-aware language Dafny.
A New Proof of P-time Completeness of Linear Lambda Calculus Satoshi Matsuoka Abstract. We give a new proof of P-time completeness of the Linear Lambda Calculus, which was originally given by H. Mairson in 2003. Our proof uses an essentially different Boolean type from the type that Mairson used. Moreover the correctness of our proof can be machined-checked using an implementation of Standard ML.