ABSTRACT. New proof assistant developments often involve concepts similar to already
formalized ones. When proving their properties, a human can often take inspiration
from the existing formalized proofs available in other provers or libraries.
In this paper we propose and evaluate a number of methods, which strengthen proof
automation by learning from proof libraries of different provers. Certain conjectures
can be proved directly from the dependencies induced by similar proofs
in the other library. Even if exact correspondences are not found, learning-reasoning
systems can make use of the association between proved theorems and their
characteristics to predict the relevant premises. Such external help can be further
combined with internal advice. We evaluate the proposed knowledge-sharing methods by
reproving the HOL Light and HOL4 standard libraries. The learning-reasoning system
HOL(y)Hammer, whose single best strategy could automatically find proofs for 30\% of
the HOL Light problems, can prove 40\% with the knowledge from HOL4.
ABSTRACT. When constructing complex program analyses, it is often useful to reason about not just individual values, but collections of values. Symbolic set abstractions provide such a building block that can be used to construct partitions of elements, relate partitions to other partitions, and determine the provenance of multiple values, all without knowing any concrete values. To address the simultaneous challenges of scalability and precision, we formalize and implement an interface for symbolic set abstractions and construct multiple abstractions relying on both specialized data structures and off-the-shelf theorem provers. Additionally, we develop techniques for lifting existing domains to improve performance and precision. We evaluate these new domains on real-world data structure analysis problems.
Fine grained SMT proofs for the theory of fixed-width bit-vectors
SPEAKER: unknown
ABSTRACT. Many high-level verification tools rely on SMT solvers to efficiently
discharge complex verification conditions. Some applications require
more than just a yes/no answer from the solver. For satisfiable
problems, a satisfying model is a natural artefact. In the
unsatisfiable case, an externally checkable proof can serve as a
certificate of correctness and can be mined to gain additional insight
into the problem.
In this paper we present a method of encoding and checking
SMT-generated proofs for the theory of fixed-width bit-vectors. Proof
generation and checking for the bit-vector theory poses additional
challenges compared to other theories: reducing the problem to
propositional logic can result in large resolution proofs as well as
requiring a proof that the reduction itself is correct. We describe a
fine-grained proof system formalized in the LFSC framework that
addresses some of these challenges by the use of computational
side-conditions. We instrument the CVC4 SMT solver to automatically
generate such proofs and evaluate the performance impact of proof
generation.
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.
Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo
SPEAKER: unknown
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 of BWare.
Modelling Moral Reasoning and Ethical Responsibility with Logic Programming
SPEAKER: unknown
ABSTRACT. In this paper, we investigate the use of high-level action languages for representing and reasoning about ethical responsibility in goal specification domains. First, we present a simplified Event Calculus formulated as a logic program under the stable model semantics in order to represent situations within Answer Set Programming. Second, we introduce a model of causality that allows us to use an answer set solver to perform reasoning over the agent’s ethical responsibility. We then extend and test this framework against the Trolley Problem and the Doctrine of Double Effect. The overarching aim of the paper is to propose a general and adaptable formal language that may be employed over a variety of ethical scenarios in which the agent’s responsibility must be examined and their choices determined. Our fundamental motivation rests in the will to displace the burden of moral reasoning from the programmer to the program itself, moving away from current computational ethics that too easily embed moral reasoning withing the computational engines, thereby feeding atomic answers that fail to truly represent the underlying dynamics at play.
ABSTRACT. Rule-based languages are being used for ever more ambitious applications. As program size grows however, so does the overhead of team-based development, reusing components, and just keeping a large flat collection of rules from interfering. In this paper, we propose a module system for a small logically-motivated rule-based language. The resulting modules are nothing more than rewrite rules of a specific form, which are themselves just logic formulas. Yet, they provide some of the same features found in advanced module systems such as that of Standard ML, in particular name space separation, support for abstract data types, and parametrization (functors in ML). Our modules also offer essential features for concurrent programming such as facilities for sharing private names. This approach is directly applicable to other rule-based languages, including most forward-chaining logic programming languages and many process algebras.
ABSTRACT. We present a new interpreter for λProlog that runs consistently faster than the bytecode compiled by Teyjus, that is believed to be the best available implementation for λProlog. The key insight is the identification of a fragment of the language, which we call Reduction-Free Fragment, that occurs quite naturally in λProlog programs and that admits constant time reduction and unification rules. The implementation exploits De Bruijn levels and no explicit substitutions, whereas Teyjus is based on De Bruijn indexes and explicit substitutions (the suspension calculus).
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. A new logical framework with explicit linear contexts and names is
presented, with the purpose of enabling direct and flexible
manipulation of contexts, both for representing systems and
meta-properties. The framework is a conservative extension of the
logical framework LF, and builds on linear logic and contextual
modal type theory. We prove that the framework admits canonical
forms, and that it possesses all desirable meta-theoretic properties,
in particular hereditary substitutions.
As proof of concept, we give an encoding of the one-sided sequent
calculus for classical linear logic and the corresponding
cut-admissibility proof, as well as an encoding of parallel reduction
of lambda terms with the corresponding value-soundness proof.
ABSTRACT. Focused proofs are sequent calculus proofs that group inference rules into alternating negative and positive phases. These phases can then be used to define macro-level inference rules from Gentzen's original and tiny introduction and structural rules.
We show here that the inference rules of labeled proof systems for modal logics can similarly be described as pairs of such negative and positive phases within the LKF focused proof system (which contains no modal connectives). In particular, we consider the system G3K of Negri for the modal logic K and define a translation from labeled modal formulas into first-order polarized formulas and show a strict correspondence between derivations in the two systems, i.e., each rule application in G3K corresponds to a bipole - a pair of a positive and a negative phases - in LKF. Since geometric axioms (when properly polarized) induce bipoles, this strong correspondence holds for all modal logics whose Kripke frames are characterized by geometric properties.
We extend these results to present a focused labeled proof system for this same class of modal logics and show its soundness and completeness. This resulting proof system allows one to define a rich set of normal forms of modal logic proofs.
A Labelled Sequent Calculus for Intuitionistic Public Announcement Logic
SPEAKER: unknown
ABSTRACT. Intuitionistic Public Announcement Logic (IntPAL) proposed by Ma et al. (2014) aims for a formal expression of change of knowledge in a constructive manner. IntPAL is a combination of Public Announcement Logic (PAL) by Plaza (1989) and the intuitionistic modal logic IK by Fischer Servi (1984) and Simpson (1994). We also refer to IK for the basis of this paper. Meanwhile, Nomura et al. (2015) provided a cut-free labelled sequent calculus based on the study of Maffezioli et al. (2010). In this paper, we introduce a labelled sequent calculus for IntPAL (we call it GIntPAL) as both an intuitionistic variant of GPAL and a public announcement extension of Simpson's labelled
calculus, and show that all theorems of the Hilbert axiomatization of IntPAL are also provable in GIntPAL with the cut rule. Then we prove the admissibility of the cut rule in GIntPAL and also its soundness for birelational Kripke semantics. Finally, we derive the semantic completeness of GIntPAL as a corollary of these theorems.
ABSTRACT. The usual Skolemization procedure, which removes strong quantifiers by introducing new function symbols, is in general unsound for first-order substructural logics defined based on classes of complete residuated lattices. However, it is shown here (following similar ideas of Baaz and Iemhoff for first-order intermediate logics) that first-order substructural logics with a semantics satisfying certain witnessing conditions admit a "parallel" Skolemization procedure where a strong quantifier is removed by introducing a finite disjunction or conjunction (as appropriate) of formulas with multiple new function symbols. These logics typically lack equivalent prenex forms. Also, semantic consequence does not in general reduce to satisfiability. The Skolemization theorems presented here therefore take various forms, applying to the left or right of the consequence relation, and to all formulas or only prenex formulas.
Automated Theorem Proving by Translation to Description Logic
SPEAKER: unknown
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.