previous day
next day
all days

View: session overviewtalk overviewside by side with other conferences

09:00-10:30 Session 110D: Decidability & Complexity
Location: Maths LT2
Deciding the First-Order Theory of an Algebra of Feature Trees with Updates

ABSTRACT. We investigate a logic of an algebra of trees including the update operation, which expresses that a tree is obtained from an input tree by replacing a particular direct subtree of the input tree, while leaving the rest intact. This operation improves on the expressivity of existing logics of tree algebras in our case of feature trees, which allow for an unbounded number of children of a node in a tree.

We show that the first-order theory of this algebra is decidable via a weak quantifier elimination procedure which is allowed to swap existential quantifiers for universal quantifiers. This study is motivated by the logical modeling of transformations on UNIX file system trees expressed in a simple programming language.

Complexity of Combinations of Qualitative Constraint Satisfaction Problems

ABSTRACT. The CSP of a first-order theory $T$ is the problem of deciding for a given finite set $S$ of atomic formulas whether $T \cup S$ is satisfiable. Let $T_1$ and $T_2$ be two theories with countably infinite models and disjoint signatures. Nelson and Oppen presented conditions that imply decidability (or polynomial-time decidability) of $\mathrm{CSP}(T_1 \cup T_2)$ under the assumption that $\mathrm{CSP}(T_1)$ and $\mathrm{CSP}(T_2)$ are decidable (or polynomial-time decidable). We show that for a large class of $\omega$-categorical theories $T_1, T_2$ the Nelson-Oppen conditions are not only sufficient, but also necessary for polynomial-time tractability of $\mathrm{CSP}(T_1 \cup T_2)$ (unless P=NP).

Focussing, MALL and the polynomial hierarchy

ABSTRACT. We investigate how to extract alternating time bounds from focussed proofs, treating synchronous phases as nondeterministic computation and asynchronous phases as co-nondeterministic computation. We refine the usual presentation of focussing to account for deterministic computations in proof search, which correspond to invertible rules that do not branch, more faithfully associating phases of focussed proof search to their alternating time complexity.

As our main result, we give a focussed system for affine MALL and give encodings to and from true quantified Boolean formulas (QBFs): in one direction we encode QBF satisfiability and in the other we encode focussed proof search. Moreover we show that the composition of the two encodings preserves quantifier alternation, hence yielding fragments of affine MALL complete for each level of the polynomial hierarchy. This refines the well-known result that affine MALL is PSPACE-complete.

10:30-11:00Coffee Break
11:00-12:30 Session 112E: Superposition
Location: Maths LT2
Superposition with Datatypes and Codatatypes

ABSTRACT. The absence of a finite axiomatization of the first-order theory of datatypes and codatatypes represents a challenge for automatic theorem provers. We propose two approaches to reason by saturation in this theory: one is a conservative theory extension with a finite number of axioms; the other is an extension of the superposition calculus, in conjunction with axioms. Both techniques are refutationally complete with respect to nonstandard models of datatypes and non-branching codatatypes. They take into account the acyclicity of datatype values and the existence and uniqueness of cyclic codatatype values. We implemented them in the first-order prover Vampire and compare them experimentally.

Superposition for Lambda-Free Higher-Order Logic

ABSTRACT. We introduce refutationally complete superposition calculi for intentional and extensional lambda-free higher-order logic, a formalism that allows partial application and applied variables. The intentional variants perfectly coincide with standard superposition on first-order clauses. The calculi are parameterized by a well-founded term order that need not be compatible with arguments, making it possible to employ the lambda-free higher-order lexicographic path and Knuth-Bendix orders. We implemented the calculi in the Zipperposition prover and evaluated them on TPTP benchmarks. They appear promising as a stepping stone towards complete, efficient automatic theorem provers for full higher-order logic.

Efficient encodings of first-order Horn formulas in equational logic

ABSTRACT. We present several translations from first-order Horn formulas to equational logic. The goal of these translations is to allow equational theorem provers to efficiently reason about non-equational problems. Using the translations we were able to solve 33 problems of rating 1.0 from the TPTP.

12:30-14:00Lunch Break
14:00-15:30 Session 115: FLoC Plenary Lecture: Byron Cook
Location: Maths LT1
Formal Reasoning about the Security of Amazon Web Services

ABSTRACT. Amazon Web Services (AWS) uses and develops tools based on formal verification to reason about the security of AWS itself, as well as the security of systems that customers build on AWS. This talk will focus on how AWS services connect customers to logic-based techniques, as well as how AWS uses formal verification internally to provide higher assurance of its security.

15:30-16:00Coffee Break
16:00-18:00 Session 116A: Oxford Union Debate: Ethics & Morality of Robotics

Public debate on "Ethics & Morality of Robotics" with panelists specializing in ethics, law, computer science, data security and privacy:

  • Prof Matthias Scheutz, Dr Sandra Wachter, Prof Jeannette Wing, Prof Francesca Rossi, Prof Luciano Floridi & Prof Ben Kuipers

See http://www.floc2018.org/public-debate/ for further details and to register.

Location: Oxford Union
19:00-21:30 FLoC banquet at Ashmolean Museum

FLoC banquet at Ashmolean Museum. Drinks and food available from 7pm (pre-booking via FLoC registration system required; guests welcome).