[Matryoshka-devel] Paper drafts
jasmin.blanchette at gmail.com
Tue Feb 7 16:40:27 CET 2017
In Nancy and Saarbrücken, we are working on some CADE submissions. We have two drafts that we would like to share with you:
Satisfiability Modulo Bounded Checking
Transfinite Knuth–Bendix Orders for Lambda-Free Higher-Order Terms
Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand
The first paper (with an optimistically named URL) describes the SMBC tool that Simon advertised on this mailing list a few weeks ago. SMBC can do some higher-order model finding and can be used as a backend in Nunchaku. The approach (a kind of hybrid between narrowing and SAT solving that is reminiscent of Koen Claessen et al.'s HBMC) is quite interesting, and the evaluation against a wide range of tools has many nice benchmark problems.
The second paper is about some first steps towards higher-order superposition, by focusing first on the term orderings. An earlier paper dealt with RPO (and hence LPO); this one is about KBO. KBO is a priori easy to generalize to lambda-free higher-order (a.k.a. applicative first order), but things get messier once you add subterm coefficients and special weight-0 unary symbols. Everything is formalized in Isabelle.
Comments welcome, before or after the deadline (18 February).
More information about the matryoshka-devel