View: session overviewtalk overviewside by side with other conferences

09:00 | SPEAKER: Nicolas Jeannerod 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. |

09:30 | SPEAKER: Johannes Greiner 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). |

10:00 | 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 satisﬁability and in the other we encode focussed proof search. Moreover we show that the composition of the two encodings preserves quantiﬁer alternation, hence yielding fragments of affine MALL complete for each level of the polynomial hierarchy. This reﬁnes the well-known result that affine MALL is PSPACE-complete. |

11:00 | SPEAKER: Simon Robillard 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. |

11:30 | SPEAKER: Alexander Bentkamp 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. |

12:00 | SPEAKER: Nicholas Smallbone 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. |

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.

17:30 | IJCAR competition presentations |

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