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) 139–148 | ||
| Results: | |||