Friday 7 July 2017, LSV, 10:00: Deduction modulo in Zipperposition: past, present, and future, Simon Cruanes (INRIA Nancy).
Zipperposition is an automatic theorem prover based on Superposition, developed in OCaml. It features several extensions that go beyond the usual untyped first-order logic: polymorphic types, linear arithmetic for integer and rational numbers, structural induction, and rewrite rules. As mandated by the Committee for Quality Deduction Modulo, these rewrite rules can be defined both for terms and propositions. In our framework, propositional rewrite rules take the form of (simplifying) polarized resolution and can optionally be restricted to only one polarity. It is also possible to define rewrite rules where the left-hand side is an equation, thus redefining the notion of equality for a given type — this ability is used in a development aiming at proving lemmas on set theory (in cooperation with David Delahaye and Pierre-Louis Euvrard), where set equality is defined by extensionality. Overall, Zipperposition could be a good testbed for exploring automatic deduction modulo.