iprover-QBF

Submitter: Konstantin Korovin
Description: Devised by Konstantin Korovin, is a general purpose theorem prover for first-order logic based an instantiation calculus Inst-Gen. It incorporates a QBF solving mode which is based on a translation of QBF into the effectively propositional fragment of first-order logic (EPR). The basic translation follows [1], and it is also implemented a dedicated Skolemization procedure with several optimization.
[1] Seidl, M., Lonsing, F., Biere, A.: qbf2epr: A Tool for Generating EPR Formulas from QBF. PAAR@ IJCAR 21 (2012) 139148
Results: