A Grounder From Second-Order Logic To QBF

EasyChair Preprint no. 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: grounding, modelling languages, QBF, QDimacs, second-order logic

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