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

DOI10.1007/978-3-319-32859-1_21zbMath1460.68086OpenAlexW2467888180MaRDI QIDQ2807841

Munehiro Kobayashi, Hirokazu Anai, Takuya Matsuzaki, Hidenao Iwane

Publication date: 25 May 2016

Published in: Mathematical Aspects of Computer and Information Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-32859-1_21

zbMATH Keywords

support vector machinereal quantifier eliminationnon-prenex formulas

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Quantifier elimination, model completeness, and related topics (03C10)

Related Items

Applying Machine Learning to Heuristics for Real Polynomial Constraint Solving, Explainable AI insights for symbolic computation: a case study on selecting the variable ordering for cylindrical algebraic decomposition, Can an A.I. win a medal in the mathematical olympiad? – Benchmarking mechanized mathematics on pre-university problems1, Using machine learning to improve cylindrical algebraic decomposition, Improved Cross-Validation for Classifiers that Make Algorithmic Choices to Minimise Runtime Without Compromising Output Correctness