Details

Autor(en) / Beteiligte

• Kobayashi, Munehiro
• Iwane, Hidenao
• Matsuzaki, Takuya
• Anai, Hirokazu
• Rump, Siegfried M.
• Yap, Chee K.
• Kotsireas, Ilias S.

Titel

Efficient Subformula Orders for Real Quantifier Elimination of Non-prenex Formulas

Ist Teil von

• Mathematical Aspects of Computer and Information Sciences, p.236-251

Ort / Verlag

Cham: Springer International Publishing

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• In this paper we study speeding up real quantifier elimination (QE) methods for non-prenex formulas. Our basic strategy is to solve non-prenex first-order formulas by performing QE for subformulas constituting the input non-prenex formula. We propose two types of methods (heuristic methods/machine learning based methods) to determine an appropriate ordering of QE computation for the subformulas. Then we empirically examine their effectiveness through experimental results over more than 2,000 non-trivial example problems. Our experiment results suggest machine learning can save much effort spent to design effective heuristics by trials and errors without losing efficiency of QE computation.