Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Current Challenges in Developing Open Source Computer Algebra Systems Read chapter Read first chapter

2016 | OriginalPaper | Chapter

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

Authors : Munehiro Kobayashi, Hidenao Iwane, Takuya Matsuzaki, Hirokazu Anai

Published in: Mathematical Aspects of Computer and Information Sciences

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Improving a CGS-QE Algorithm
next chapter Solving Extended Ideal Membership Problems in Rings of Convergent Power Series via Gröbner Bases
Literature
1.
Arai, N.H., Matsuzaki, T., Iwane, H., Anai, H.: Mathematics by machine. In: Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation, pp. 1–8. ACM (2014)
2.
Brown, C.W., Davenport, J.H.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proceedings of the 2007 International Symposium on Symbolic and Algebraic Computation, ISSAC 2007, pp. 54–60. ACM, New York (2007)
3.
Chang, C.C., Lin, C.J.: LIBSVM: a library for support vector machines. ACM Trans. Intell. Syst. Technol. (TIST) 2(3), 27 (2011)
4.
Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation, pp. 111–118. ACM (2004)
5.
Hsu, C.W., Chang, C.C., Lin, C.J., et al.: A practical guide to support vector classification (2003)
6.
Huang, Z., England, M., Wilson, D., Davenport, J.H., Paulson, L.C., Bridge, J.: Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 92–107. Springer, Heidelberg (2014)
7.
Iwane, H., Higuchi, H., Anai, H.: An effective implementation of a special quantifier elimination for a sign definite condition by logical formula simplification. In: Gerdt, V.P., Koepf, W., Mayr, E.W., Vorozhtsov, E.V. (eds.) CASC 2013. LNCS, vol. 8136, pp. 194–208. Springer, Heidelberg (2013)CrossRef
8.
Iwane, H., Matsuzaki, T., Arai, N., Anai, H.: Automated natural language geometry math problem solving by real quantifier elimination. In: Proceedings of the 10th International Workshop on Automated Deduction in Geometry, pp. 75–84 (2014)
9.
Iwane, H., Yanami, H., Anai, H.: SyNRAC: a toolbox for solving real algebraic constraints. In: Hong, H., Yap, C. (eds.) ICMS 2014. LNCS, vol. 8592, pp. 518–522. Springer, Heidelberg (2014)
10.
Matsuzaki, T., Iwane, H., Anai, H., Arai, N.H.: The most uncreative examinee: a first step toward wide coverage natural language math problem solving. In: Twenty-Eighth AAAI Conference on Artificial Intelligence, pp. 1098–1104 (2014)
11.
Strzeboński, A.W.: Real quantifier elimination for non-prenex formulas (2011). unpublished manuscript
Metadata
Title
Efficient Subformula Orders for Real Quantifier Elimination of Non-prenex Formulas
Authors
Munehiro Kobayashi
Hidenao Iwane
Takuya Matsuzaki
Hirokazu Anai
Copyright Year
2016
Book
Mathematical Aspects of Computer and Information Sciences

Print ISBN: 978-3-319-32858-4

Electronic ISBN: 978-3-319-32859-1

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-319-32859-1_21

Premium Partner

    Image Credits