[Matryoshka-devel] Paper drafts

Jasmin Blanchette jasmin.blanchette at gmail.com
Tue Feb 7 16:40:27 CET 2017


Hi all,

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
	Simon Cruanes
	http://cedeela.fr/~simon/files/cade_17_paper.pdf

	Transfinite Knuth–Bendix Orders for Lambda-Free Higher-Order Terms
	Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand
	http://people.mpi-inf.mpg.de/~jblanche/lambda_free_kbo_conf.pdf

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).

Jasmin



More information about the matryoshka-devel mailing list