Eliminace kvantifikátorů v oboru reálných čísel je jednou z mladších oblastí
na pomezí matematiky, logiky a výpočetní techniky. Pomocí metody nazývané
cylindrická algebraická dekompozice dovoluje zjednodušit matematické kvantifikované
formule do jednoduššího tvaru neobsahujícího kvantifikátory. Jelikož se jedná o vcelku
složitý postup, jsou velmi užitečné programy počítačové algebry (například program
Mathematica od firmy Wolfram Research). Mnoho matematických úloh (jako třeba
řešení rovnic a nerovnic) může být převedeno právě na matematické formule obsahující
kvantifikátory, u nichž pak eliminace dovoluje zjistit řešení nebo určit, zda jsou
řešitelné. Z toho důvodu může být tato metoda přínosem nejen pro matematiky
samotné, ale též pro učitele matematiky a talentované žáky.
Anotace v angličtině
Quantifier elimination over real fields is a discipline connected with
mathematics, logic and computer science. Using so called cylindrical algebraic
decomposition it allows to simplify mathematical formulas with quantifiers into
quantifier-free formulas. Since this is quite complex problem programs of computer
algebra (such as Mathematica by Wolfram Research) are very helpful. Many
mathematical problems (for example equations and inequations) can be transformed into
quantified formulas and the elimination is a way to solve them or find out if they are
solvable. Therefore this method may be useful not only for mathematicians but for math
teachers and talented pupils too.
Klíčová slova
eliminace kvantifikátorů, CAD, cylindrická algebraická dekompozice,
Alfred Tarski, George E. Collins, počítačová algebra, Mathematica, trojúhelníková
dekompozice, regulární řetězce
Klíčová slova v angličtině
quantifier elimination, CAD, cylindrical algebraic decomposition, Alfred
Tarski, George E. Collins, computer algebra, Mathematica, triangular decomposition,
regular chains
Rozsah průvodní práce
124
Jazyk
CZ
Anotace
Eliminace kvantifikátorů v oboru reálných čísel je jednou z mladších oblastí
na pomezí matematiky, logiky a výpočetní techniky. Pomocí metody nazývané
cylindrická algebraická dekompozice dovoluje zjednodušit matematické kvantifikované
formule do jednoduššího tvaru neobsahujícího kvantifikátory. Jelikož se jedná o vcelku
složitý postup, jsou velmi užitečné programy počítačové algebry (například program
Mathematica od firmy Wolfram Research). Mnoho matematických úloh (jako třeba
řešení rovnic a nerovnic) může být převedeno právě na matematické formule obsahující
kvantifikátory, u nichž pak eliminace dovoluje zjistit řešení nebo určit, zda jsou
řešitelné. Z toho důvodu může být tato metoda přínosem nejen pro matematiky
samotné, ale též pro učitele matematiky a talentované žáky.
Anotace v angličtině
Quantifier elimination over real fields is a discipline connected with
mathematics, logic and computer science. Using so called cylindrical algebraic
decomposition it allows to simplify mathematical formulas with quantifiers into
quantifier-free formulas. Since this is quite complex problem programs of computer
algebra (such as Mathematica by Wolfram Research) are very helpful. Many
mathematical problems (for example equations and inequations) can be transformed into
quantified formulas and the elimination is a way to solve them or find out if they are
solvable. Therefore this method may be useful not only for mathematicians but for math
teachers and talented pupils too.
Klíčová slova
eliminace kvantifikátorů, CAD, cylindrická algebraická dekompozice,
Alfred Tarski, George E. Collins, počítačová algebra, Mathematica, trojúhelníková
dekompozice, regulární řetězce
Klíčová slova v angličtině
quantifier elimination, CAD, cylindrical algebraic decomposition, Alfred
Tarski, George E. Collins, computer algebra, Mathematica, triangular decomposition,
regular chains
Zásady pro vypracování
1) Úvod do problematiky.
2) Historie problematiky.
3) Algoritmizace CAD a QE.
4) Matematické programy pracující s CAD.
5) Využití QE ve středoškolské a vysokoškolské praxi.
Zásady pro vypracování
1) Úvod do problematiky.
2) Historie problematiky.
3) Algoritmizace CAD a QE.
4) Matematické programy pracující s CAD.
5) Využití QE ve středoškolské a vysokoškolské praxi.
Seznam doporučené literatury
WINKLER, Franz. Polynomial Algorithms in Computer Algebra. New York: Springer, 1996. 270 s. ISBN 32-118-2759-5.
TARSKI, Alfred. A Decision Method for Elementary Algebra and Geometry. 2. vyd. Santa Monica, California: The RAND Corporation, 1957. Dostupné z: http://www.rand.org/pubs/reports/2008/R109.pdf
DAVÍDEK, Ondřej. Cylindrická algebraická dekompozice a její aplikace. Plzeň, 2009. Diplomová práce. ZČU v Plzni. Vedoucí práce Ing. Bohumír Bastl, PhD.
ARNON, D. S., COLLINS, G. E., MCCALLUM, S. Cylindrical algebraic decomposition I: the basic algorithm. SIAM Journal on Computing. 1984, vol. 13, is. 4, s. 865-877. Dostupný z: http://www.cs.purdue.edu/research/technical_reports/1982/TR%2082-427A.pdf
ARNON, D. S., COLLINS, G. E., MCCALLUM, S. Cylindrical algebraic decomposition II: an adjacency algorithm for the plane. SIAM Journal on Computing. 1984, vol. 13, is. 4, s. 878-888. Dostupný z: http://www.cs.purdue.edu/research/technical_reports/1982/TR%2082-428.pdf
Seznam doporučené literatury
WINKLER, Franz. Polynomial Algorithms in Computer Algebra. New York: Springer, 1996. 270 s. ISBN 32-118-2759-5.
TARSKI, Alfred. A Decision Method for Elementary Algebra and Geometry. 2. vyd. Santa Monica, California: The RAND Corporation, 1957. Dostupné z: http://www.rand.org/pubs/reports/2008/R109.pdf
DAVÍDEK, Ondřej. Cylindrická algebraická dekompozice a její aplikace. Plzeň, 2009. Diplomová práce. ZČU v Plzni. Vedoucí práce Ing. Bohumír Bastl, PhD.
ARNON, D. S., COLLINS, G. E., MCCALLUM, S. Cylindrical algebraic decomposition I: the basic algorithm. SIAM Journal on Computing. 1984, vol. 13, is. 4, s. 865-877. Dostupný z: http://www.cs.purdue.edu/research/technical_reports/1982/TR%2082-427A.pdf
ARNON, D. S., COLLINS, G. E., MCCALLUM, S. Cylindrical algebraic decomposition II: an adjacency algorithm for the plane. SIAM Journal on Computing. 1984, vol. 13, is. 4, s. 878-888. Dostupný z: http://www.cs.purdue.edu/research/technical_reports/1982/TR%2082-428.pdf