LPAR-20: Papers with Abstracts

Papers
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.
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.
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?
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.
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.
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.
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.
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.
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.
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.