Efficient subformula orders for real quantifier elimination of non-prenex formulas

DOI10.1007/978-3-319-32859-1_21MaRDI QIDQ2807841zbMATH OpenOpenAlexFDO

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

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

non-prenex formulasreal quantifier eliminationsupport vector machine

Mathematics Subject Classification ID

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

Recommendations

• Efficient Preprocessing Methods for Quantifier Elimination
• scientific article; zbMATH DE number 1302474
• scientific article; zbMATH DE number 1263423
• Quantifier elimination for real algebra -- the quadratic case and beyond
• Simplification of quantifier-free formulae over ordered fields

Cited in

(6)

• Using machine learning to improve cylindrical algebraic decomposition
• Efficient Preprocessing Methods for Quantifier Elimination
• Improved Cross-Validation for Classifiers that Make Algorithmic Choices to Minimise Runtime Without Compromising Output Correctness
• Applying machine learning to heuristics for real polynomial constraint solving
• Can an A.I. win a medal in the mathematical olympiad? -- Benchmarking mechanized mathematics on pre-university problems
• Explainable AI insights for symbolic computation: a case study on selecting the variable ordering for cylindrical algebraic decomposition

This page was built for publication: Efficient subformula orders for real quantifier elimination of non-prenex formulas

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2807841)