A Grounder From Second-Order Logic To QBF

EasyChair Preprint 392

Abstract

Recent solver research has developed powerful QBF solvers. Alas, we know of few tools that provide a modelling language on a higher level, translating this to QBF. This is surprising, as in the closely related field of SAT solvers, research has gone hand in hand with the develop- ment of such systems. This extended abstract on work in progress reports on a system that allows the use of second-order logic as a high-level modelling language and that grounds (translates) models written in such a language to a QBF formula. We provide an example encoding, outline the grounding process and propose further research and experiments.

Keyphrases: QBF, QDimacs, grounding, modelling languages, second-order logic

@booklet{EasyChair:392,
  author    = {Matthias van der Hallen and Gerda Janssens},
  title     = {A Grounder From Second-Order Logic To QBF},
  doi       = {10.29007/k3nd},
  howpublished = {EasyChair Preprint 392},
  year      = {EasyChair, 2018}}