CINXE.COM

Tarski's Theorem -- from Wolfram MathWorld

<!doctype html> <html lang="en" class="foundationsofmathematics mathworldcontributors"> <head> <title>Tarski's Theorem -- from Wolfram MathWorld</title> <meta name="DC.Title" content="Tarski's Theorem" /> <meta name="DC.Creator" content="Weisstein, Eric W." /> <meta name="DC.Description" content="Tarski's theorem says that the first-order theory of reals with +, *, =, and &gt; allows quantifier elimination. Algorithmic quantifier elimination implies decidability assuming that the truth values of sentences involving only constants can be computed. However, the converse is not true. For example, the first-order theory of reals with +, *, and = is decidable, but does not allow quantifier elimination. Tarski's theorem means that the solution set of a quantified system of real algebraic..." /> <meta name="description" content="Tarski's theorem says that the first-order theory of reals with +, *, =, and &gt; allows quantifier elimination. Algorithmic quantifier elimination implies decidability assuming that the truth values of sentences involving only constants can be computed. However, the converse is not true. For example, the first-order theory of reals with +, *, and = is decidable, but does not allow quantifier elimination. Tarski's theorem means that the solution set of a quantified system of real algebraic..." /> <meta name="DC.Date.Modified" scheme="W3CDTF" content="2003-08-04" /> <meta name="DC.Subject" scheme="MathWorld" content="Mathematics:Foundations of Mathematics:Logic:Decidability" /> <meta name="DC.Subject" scheme="MathWorld" content="Mathematics:MathWorld Contributors:Strzebonski" /> <meta name="DC.Subject" scheme="MSC_2000" content="03B25" /> <meta name="DC.Rights" content="Copyright 1999-2024 Wolfram Research, Inc. See https://mathworld.wolfram.com/about/terms.html for a full terms of use statement." /> <meta name="DC.Format" scheme="IMT" content="text/html" /> <meta name="DC.Identifier" scheme="URI" content="https://mathworld.wolfram.com/TarskisTheorem.html" /> <meta name="DC.Language" scheme="RFC3066" content="en" /> <meta name="DC.Publisher" content="Wolfram Research, Inc." /> <meta name="DC.Relation.IsPartOf" scheme="URI" content="https://mathworld.wolfram.com/" /> <meta name="DC.Type" scheme="DCMIType" content="Text" /> <meta name="Last-Modified" content="2003-08-04" /> <meta property="og:image" content="https://mathworld.wolfram.com/images/socialmedia/share/ogimage_TarskisTheorem.png"> <meta property="og:url" content="https://mathworld.wolfram.com/TarskisTheorem.html"> <meta property="og:type" content="website"> <meta property="og:title" content="Tarski's Theorem -- from Wolfram MathWorld"> <meta property="og:description" content="Tarski's theorem says that the first-order theory of reals with +, *, =, and &gt; allows quantifier elimination. Algorithmic quantifier elimination implies decidability assuming that the truth values of sentences involving only constants can be computed. However, the converse is not true. For example, the first-order theory of reals with +, *, and = is decidable, but does not allow quantifier elimination. Tarski's theorem means that the solution set of a quantified system of real algebraic..."> <meta name="twitter:card" content="summary_large_image"> <meta name="twitter:site" content="@WolframResearch"> <meta name="twitter:title" content="Tarski's Theorem -- from Wolfram MathWorld"> <meta name="twitter:description" content="Tarski's theorem says that the first-order theory of reals with +, *, =, and &gt; allows quantifier elimination. Algorithmic quantifier elimination implies decidability assuming that the truth values of sentences involving only constants can be computed. However, the converse is not true. For example, the first-order theory of reals with +, *, and = is decidable, but does not allow quantifier elimination. Tarski's theorem means that the solution set of a quantified system of real algebraic..."> <meta name="twitter:image:src" content="https://mathworld.wolfram.com/images/socialmedia/share/ogimage_TarskisTheorem.png"> <link rel="canonical" href="https://mathworld.wolfram.com/TarskisTheorem.html" /> <meta http-equiv="x-ua-compatible" content="ie=edge"> <meta name="viewport" content="width=device-width, initial-scale=1"> <meta charset="utf-8"> <script async src="/common/javascript/analytics.js"></script> <script async src="//www.wolframcdn.com/consent/cookie-consent.js"></script> <script async src="/common/javascript/wal/latest/walLoad.js"></script> <link rel="stylesheet" href="/css/styles.css"> <link rel="preload" href="//www.wolframcdn.com/fonts/source-sans-pro/1.0/global.css" as="style" onload="this.onload=null;this.rel='stylesheet'"> <noscript><link rel="stylesheet" href="//www.wolframcdn.com/fonts/source-sans-pro/1.0/global.css"></noscript> </head> <body id="topics"> <main id="entry"> <div class="wrapper"> <section id="container"> <header class="text-align-c"> <div id="header-dropdown-menu"> <img src="/images/header/menu-icon.png" width="18" height="12" id="menu-icon"> <span class="display-n__600">TOPICS</span> </div> <svg version="1.1" id="logo" width="490" height="30" class="hide__600" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" x="0px" y="0px" viewBox="0 0 480.7 30" style="enable-background:new 0 0 480.7 30;" xml:space="preserve"> <g> <g> <g> <polygon fill="#0095AA" points="144.2,17.1 137.8,4 133.2,4 133.2,28.5 136.5,28.5 136.5,8.6 143,21.8 143,21.9 145.2,21.9 151.7,8.6 151.7,28.5 155,28.5 155,4 150.6,4"/> <path fill="#0095AA" d="M170.8,10.8c-1.2-1-3.1-1.5-5.8-1.5c-1.7,0-3.2,0.3-4.3,0.8c-1.2,0.6-2.1,1.4-2.6,2.4l0,0.1l2.6,1.6l0-0.1 c0.3-0.5,0.8-1,1.4-1.4c0.7-0.4,1.6-0.6,2.8-0.6c1.4,0,2.5,0.3,3.2,0.8c0.8,0.5,1.1,1.4,1.1,2.8v0.8l-4.5,0.4 c-1.8,0.2-3.2,0.6-4.1,1.1c-1,0.5-1.7,1.2-2.2,2c-0.5,0.8-0.8,1.9-0.8,3.2c0,1.7,0.5,3.1,1.5,4.2c1,1.1,2.4,1.6,4.1,1.6 c1.2,0,2.3-0.3,3.3-0.8c0.9-0.5,1.8-1.2,2.7-1.9v2.2h3.2V15.9C172.6,13.5,172,11.8,170.8,10.8z M169.4,19.2v4.4 c-0.4,0.3-0.8,0.6-1.2,0.9c-0.4,0.3-0.8,0.6-1.2,0.9c-0.4,0.2-0.9,0.5-1.3,0.6c-0.4,0.2-0.9,0.2-1.3,0.2c-1.1,0-1.9-0.2-2.4-0.7 c-0.5-0.5-0.8-1.2-0.8-2.3c0-1.1,0.4-2,1.2-2.6c0.8-0.6,2.2-1,4.2-1.2L169.4,19.2z"/> <path fill="#0095AA" d="M184.9,25.9c-0.7,0.3-1.6,0.5-2.4,0.5c-1,0-1.6-0.3-1.9-0.9c-0.3-0.6-0.4-1.7-0.4-3.2v-9.7h4.7V9.9h-4.7V4.7 h-3.2v5.1h-2.6v2.7h2.6v10.3c0,2.1,0.4,3.7,1.2,4.7c0.8,1,2.2,1.5,4.1,1.5c1.2,0,2.3-0.2,3.5-0.6l0.1,0L184.9,25.9L184.9,25.9z" /> <path fill="#0095AA" d="M198.1,9.3c-1.2,0-2.3,0.3-3.5,1c-1.1,0.6-2,1.3-2.9,2.1V2.1h-3.2v26.4h3.2V15.4c0.9-0.8,1.9-1.5,2.9-2.1 c1-0.6,1.9-0.9,2.7-0.9c0.8,0,1.3,0.1,1.7,0.4c0.4,0.3,0.7,0.7,0.8,1.2c0.2,0.6,0.3,1.7,0.3,3.5v11h3.2V16.1 c0-2.4-0.4-4.2-1.3-5.2C201.2,9.9,199.9,9.3,198.1,9.3z"/> <polygon fill="#0095AA" points="225.2,23.5 220.6,4 220.6,4 216.8,4 212.2,23.3 207.8,4 207.8,4 204.3,4 210.1,28.4 210.1,28.5 214.1,28.5 218.6,9.3 223.1,28.4 223.2,28.5 227.2,28.5 233.1,4 229.7,4"/> <path fill="#0095AA" d="M264.2,9.6c-1.2,0-2.2,0.3-3.2,1c-0.9,0.6-1.7,1.3-2.5,2.1V9.9h-3.2v18.7h3.2V15.7c1.1-1.1,2.1-1.8,2.9-2.3 c0.8-0.4,1.7-0.6,2.6-0.6c0.6,0,1.1,0.1,1.4,0.2l0.1,0l0.7-3.1l-0.1,0C265.6,9.7,264.9,9.6,264.2,9.6z"/> <rect x="269" y="2.1" fill="#0095AA" width="3.2" height="26.4"/> <path fill="#0095AA" d="M287.6,2.1v9.2c-1.5-1.3-3.2-1.9-5-1.9c-2.3,0-4.2,0.9-5.5,2.7c-1.3,1.8-2,4.3-2,7.3c0,3.1,0.6,5.5,1.8,7.2 c1.2,1.7,3,2.5,5.2,2.5c1.1,0,2.2-0.2,3.2-0.7c0.9-0.4,1.7-0.9,2.4-1.6v1.7h3.2V2.1H287.6z M287.6,14.2v9.7 c-0.6,0.6-1.4,1.1-2.2,1.6c-0.9,0.5-1.8,0.7-2.7,0.7c-2.9,0-4.3-2.3-4.3-6.9c0-2.4,0.4-4.2,1.3-5.4c0.9-1.1,2-1.7,3.3-1.7 C284.5,12.2,286,12.9,287.6,14.2z"/> </g> <g> <polygon fill="#666666" points="29,3.3 25.4,3.3 21,22.5 16.5,3.4 16.5,3.3 12.5,3.3 8,22.4 3.7,3.3 0,3.3 5.8,28.1 5.8,28.2 10,28.2 14.4,9.3 18.8,28.1 18.8,28.2 23.1,28.2 29,3.5"/> <path fill="#666666" d="M37,8.7c-2.7,0-4.8,0.8-6.2,2.5c-1.4,1.7-2.1,4.2-2.1,7.6c0,3.3,0.7,5.8,2.1,7.5c1.4,1.7,3.5,2.5,6.2,2.5 c2.7,0,4.8-0.9,6.2-2.6c1.4-1.7,2.1-4.2,2.1-7.5c0-3.3-0.7-5.8-2.1-7.5C41.8,9.5,39.7,8.7,37,8.7z M40.5,24 c-0.8,1.1-1.9,1.7-3.6,1.7c-1.7,0-2.9-0.5-3.7-1.7c-0.8-1.1-1.2-2.9-1.2-5.3c0-2.5,0.4-4.3,1.2-5.4c0.8-1.1,2-1.6,3.6-1.6 c1.6,0,2.8,0.5,3.5,1.6c0.8,1.1,1.2,2.9,1.2,5.4C41.7,21.2,41.3,22.9,40.5,24z"/> <rect x="48.7" y="1.4" fill="#666666" width="3.4" height="26.8"/> <path fill="#666666" d="M67,1.6c-1.1-0.5-2.3-0.7-3.6-0.7c-2.2,0-3.7,0.6-4.6,1.7c-0.9,1.1-1.3,2.8-1.3,5.1v1.6h-2.7v3h2.7v16.1h3.4 V12.2h4.1v-3h-4.1V7.6c0-1.5,0.2-2.5,0.6-3c0.4-0.5,1-0.7,2-0.7c0.4,0,0.8,0.1,1.3,0.2c0.5,0.1,0.9,0.3,1.2,0.4l0.2,0.1l1-3 L67,1.6z"/> <path fill="#666666" d="M76.3,8.9c-1.2,0-2.3,0.4-3.2,1c-0.8,0.6-1.6,1.2-2.3,2V9.2h-3.4v19h3.4v-13c1.1-1.1,2-1.8,2.8-2.2 c0.8-0.4,1.7-0.6,2.5-0.6c0.6,0,1,0.1,1.3,0.2l0.2,0.1l0.7-3.3l-0.1-0.1C77.7,9.1,77.1,8.9,76.3,8.9z"/> <path fill="#666666" d="M92.3,10.2c-1.2-1-3.1-1.5-5.8-1.5c-1.7,0-3.2,0.3-4.4,0.8c-1.2,0.6-2.1,1.4-2.7,2.5l-0.1,0.2l2.8,1.7 l0.1-0.2c0.3-0.5,0.7-0.9,1.4-1.3c0.6-0.4,1.6-0.6,2.8-0.6c1.3,0,2.4,0.3,3.2,0.7c0.7,0.5,1.1,1.4,1.1,2.8v0.7l-4.4,0.4 c-1.8,0.2-3.2,0.6-4.2,1.1c-1,0.5-1.7,1.2-2.2,2.1c-0.5,0.9-0.8,2-0.8,3.3c0,1.7,0.5,3.2,1.5,4.3c1,1.1,2.4,1.7,4.2,1.7 c1.2,0,2.3-0.3,3.3-0.8c0.8-0.5,1.7-1.1,2.5-1.8v2.1h3.4V15.4C94.1,12.9,93.5,11.2,92.3,10.2z M85.8,25.6c-1,0-1.8-0.2-2.3-0.7 c-0.5-0.4-0.8-1.2-0.8-2.2c0-1.1,0.4-1.9,1.1-2.5c0.8-0.6,2.2-1,4.1-1.1l2.7-0.3V23c-0.4,0.3-0.7,0.6-1.1,0.9 c-0.4,0.3-0.8,0.6-1.2,0.9c-0.4,0.2-0.9,0.5-1.3,0.6C86.7,25.5,86.2,25.6,85.8,25.6z"/> <path fill="#666666" d="M122,11.6c-0.3-0.9-0.9-1.7-1.6-2.2c-0.7-0.5-1.7-0.8-2.8-0.8c-1.3,0-2.4,0.4-3.4,1.1 c-0.9,0.6-1.8,1.4-2.7,2.3c-0.3-1.1-0.8-2-1.5-2.5c-0.8-0.6-1.8-0.9-3.1-0.9c-1.2,0-2.3,0.3-3.3,1c-0.8,0.6-1.6,1.2-2.4,2V9.2 h-3.4v19h3.4V15c0.9-0.9,1.8-1.7,2.7-2.2c0.8-0.5,1.6-0.8,2.2-0.8c0.7,0,1.2,0.1,1.5,0.3c0.3,0.2,0.5,0.6,0.6,1.2 c0.1,0.6,0.2,1.8,0.2,3.5v11.2h3.4V15c1.2-1.1,2.2-1.9,2.9-2.3c0.7-0.4,1.4-0.6,2-0.6c0.7,0,1.2,0.1,1.5,0.3 c0.3,0.2,0.5,0.6,0.7,1.1c0.1,0.6,0.2,1.8,0.2,3.6v11.2h3.4V15.6C122.5,13.9,122.3,12.5,122,11.6z"/> </g> <path fill="#0095AA" d="M242.6,8.3c-5.8,0-10.5,4.7-10.5,10.5s4.7,10.5,10.5,10.5c5.8,0,10.5-4.7,10.5-10.5S248.4,8.3,242.6,8.3z M235.7,23.9c0-0.5,0.1-1,0.2-1.6c1.1,0.9,2.3,1.7,3.7,2.4l-0.6,1.4C237.8,25.5,236.6,24.7,235.7,23.9z M238.8,26.5l-0.2,0.5 c-0.9-0.4-1.8-1-2.5-1.6c-0.2-0.2-0.3-0.5-0.3-0.8C236.6,25.4,237.7,26,238.8,26.5z M235.1,23.4c-0.8-0.8-1.4-1.6-1.6-2.4 c-0.1-0.5-0.1-1.1-0.1-1.6c0.4,0.8,1.1,1.7,2,2.5C235.3,22.4,235.2,23,235.1,23.4z M235.2,24.6L235.2,24.6 c-0.3-0.4-0.6-0.8-0.8-1.2c0.2,0.2,0.5,0.5,0.7,0.7C235.2,24.3,235.2,24.4,235.2,24.6z M233.4,17.5c0-0.1,0-0.1,0-0.2 c0.1-0.7,0.4-1.5,0.7-2.2c0-0.1,0-0.1,0.1-0.2c0,0.3,0.1,0.6,0.2,0.9c-0.3,0.4-0.5,0.8-0.7,1.2C233.5,17.1,233.5,17.3,233.4,17.5z M233.6,18.5c0.1-0.4,0.2-0.8,0.4-1.2c0.1-0.3,0.3-0.6,0.5-0.9c0.4,0.9,1.1,1.9,2.1,2.8c-0.2,0.4-0.4,0.8-0.6,1.2 c-0.1,0.3-0.3,0.6-0.4,0.9C234.6,20.4,234,19.4,233.6,18.5z M250.7,15.2c-0.1,0.4-0.3,0.8-0.8,1c-0.3-0.8-0.8-1.6-1.3-2.4 c0.2-0.1,0.3-0.3,0.4-0.5C249.7,14,250.3,14.6,250.7,15.2z M249.2,12.4c0.4,0.2,0.7,0.5,1,0.8c0.3,0.4,0.4,0.7,0.5,1 c0,0,0,0.1,0,0.1c-0.4-0.5-0.9-1-1.4-1.5C249.2,12.7,249.2,12.6,249.2,12.4C249.2,12.4,249.2,12.4,249.2,12.4z M251.8,17.8 c-0.1,0.6-0.5,1.1-1.1,1.5c-0.1-0.8-0.3-1.7-0.6-2.5c0.4-0.2,0.7-0.6,0.9-0.9C251.4,16.5,251.7,17.1,251.8,17.8z M251.3,15.2 C251.3,15.2,251.3,15.2,251.3,15.2C251.3,15.2,251.3,15.2,251.3,15.2C251.3,15.2,251.3,15.2,251.3,15.2z M239.2,16.5 c0.6-0.7,1.2-1.3,1.8-1.9c0.7,0.6,1.5,1.1,2.5,1.6l-1.1,2.4C241.2,18,240.1,17.3,239.2,16.5z M242.2,19.1l-1.1,2.4 c-1.4-0.7-2.7-1.5-3.7-2.4c0.4-0.7,0.9-1.4,1.5-2.1C239.8,17.8,241,18.5,242.2,19.1z M244,16.4c0.8,0.3,1.5,0.6,2.3,0.7 c0.2,0,0.4,0.1,0.6,0.1c0,0.9-0.1,1.8-0.2,2.6c-0.3,0-0.6-0.1-0.9-0.1c-1-0.2-2-0.5-3-0.9C243.3,18,243.7,17.2,244,16.4z M246.7,14.2c0.1,0.8,0.2,1.6,0.3,2.4c-0.2,0-0.4-0.1-0.5-0.1c-0.7-0.1-1.4-0.4-2.1-0.7c0.3-0.7,0.6-1.5,0.9-2.1 c0.4,0.2,0.8,0.3,1.2,0.4C246.5,14.2,246.6,14.2,246.7,14.2z M246.6,12.2c0.5,0.4,0.9,0.9,1.3,1.4c-0.2,0.1-0.5,0.1-0.8,0.1 C247,13.1,246.8,12.6,246.6,12.2z M245,13.1c-0.3-0.2-0.7-0.4-1-0.6c0.5-0.3,1.1-0.6,1.6-0.7L245,13.1z M244.7,13.6l-1,2.1 c-0.8-0.4-1.6-0.9-2.3-1.4c0.7-0.6,1.3-1,2-1.5C243.9,13.1,244.3,13.4,244.7,13.6z M241.1,13.9c-0.6-0.6-1-1.1-1.2-1.7 c0.8-0.3,1.7-0.5,2.6-0.7c0.1,0.3,0.3,0.6,0.6,0.9C242.5,12.8,241.8,13.3,241.1,13.9z M242.3,11c-0.9,0.1-1.8,0.3-2.6,0.6 c-0.1-0.5,0-0.9,0.2-1.3c0.8-0.1,1.6-0.1,2.4,0C242.3,10.6,242.3,10.8,242.3,11z M240.7,14.3c-0.7,0.6-1.3,1.2-1.9,1.9 c-0.8-0.8-1.4-1.6-1.7-2.4c0.7-0.5,1.5-0.9,2.3-1.3C239.6,13,240.1,13.7,240.7,14.3z M239.2,11.9c-0.8,0.3-1.6,0.8-2.3,1.2 c-0.2-0.7,0-1.4,0.4-1.9c0.6-0.3,1.3-0.6,2-0.8C239.1,10.9,239.1,11.4,239.2,11.9z M238.4,16.6c-0.6,0.7-1.1,1.4-1.5,2.1 c-1-0.9-1.7-1.9-2-2.9c0.5-0.6,1-1.2,1.7-1.8C236.9,14.9,237.6,15.8,238.4,16.6z M237,19.6c1.1,0.9,2.4,1.8,3.8,2.4l-1,2.1 c-1.4-0.7-2.7-1.5-3.8-2.4c0.1-0.3,0.3-0.7,0.4-1.1C236.7,20.3,236.8,20,237,19.6z M240.2,24.9c1.2,0.5,2.4,0.9,3.5,1.1 c0.3,0.1,0.6,0.1,0.9,0.1c-0.3,0.5-0.7,0.9-1.1,1.2c-0.3,0-0.7-0.1-1-0.1c-1-0.2-2-0.5-3-0.9C239.7,25.9,239.9,25.5,240.2,24.9z M243.7,27.9c0.3,0,0.6,0,0.9,0c-0.4,0.1-0.9,0.2-1.3,0.2C243.5,28.1,243.6,28,243.7,27.9z M244.3,27.4c0.3-0.3,0.7-0.7,1-1.2 c1.1,0.1,2.2,0,3-0.2c-0.4,0.4-0.8,0.7-1.2,1C246.3,27.3,245.4,27.5,244.3,27.4z M244.9,25.7c-0.4,0-0.7-0.1-1.1-0.2 c-1.1-0.2-2.3-0.6-3.4-1.1c0.1-0.3,0.3-0.6,0.5-1l0.5-1.1c1.2,0.5,2.4,0.9,3.5,1.1c0.3,0.1,0.7,0.1,1,0.2 c-0.1,0.4-0.3,0.7-0.4,1.1C245.3,25,245.1,25.3,244.9,25.7z M245.1,22.8c-1.1-0.2-2.3-0.6-3.4-1.1c0.4-0.8,0.7-1.6,1.1-2.4 c1,0.4,2.1,0.8,3.1,1c0.3,0.1,0.6,0.1,0.9,0.1c-0.1,0.9-0.3,1.7-0.6,2.5C245.8,22.9,245.4,22.9,245.1,22.8z M247.3,20.5 c1.1,0.1,2.2,0,3-0.4c0,0.8,0,1.7-0.2,2.4c-0.9,0.4-2,0.5-3.4,0.5C247,22.2,247.1,21.4,247.3,20.5z M247.4,19.9 c0.1-0.9,0.2-1.8,0.1-2.6c0.8,0,1.6,0,2.2-0.3c0.3,0.8,0.5,1.7,0.5,2.5C249.5,19.9,248.5,20,247.4,19.9z M249.5,16.5 c-0.5,0.2-1.2,0.3-2,0.2c0-0.9-0.1-1.7-0.3-2.5c0.4,0,0.7,0,1-0.1C248.8,14.8,249.2,15.6,249.5,16.5z M248.4,13.4 c-0.3-0.4-0.7-0.8-1.1-1.2c0.5,0.3,0.9,0.5,1.3,0.9C248.6,13.2,248.5,13.3,248.4,13.4z M247.4,11.7c0.4,0.1,0.7,0.2,1,0.3 c0.1,0.2,0.2,0.3,0.2,0.5C248.2,12.2,247.8,11.9,247.4,11.7z M246.7,11.1c0.2-0.1,0.4-0.2,0.5-0.2c0.2,0.1,0.3,0.2,0.5,0.4 C247.4,11.2,247.1,11.2,246.7,11.1z M246.2,10.9c0-0.2-0.1-0.5-0.1-0.7c0.2,0.1,0.5,0.2,0.7,0.3C246.6,10.7,246.4,10.8,246.2,10.9 z M246.6,13.6c0,0-0.1,0-0.1,0c-0.3-0.1-0.7-0.2-1-0.3c0.2-0.5,0.4-1,0.6-1.4C246.2,12.4,246.4,13,246.6,13.6z M244.8,10 c0.1,0,0.2,0,0.3,0.1c0.1,0,0.2,0,0.3,0.1c0.1,0.1,0.2,0.3,0.2,0.6C245.4,10.4,245.1,10.2,244.8,10z M245,11.4 c-0.5,0.2-0.9,0.4-1.4,0.7c-0.2-0.2-0.4-0.5-0.5-0.7C243.8,11.4,244.4,11.4,245,11.4z M244.6,11c-0.6,0-1.1,0-1.7,0 c0-0.2,0-0.3,0.1-0.5C243.5,10.6,244.1,10.8,244.6,11z M243.4,10.1c0.1-0.1,0.3-0.1,0.4-0.1c0.3,0.1,0.6,0.3,0.9,0.5 C244.3,10.4,243.9,10.2,243.4,10.1z M242.7,10c-0.5-0.1-1-0.1-1.5-0.1c-0.2,0-0.4,0-0.5,0c0.3-0.2,0.7-0.3,1.1-0.4 c0.5,0,0.9,0,1.4,0.2C243,9.8,242.8,9.9,242.7,10z M236.4,13.5c-0.6,0.5-1.2,1.1-1.7,1.7c-0.1-0.6-0.1-1.1,0.1-1.5 c0.4-0.7,1-1.3,1.6-1.8C236.2,12.4,236.2,12.9,236.4,13.5z M239.3,26.8c1,0.4,2,0.8,3.1,0.9c0.2,0,0.3,0.1,0.5,0.1 c-0.3,0.1-0.5,0.2-0.8,0.2c-0.3,0-0.5-0.1-0.8-0.1c-0.7-0.1-1.5-0.4-2.2-0.7C239.2,27.1,239.2,27,239.3,26.8z M245.6,25.7 c0.2-0.3,0.3-0.6,0.5-0.9c0.2-0.4,0.3-0.8,0.5-1.2c1.3,0.1,2.4,0,3.4-0.4c-0.1,0.3-0.2,0.6-0.3,0.9c-0.2,0.4-0.4,0.8-0.6,1.1 C248,25.6,246.9,25.8,245.6,25.7z M250,24.3c0.2-0.4,0.3-0.8,0.5-1.3c0.2-0.1,0.5-0.3,0.7-0.4c-0.3,0.7-0.7,1.3-1.1,1.9 c-0.1,0.1-0.1,0.1-0.2,0.2C249.9,24.5,250,24.4,250,24.3z M250.7,22.3c0.1-0.8,0.2-1.5,0.1-2.3c0.5-0.3,0.9-0.6,1.2-1 c0,0.1,0,0.2,0,0.3c0,0.6-0.1,1.3-0.3,1.8C251.5,21.5,251.2,21.9,250.7,22.3z"/> </g> <g> <path fill="#0095AA" d="M297.9,7.6h4.5v0.8h-3.5V11h2.9v0.8h-2.9v3.5h-1V7.6z"/> <path fill="#0095AA" d="M303.7,7.6h2.4c1.6,0,2.7,0.6,2.7,2.2c0,1.2-0.7,1.9-1.7,2.2l2,3.4H308l-1.9-3.3h-1.4v3.3h-1V7.6z M306,11.2 c1.2,0,1.9-0.5,1.9-1.5c0-1-0.7-1.4-1.9-1.4h-1.3v2.9H306z"/> <path fill="#0095AA" d="M309.9,11.4c0-2.5,1.4-4,3.3-4c1.9,0,3.3,1.5,3.3,4c0,2.5-1.4,4-3.3,4C311.2,15.5,309.9,13.9,309.9,11.4z M315.5,11.4c0-1.9-0.9-3.1-2.3-3.1c-1.4,0-2.3,1.2-2.3,3.1c0,1.9,0.9,3.2,2.3,3.2C314.6,14.6,315.5,13.3,315.5,11.4z"/> <path fill="#0095AA" d="M318.1,7.6h1.2l1.5,4.1c0.2,0.5,0.4,1,0.5,1.6h0c0.2-0.6,0.3-1.1,0.5-1.6l1.5-4.1h1.2v7.7h-0.9V11 c0-0.7,0.1-1.6,0.1-2.3h0l-0.6,1.8l-1.5,4H321l-1.4-4L319,8.7h0c0.1,0.7,0.1,1.6,0.1,2.3v4.3h-0.9V7.6z"/> <path fill="#0095AA" d="M330.7,8.4h-2.3V7.6h5.7v0.8h-2.3v6.9h-1V8.4z"/> <path fill="#0095AA" d="M335.4,7.6h1v3.2h3.6V7.6h1v7.7h-1v-3.6h-3.6v3.6h-1V7.6z"/> <path fill="#0095AA" d="M343.1,7.6h4.5v0.8h-3.5v2.4h2.9v0.8h-2.9v2.8h3.6v0.8h-4.6V7.6z"/> <path fill="#0095AA" d="M351.7,7.6h1.2l1.5,4.1c0.2,0.5,0.4,1,0.5,1.6h0c0.2-0.6,0.3-1.1,0.5-1.6l1.5-4.1h1.2v7.7h-0.9V11 c0-0.7,0.1-1.6,0.1-2.3h0l-0.6,1.8l-1.5,4h-0.7l-1.4-4l-0.6-1.8h0c0.1,0.7,0.1,1.6,0.1,2.3v4.3h-0.9V7.6z"/> <path fill="#0095AA" d="M361.8,7.6h1.1l2.6,7.7h-1.1l-0.7-2.3H361l-0.7,2.3h-1L361.8,7.6z M361.2,12.2h2.3l-0.4-1.2 c-0.3-0.9-0.5-1.7-0.8-2.6h0c-0.2,0.9-0.5,1.7-0.8,2.6L361.2,12.2z"/> <path fill="#0095AA" d="M366.7,7.6h1v3.9h0l3.2-3.9h1.1l-2.4,2.9l2.8,4.8h-1.1l-2.3-4l-1.3,1.6v2.4h-1V7.6z"/> <path fill="#0095AA" d="M373,7.6h4.5v0.8H374v2.4h2.9v0.8H374v2.8h3.6v0.8H373V7.6z"/> <path fill="#0095AA" d="M379.2,7.6h2.4c1.6,0,2.7,0.6,2.7,2.2c0,1.2-0.7,1.9-1.7,2.2l2,3.4h-1.1l-1.9-3.3h-1.4v3.3h-1V7.6z M381.5,11.2c1.2,0,1.9-0.5,1.9-1.5c0-1-0.7-1.4-1.9-1.4h-1.3v2.9H381.5z"/> <path fill="#0095AA" d="M385.4,14.3l0.6-0.6c0.6,0.6,1.4,0.9,2.2,0.9c1,0,1.6-0.5,1.6-1.3c0-0.8-0.6-1-1.3-1.4l-1.1-0.5 c-0.7-0.3-1.6-0.8-1.6-2c0-1.2,1-2.1,2.4-2.1c0.9,0,1.7,0.4,2.3,0.9L390,9c-0.5-0.4-1.1-0.7-1.7-0.7c-0.9,0-1.4,0.4-1.4,1.1 c0,0.7,0.7,1,1.3,1.3l1.1,0.5c0.9,0.4,1.6,0.9,1.6,2.1c0,1.2-1,2.2-2.6,2.2C387,15.5,386.1,15,385.4,14.3z"/> <path fill="#0095AA" d="M393.7,11.4c0-2.5,1.4-4,3.3-4c1.9,0,3.3,1.5,3.3,4c0,2.5-1.4,4-3.3,4C395.1,15.5,393.7,13.9,393.7,11.4z M399.3,11.4c0-1.9-0.9-3.1-2.3-3.1c-1.4,0-2.3,1.2-2.3,3.1c0,1.9,0.9,3.2,2.3,3.2C398.4,14.6,399.3,13.3,399.3,11.4z"/> <path fill="#0095AA" d="M402,7.6h4.5v0.8H403V11h2.9v0.8H403v3.5h-1V7.6z"/> <path fill="#0095AA" d="M410.1,7.6h1.7l1.3,3.8c0.2,0.5,0.3,0.9,0.4,1.5h0c0.1-0.6,0.3-1,0.4-1.5l1.3-3.8h1.7v7.7h-1.3v-3.5 c0-0.7,0.1-1.8,0.2-2.5h0l-0.6,1.9l-1.3,3.4H413l-1.2-3.4l-0.6-1.9h0c0.1,0.7,0.2,1.8,0.2,2.5v3.5h-1.3V7.6z"/> <path fill="#0095AA" d="M420.2,7.6h1.7l2.5,7.7h-1.5l-0.6-2.1h-2.6l-0.6,2.1h-1.4L420.2,7.6z M420,12.2h1.9l-0.3-0.9 c-0.2-0.8-0.5-1.7-0.7-2.5h0c-0.2,0.8-0.4,1.7-0.7,2.5L420,12.2z"/> <path fill="#0095AA" d="M425.6,8.8h-2.2V7.6h5.8v1.2H427v6.5h-1.4V8.8z"/> <path fill="#0095AA" d="M430,7.6h1.4v3.1h3.1V7.6h1.4v7.7h-1.4v-3.4h-3.1v3.4H430V7.6z"/> <path fill="#0095AA" d="M437.4,7.6h4.7v1.2h-3.3v1.9h2.8v1.2h-2.8v2.2h3.4v1.2h-4.8V7.6z"/> <path fill="#0095AA" d="M443.3,7.6h1.7l1.3,3.8c0.2,0.5,0.3,0.9,0.4,1.5h0c0.1-0.6,0.3-1,0.4-1.5l1.3-3.8h1.7v7.7h-1.3v-3.5 c0-0.7,0.1-1.8,0.2-2.5h0l-0.6,1.9l-1.3,3.4h-0.9l-1.2-3.4l-0.6-1.9h0c0.1,0.7,0.2,1.8,0.2,2.5v3.5h-1.3V7.6z"/> <path fill="#0095AA" d="M453.3,7.6h1.7l2.5,7.7H456l-0.6-2.1h-2.6l-0.6,2.1h-1.4L453.3,7.6z M453.2,12.2h1.9l-0.3-0.9 c-0.2-0.8-0.5-1.7-0.7-2.5h0c-0.2,0.8-0.4,1.7-0.7,2.5L453.2,12.2z"/> <path fill="#0095AA" d="M459,8.8h-2.2V7.6h5.8v1.2h-2.2v6.5H459V8.8z"/> <path fill="#0095AA" d="M463.7,7.6h1.4v7.7h-1.4V7.6z"/> <path fill="#0095AA" d="M466.4,11.5c0-2.5,1.6-4,3.5-4c1,0,1.7,0.4,2.2,1l-0.7,0.9c-0.4-0.4-0.9-0.6-1.5-0.6c-1.2,0-2.1,1-2.1,2.8 c0,1.7,0.8,2.8,2.1,2.8c0.7,0,1.2-0.3,1.6-0.7l0.8,0.8c-0.6,0.7-1.5,1.1-2.4,1.1C467.9,15.5,466.4,14,466.4,11.5z"/> <path fill="#0095AA" d="M474.8,7.6h1.7l2.5,7.7h-1.5l-0.6-2.1h-2.6l-0.6,2.1h-1.4L474.8,7.6z M474.7,12.2h1.9l-0.3-0.9 c-0.2-0.8-0.5-1.7-0.7-2.5h0c-0.2,0.8-0.4,1.7-0.7,2.5L474.7,12.2z"/> <path fill="#0095AA" d="M299.5,20.7h1.1l2.6,7.7h-1.1l-0.7-2.3h-2.8l-0.7,2.3h-1L299.5,20.7z M298.9,25.3h2.3l-0.4-1.2 c-0.3-0.9-0.5-1.7-0.8-2.6h0c-0.2,0.9-0.5,1.7-0.8,2.6L298.9,25.3z"/> <path fill="#0095AA" d="M304.1,20.7h1.1l2.8,4.8c0.3,0.5,0.6,1.1,0.8,1.7h0c-0.1-0.8-0.1-1.7-0.1-2.5v-4h0.9v7.7h-1.1l-2.8-4.8 c-0.3-0.5-0.6-1.1-0.8-1.7h0c0.1,0.8,0.1,1.6,0.1,2.4v4.1h-0.9V20.7z"/> <path fill="#0095AA" d="M311.4,20.7h1.9c2.4,0,3.7,1.4,3.7,3.8c0,2.5-1.3,3.9-3.6,3.9h-2V20.7z M313.3,27.6c1.8,0,2.7-1.1,2.7-3.1 c0-1.9-0.9-3-2.7-3h-0.9v6.1H313.3z"/> <path fill="#0095AA" d="M320.4,20.6l1.4,0l0.6,3.9c0.1,0.8,0.2,1.6,0.3,2.5l0,0c0.2-0.9,0.3-1.7,0.5-2.5l1-3.9l1.3,0l0.9,3.9 c0.2,0.8,0.3,1.6,0.5,2.5l0,0c0.1-0.9,0.2-1.7,0.4-2.5l0.7-3.9l1.3,0l-1.6,7.7l-1.8,0l-0.8-4.1c-0.1-0.6-0.2-1.2-0.3-1.9l0,0 c-0.1,0.7-0.2,1.2-0.3,1.9l-0.9,4l-1.8,0L320.4,20.6z"/> <path fill="#0095AA" d="M329.8,24.5c0-2.5,1.5-3.9,3.5-3.9c2,0,3.4,1.5,3.3,4c0,2.5-1.5,4-3.5,4C331.2,28.5,329.8,27,329.8,24.5z M335.2,24.6c0-1.7-0.7-2.7-1.9-2.8c-1.2,0-2,1-2,2.7c0,1.7,0.7,2.8,1.9,2.9C334.4,27.4,335.2,26.3,335.2,24.6z"/> <path fill="#0095AA" d="M337.8,20.7l1.4,0l-0.1,6.5l3.2,0.1l0,1.2l-4.6-0.1L337.8,20.7z"/> <path fill="#0095AA" d="M343.4,20.7l4.7,0.1l0,1.2l-3.3-0.1l0,2.2l2.8,0l0,1.2l-2.8,0l-0.1,3.2l-1.4,0L343.4,20.7z"/> <path fill="#0095AA" d="M349,20.7l2.6,0c1.6,0,2.8,0.6,2.8,2.3c0,1.2-0.6,1.9-1.6,2.2l1.8,3.2l-1.6,0l-1.6-3l-1.1,0l-0.1,3l-1.4,0 L349,20.7z M351.4,24.3c1,0,1.6-0.4,1.6-1.3c0-0.9-0.5-1.2-1.6-1.2l-1.1,0l0,2.5L351.4,24.3z"/> <path fill="#0095AA" d="M357.4,20.7l1.7,0l2.4,7.8l-1.5,0l-0.6-2.1l-2.6,0l-0.6,2.1l-1.4,0L357.4,20.7z M357.2,25.2l1.9,0l-0.2-0.9 c-0.2-0.8-0.4-1.7-0.7-2.5l0,0c-0.2,0.8-0.5,1.7-0.7,2.5L357.2,25.2z"/> <path fill="#0095AA" d="M362.5,20.6l1.7,0l1.3,3.8c0.2,0.5,0.3,0.9,0.4,1.5l0,0c0.2-0.6,0.3-1,0.5-1.5l1.4-3.8l1.7,0l-0.1,7.7l-1.3,0 l0.1-3.5c0-0.7,0.1-1.8,0.3-2.5l0,0l-0.6,1.9l-1.3,3.4l-0.9,0l-1.2-3.5l-0.6-1.9l0,0c0.1,0.7,0.2,1.8,0.2,2.5l-0.1,3.5l-1.3,0 L362.5,20.6z"/> <path fill="#0095AA" d="M370.8,19.1l0.9,0L371.5,30l-0.9,0L370.8,19.1z"/> <path fill="#0095AA" d="M375.1,20.7l1.7,0l2.4,7.8l-1.5,0l-0.6-2.1l-2.6,0l-0.6,2.1l-1.4,0L375.1,20.7z M374.8,25.2l1.9,0l-0.2-0.9 c-0.2-0.8-0.4-1.7-0.7-2.5l0,0c-0.2,0.8-0.5,1.7-0.7,2.5L374.8,25.2z"/> <path fill="#0095AA" d="M379.9,20.7l1.4,0l-0.1,6.5l3.2,0.1l0,1.2l-4.6-0.1L379.9,20.7z"/> <path fill="#0095AA" d="M385.6,20.7l2.4,0c1.7,0,3,0.7,3,2.4c0,1.7-1.3,2.5-3,2.4l-1.1,0l0,2.8l-1.4,0L385.6,20.7z M387.9,24.5 c1.1,0,1.7-0.4,1.7-1.4c0-0.9-0.6-1.3-1.7-1.3l-0.9,0l0,2.7L387.9,24.5z"/> <path fill="#0095AA" d="M392,20.6l1.4,0l-0.1,3.1l3.1,0.1l0.1-3.1l1.4,0l-0.1,7.7l-1.4,0l0.1-3.4l-3.1-0.1l-0.1,3.4l-1.4,0L392,20.6z "/> <path fill="#0095AA" d="M401,20.7l1.7,0l2.4,7.8l-1.5,0l-0.6-2.1l-2.6,0l-0.6,2.1l-1.4,0L401,20.7z M400.8,25.2l1.9,0l-0.2-0.9 c-0.2-0.8-0.4-1.7-0.7-2.5l0,0c-0.2,0.8-0.5,1.7-0.7,2.5L400.8,25.2z"/> </g> </g> <a href="https://www.wolfram.com/mathematica/"><rect x="409" y="5.9" style="fill:#ffffff00;" width="70" height="11.6"/></a> <a href="https://wolframalpha.com/"><rect x="319.6" y="18.2" style="fill:#ffffff00;" width="86.9" height="11.6"/></a> <a href="/"><rect y="0.1" style="fill:#ffffff00;" width="292.4" height="29.9"/></a> </svg> <svg version="1.1" id="logo-600" class="hide show__600" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" x="0px" y="0px" viewBox="0 0 480.7 30" style="enable-background:new 0 0 480.7 30;" xml:space="preserve"> <g> <g> <g> <polygon fill="#0095AA" points="145.2,17.1 138.8,3.9 134.2,3.9 134.2,28.5 137.5,28.5 137.5,8.6 144,21.8 144,21.9 146.2,21.9 152.7,8.6 152.7,28.5 156,28.5 156,3.9 151.6,3.9"/> <path fill="#0095AA" d="M171.8,10.8c-1.2-1-3.1-1.5-5.8-1.5c-1.7,0-3.2,0.3-4.3,0.8c-1.2,0.6-2.1,1.4-2.6,2.4l0,0.1l2.6,1.6l0-0.1 c0.3-0.5,0.8-1,1.4-1.4c0.7-0.4,1.6-0.6,2.8-0.6c1.4,0,2.5,0.3,3.2,0.8c0.8,0.5,1.1,1.4,1.1,2.8v0.8l-4.5,0.4 c-1.8,0.2-3.2,0.6-4.1,1.1c-1,0.5-1.7,1.2-2.2,2c-0.5,0.8-0.8,1.9-0.8,3.2c0,1.7,0.5,3.1,1.5,4.2c1,1.1,2.4,1.6,4.1,1.6 c1.2,0,2.3-0.3,3.3-0.8c0.9-0.5,1.8-1.2,2.7-1.9v2.2h3.2V15.9C173.6,13.5,173,11.8,171.8,10.8z M170.4,19.1v4.4 c-0.4,0.3-0.8,0.6-1.2,0.9c-0.4,0.3-0.8,0.6-1.2,0.9c-0.4,0.2-0.9,0.5-1.3,0.6c-0.4,0.2-0.9,0.2-1.3,0.2c-1.1,0-1.9-0.2-2.4-0.7 c-0.5-0.5-0.8-1.2-0.8-2.3c0-1.1,0.4-2,1.2-2.6c0.8-0.6,2.2-1,4.2-1.2L170.4,19.1z"/> <path fill="#0095AA" d="M185.9,25.8c-0.7,0.3-1.6,0.5-2.4,0.5c-1,0-1.6-0.3-1.9-0.9c-0.3-0.6-0.4-1.7-0.4-3.2v-9.7h4.7V9.8h-4.7V4.7 h-3.2v5.1h-2.6v2.7h2.6v10.3c0,2.1,0.4,3.7,1.2,4.7c0.8,1,2.2,1.5,4.1,1.5c1.2,0,2.3-0.2,3.5-0.6l0.1,0L185.9,25.8L185.9,25.8z" /> <path fill="#0095AA" d="M199.1,9.3c-1.2,0-2.3,0.3-3.5,1c-1.1,0.6-2,1.3-2.9,2.1V2.1h-3.2v26.4h3.2V15.4c0.9-0.8,1.9-1.5,2.9-2.1 c1-0.6,1.9-0.9,2.7-0.9c0.8,0,1.3,0.1,1.7,0.4c0.4,0.3,0.7,0.7,0.8,1.2c0.2,0.6,0.3,1.7,0.3,3.5v11h3.2V16.1 c0-2.4-0.4-4.2-1.3-5.2C202.2,9.8,200.9,9.3,199.1,9.3z"/> <polygon fill="#0095AA" points="226.2,23.5 221.6,4 221.6,3.9 217.8,3.9 213.2,23.3 208.8,4 208.8,3.9 205.3,3.9 211.1,28.4 211.1,28.5 215.1,28.5 219.6,9.3 224.1,28.4 224.1,28.5 228.2,28.5 234.1,3.9 230.7,3.9 "/> <path fill="#0095AA" d="M265.2,9.6c-1.2,0-2.2,0.3-3.2,1c-0.9,0.6-1.7,1.3-2.5,2.1V9.8h-3.2v18.7h3.2V15.7c1.1-1.1,2.1-1.8,2.9-2.3 c0.8-0.4,1.7-0.6,2.6-0.6c0.6,0,1.1,0.1,1.4,0.2l0.1,0l0.7-3.1l-0.1,0C266.6,9.7,265.9,9.6,265.2,9.6z"/> <rect x="270" y="2.1" fill="#0095AA" width="3.2" height="26.4"/> <path fill="#0095AA" d="M288.6,2.1v9.2c-1.5-1.3-3.2-1.9-5-1.9c-2.3,0-4.2,0.9-5.5,2.7c-1.3,1.8-2,4.3-2,7.3c0,3.1,0.6,5.5,1.8,7.2 c1.2,1.7,3,2.5,5.2,2.5c1.1,0,2.2-0.2,3.2-0.7c0.9-0.4,1.7-0.9,2.4-1.6v1.7h3.2V2.1H288.6z M288.6,14.1v9.7 c-0.6,0.6-1.4,1.1-2.2,1.6c-0.9,0.5-1.8,0.7-2.7,0.7c-2.9,0-4.3-2.3-4.3-6.9c0-2.4,0.4-4.2,1.3-5.4c0.9-1.1,2-1.7,3.3-1.7 C285.5,12.2,287,12.8,288.6,14.1z"/> </g> <g> <polygon fill="#666666" points="30,3.2 26.4,3.2 22,22.5 17.5,3.4 17.5,3.2 13.5,3.2 9,22.4 4.7,3.2 1,3.2 6.8,28 6.8,28.2 11,28.2 15.4,9.2 19.8,28 19.8,28.2 24,28.2 30,3.5"/> <path fill="#666666" d="M38,8.7c-2.7,0-4.8,0.8-6.2,2.5c-1.4,1.7-2.1,4.2-2.1,7.6c0,3.3,0.7,5.8,2.1,7.5c1.4,1.7,3.5,2.5,6.2,2.5 c2.7,0,4.8-0.9,6.2-2.6c1.4-1.7,2.1-4.2,2.1-7.5c0-3.3-0.7-5.8-2.1-7.5C42.8,9.5,40.7,8.7,38,8.7z M41.5,24 c-0.8,1.1-1.9,1.7-3.6,1.7c-1.7,0-2.9-0.5-3.7-1.7c-0.8-1.1-1.2-2.9-1.2-5.3c0-2.5,0.4-4.3,1.2-5.4c0.8-1.1,2-1.6,3.6-1.6 c1.6,0,2.8,0.5,3.5,1.6c0.8,1.1,1.2,2.9,1.2,5.4C42.7,21.1,42.3,22.9,41.5,24z"/> <rect x="49.7" y="1.4" fill="#666666" width="3.4" height="26.8"/> <path fill="#666666" d="M67.9,1.5c-1.1-0.5-2.3-0.7-3.6-0.7c-2.2,0-3.7,0.6-4.6,1.7c-0.9,1.1-1.3,2.8-1.3,5.1v1.6h-2.7v3h2.7v16.1 h3.4V12.2h4.1v-3h-4.1V7.6c0-1.5,0.2-2.5,0.6-3c0.4-0.5,1-0.7,2-0.7c0.4,0,0.8,0.1,1.3,0.2c0.5,0.1,0.9,0.3,1.2,0.4l0.2,0.1l1-3 L67.9,1.5z"/> <path fill="#666666" d="M77.3,8.9c-1.2,0-2.3,0.4-3.2,1c-0.8,0.6-1.6,1.2-2.3,2V9.2h-3.4v19h3.4v-13c1.1-1.1,2-1.8,2.8-2.2 c0.8-0.4,1.7-0.6,2.5-0.6c0.6,0,1,0.1,1.3,0.2l0.2,0.1l0.7-3.3l-0.1-0.1C78.7,9,78.1,8.9,77.3,8.9z"/> <path fill="#666666" d="M93.3,10.2c-1.2-1-3.1-1.5-5.8-1.5c-1.7,0-3.2,0.3-4.4,0.8c-1.2,0.6-2.1,1.4-2.7,2.5l-0.1,0.2l2.8,1.7 l0.1-0.2c0.3-0.5,0.7-0.9,1.4-1.3c0.6-0.4,1.6-0.6,2.8-0.6c1.3,0,2.4,0.3,3.2,0.7c0.7,0.5,1.1,1.4,1.1,2.8v0.7l-4.4,0.4 c-1.8,0.2-3.2,0.6-4.2,1.1c-1,0.5-1.7,1.2-2.2,2.1c-0.5,0.9-0.8,2-0.8,3.3c0,1.7,0.5,3.2,1.5,4.3c1,1.1,2.4,1.7,4.2,1.7 c1.2,0,2.3-0.3,3.3-0.8c0.8-0.5,1.7-1.1,2.5-1.8v2.1h3.4V15.4C95.1,12.9,94.5,11.2,93.3,10.2z M86.8,25.6c-1,0-1.8-0.2-2.3-0.7 c-0.5-0.4-0.8-1.2-0.8-2.2c0-1.1,0.4-1.9,1.1-2.5c0.8-0.6,2.2-1,4.1-1.1l2.7-0.3V23c-0.4,0.3-0.7,0.6-1.1,0.9 c-0.4,0.3-0.8,0.6-1.2,0.9c-0.4,0.2-0.9,0.5-1.3,0.6C87.7,25.5,87.2,25.6,86.8,25.6z"/> <path fill="#666666" d="M123,11.6c-0.3-0.9-0.9-1.7-1.6-2.2c-0.7-0.5-1.7-0.8-2.8-0.8c-1.3,0-2.4,0.4-3.4,1.1 c-0.9,0.6-1.8,1.4-2.7,2.3c-0.3-1.1-0.8-2-1.5-2.5c-0.8-0.6-1.8-0.9-3.1-0.9c-1.2,0-2.3,0.3-3.3,1c-0.8,0.6-1.6,1.2-2.4,2V9.2 h-3.4v19h3.4V14.9c0.9-0.9,1.8-1.7,2.7-2.2c0.8-0.5,1.6-0.8,2.2-0.8c0.7,0,1.2,0.1,1.5,0.3c0.3,0.2,0.5,0.6,0.6,1.2 c0.1,0.6,0.2,1.8,0.2,3.5v11.2h3.4V14.9c1.2-1.1,2.2-1.9,2.9-2.3c0.7-0.4,1.4-0.6,2-0.6c0.7,0,1.2,0.1,1.5,0.3 c0.3,0.2,0.5,0.6,0.7,1.1c0.1,0.6,0.2,1.8,0.2,3.6v11.2h3.4V15.6C123.5,13.9,123.3,12.5,123,11.6z"/> </g> <path fill="#0095AA" d="M243.6,8.3c-5.8,0-10.5,4.7-10.5,10.5s4.7,10.5,10.5,10.5c5.8,0,10.5-4.7,10.5-10.5S249.4,8.3,243.6,8.3z M236.7,23.9c0-0.5,0.1-1,0.2-1.6c1.1,0.9,2.3,1.7,3.7,2.4L240,26C238.8,25.5,237.6,24.7,236.7,23.9z M239.8,26.5l-0.2,0.5 c-0.9-0.4-1.8-1-2.5-1.6c-0.2-0.2-0.3-0.5-0.3-0.8C237.6,25.4,238.7,26,239.8,26.5z M236.1,23.4c-0.8-0.8-1.4-1.6-1.6-2.4 c-0.1-0.5-0.1-1.1-0.1-1.6c0.4,0.8,1.1,1.7,2,2.5C236.3,22.4,236.2,22.9,236.1,23.4z M236.2,24.5L236.2,24.5 c-0.3-0.4-0.6-0.8-0.8-1.2c0.2,0.2,0.5,0.5,0.7,0.7C236.2,24.3,236.2,24.4,236.2,24.5z M234.4,17.4c0-0.1,0-0.1,0-0.2 c0.1-0.7,0.4-1.5,0.7-2.2c0-0.1,0-0.1,0.1-0.2c0,0.3,0.1,0.6,0.2,0.9c-0.3,0.4-0.5,0.8-0.7,1.2C234.5,17.1,234.5,17.3,234.4,17.4z M234.6,18.4c0.1-0.4,0.2-0.8,0.4-1.2c0.1-0.3,0.3-0.6,0.5-0.9c0.4,0.9,1.1,1.9,2.1,2.8c-0.2,0.4-0.4,0.8-0.6,1.2 c-0.1,0.3-0.3,0.6-0.4,0.9C235.6,20.4,235,19.4,234.6,18.4z M251.7,15.2c-0.1,0.4-0.3,0.8-0.8,1c-0.3-0.8-0.8-1.6-1.3-2.4 c0.2-0.1,0.3-0.3,0.4-0.5C250.7,13.9,251.3,14.5,251.7,15.2z M250.2,12.3c0.4,0.2,0.7,0.5,1,0.8c0.3,0.4,0.4,0.7,0.5,1 c0,0,0,0.1,0,0.1c-0.4-0.5-0.9-1-1.4-1.5C250.2,12.7,250.2,12.5,250.2,12.3C250.2,12.4,250.2,12.3,250.2,12.3z M252.8,17.8 c-0.1,0.6-0.5,1.1-1.1,1.5c-0.1-0.8-0.3-1.7-0.6-2.5c0.4-0.2,0.7-0.6,0.9-0.9C252.4,16.5,252.7,17.1,252.8,17.8z M252.3,15.2 C252.3,15.2,252.3,15.2,252.3,15.2C252.3,15.2,252.3,15.2,252.3,15.2C252.3,15.2,252.3,15.2,252.3,15.2z M240.2,16.5 c0.6-0.7,1.2-1.3,1.8-1.9c0.7,0.6,1.5,1.1,2.5,1.6l-1.1,2.4C242.2,18,241.1,17.3,240.2,16.5z M243.2,19.1l-1.1,2.4 c-1.4-0.7-2.7-1.5-3.7-2.4c0.4-0.7,0.9-1.4,1.5-2.1C240.8,17.8,242,18.5,243.2,19.1z M245,16.4c0.8,0.3,1.5,0.6,2.3,0.7 c0.2,0,0.4,0.1,0.6,0.1c0,0.9-0.1,1.8-0.2,2.6c-0.3,0-0.6-0.1-0.9-0.1c-1-0.2-2-0.5-3-0.9C244.3,18,244.7,17.2,245,16.4z M247.7,14.2c0.1,0.8,0.2,1.6,0.3,2.4c-0.2,0-0.4-0.1-0.5-0.1c-0.7-0.1-1.4-0.4-2.1-0.7c0.3-0.7,0.6-1.5,0.9-2.1 c0.4,0.2,0.8,0.3,1.2,0.4C247.5,14.1,247.6,14.2,247.7,14.2z M247.6,12.2c0.5,0.4,0.9,0.9,1.3,1.4c-0.2,0.1-0.5,0.1-0.8,0.1 C248,13.1,247.8,12.6,247.6,12.2z M246,13.1c-0.3-0.2-0.7-0.4-1-0.6c0.5-0.3,1.1-0.6,1.6-0.7L246,13.1z M245.7,13.6l-1,2.1 c-0.8-0.4-1.6-0.9-2.3-1.4c0.7-0.6,1.3-1,2-1.5C244.9,13.1,245.3,13.3,245.7,13.6z M242.1,13.9c-0.6-0.6-1-1.1-1.2-1.7 c0.8-0.3,1.7-0.5,2.6-0.7c0.1,0.3,0.3,0.6,0.6,0.9C243.5,12.8,242.8,13.3,242.1,13.9z M243.3,11c-0.9,0.1-1.8,0.3-2.6,0.6 c-0.1-0.5,0-0.9,0.2-1.3c0.8-0.1,1.6-0.1,2.4,0C243.3,10.6,243.3,10.8,243.3,11z M241.7,14.2c-0.7,0.6-1.3,1.2-1.9,1.9 c-0.8-0.8-1.4-1.6-1.7-2.4c0.7-0.5,1.5-0.9,2.3-1.3C240.6,13,241.1,13.6,241.7,14.2z M240.2,11.9c-0.8,0.3-1.6,0.8-2.3,1.2 c-0.2-0.7,0-1.4,0.4-1.9c0.6-0.3,1.3-0.6,2-0.8C240.1,10.9,240.1,11.4,240.2,11.9z M239.4,16.6c-0.6,0.7-1.1,1.4-1.5,2.1 c-1-0.9-1.7-1.9-2-2.9c0.5-0.6,1-1.2,1.7-1.8C237.9,14.9,238.6,15.8,239.4,16.6z M238,19.6c1.1,0.9,2.4,1.8,3.8,2.4l-1,2.1 c-1.4-0.7-2.7-1.5-3.8-2.4c0.1-0.3,0.3-0.7,0.4-1.1C237.7,20.3,237.8,20,238,19.6z M241.2,24.9c1.2,0.5,2.4,0.9,3.5,1.1 c0.3,0.1,0.6,0.1,0.9,0.1c-0.3,0.5-0.7,0.9-1.1,1.2c-0.3,0-0.7-0.1-1-0.1c-1-0.2-2-0.5-3-0.9C240.7,25.9,240.9,25.5,241.2,24.9z M244.7,27.9c0.3,0,0.6,0,0.9,0c-0.4,0.1-0.9,0.2-1.3,0.2C244.5,28,244.6,28,244.7,27.9z M245.3,27.4c0.3-0.3,0.7-0.7,1-1.2 c1.1,0.1,2.2,0,3-0.2c-0.4,0.4-0.8,0.7-1.2,1C247.3,27.3,246.4,27.4,245.3,27.4z M245.9,25.6c-0.4,0-0.7-0.1-1.1-0.2 c-1.1-0.2-2.3-0.6-3.4-1.1c0.1-0.3,0.3-0.6,0.5-1l0.5-1.1c1.2,0.5,2.4,0.9,3.5,1.1c0.3,0.1,0.7,0.1,1,0.2 c-0.1,0.4-0.3,0.7-0.4,1.1C246.3,25,246.1,25.3,245.9,25.6z M246.1,22.8c-1.1-0.2-2.3-0.6-3.4-1.1c0.4-0.8,0.7-1.6,1.1-2.4 c1,0.4,2.1,0.8,3.1,1c0.3,0.1,0.6,0.1,0.9,0.1c-0.1,0.9-0.3,1.7-0.6,2.5C246.8,22.9,246.4,22.9,246.1,22.8z M248.3,20.5 c1.1,0.1,2.2,0,3-0.4c0,0.8,0,1.7-0.2,2.4c-0.9,0.4-2,0.5-3.4,0.5C248,22.2,248.1,21.4,248.3,20.5z M248.4,19.9 c0.1-0.9,0.2-1.8,0.1-2.6c0.8,0,1.6,0,2.2-0.3c0.3,0.8,0.5,1.7,0.5,2.5C250.5,19.8,249.5,20,248.4,19.9z M250.5,16.4 c-0.5,0.2-1.2,0.3-2,0.2c0-0.9-0.1-1.7-0.3-2.5c0.4,0,0.7,0,1-0.1C249.8,14.8,250.2,15.6,250.5,16.4z M249.4,13.4 c-0.3-0.4-0.7-0.8-1.1-1.2c0.5,0.3,0.9,0.5,1.3,0.9C249.6,13.2,249.5,13.3,249.4,13.4z M248.4,11.7c0.4,0.1,0.7,0.2,1,0.3 c0.1,0.2,0.2,0.3,0.2,0.5C249.2,12.1,248.8,11.9,248.4,11.7z M247.7,11.1c0.2-0.1,0.4-0.2,0.5-0.2c0.2,0.1,0.3,0.2,0.5,0.4 C248.4,11.2,248.1,11.2,247.7,11.1z M247.2,10.9c0-0.2-0.1-0.5-0.1-0.7c0.2,0.1,0.5,0.2,0.7,0.3C247.6,10.7,247.4,10.8,247.2,10.9 z M247.6,13.6c0,0-0.1,0-0.1,0c-0.3-0.1-0.7-0.2-1-0.3c0.2-0.5,0.4-1,0.6-1.4C247.2,12.4,247.4,13,247.6,13.6z M245.8,10 c0.1,0,0.2,0,0.3,0.1c0.1,0,0.2,0,0.3,0.1c0.1,0.1,0.2,0.3,0.2,0.6C246.4,10.4,246.1,10.2,245.8,10z M246,11.4 c-0.5,0.2-0.9,0.4-1.4,0.7c-0.2-0.2-0.4-0.5-0.5-0.7C244.7,11.4,245.4,11.4,246,11.4z M245.6,10.9c-0.6,0-1.1,0-1.7,0 c0-0.2,0-0.3,0.1-0.5C244.5,10.6,245.1,10.7,245.6,10.9z M244.4,10.1c0.1-0.1,0.3-0.1,0.4-0.1c0.3,0.1,0.6,0.3,0.9,0.5 C245.3,10.3,244.9,10.2,244.4,10.1z M243.7,9.9c-0.5-0.1-1-0.1-1.5-0.1c-0.2,0-0.4,0-0.5,0c0.3-0.2,0.7-0.3,1.1-0.4 c0.5,0,0.9,0,1.4,0.2C243.9,9.7,243.8,9.8,243.7,9.9z M237.4,13.5c-0.6,0.5-1.2,1.1-1.7,1.7c-0.1-0.6-0.1-1.1,0.1-1.5 c0.4-0.7,1-1.3,1.6-1.8C237.2,12.4,237.2,12.9,237.4,13.5z M240.3,26.8c1,0.4,2,0.8,3.1,0.9c0.2,0,0.3,0.1,0.5,0.1 c-0.3,0.1-0.5,0.2-0.8,0.2c-0.3,0-0.5-0.1-0.8-0.1c-0.7-0.1-1.5-0.4-2.2-0.7C240.1,27.1,240.2,27,240.3,26.8z M246.6,25.7 c0.2-0.3,0.3-0.6,0.5-0.9c0.2-0.4,0.3-0.8,0.5-1.2c1.3,0.1,2.4,0,3.4-0.4c-0.1,0.3-0.2,0.6-0.3,0.9c-0.2,0.4-0.4,0.8-0.6,1.1 C249,25.6,247.9,25.8,246.6,25.7z M251,24.3c0.2-0.4,0.3-0.8,0.5-1.3c0.2-0.1,0.5-0.3,0.7-0.4c-0.3,0.7-0.7,1.3-1.1,1.9 c-0.1,0.1-0.1,0.1-0.2,0.2C250.9,24.5,251,24.4,251,24.3z M251.7,22.2c0.1-0.8,0.2-1.5,0.1-2.3c0.5-0.3,0.9-0.6,1.2-1 c0,0.1,0,0.2,0,0.3c0,0.6-0.1,1.3-0.3,1.8C252.5,21.5,252.2,21.9,251.7,22.2z"/> </g> <g> <path fill="#0095AA" d="M298.9,7.6h4.5v0.8h-3.5V11h2.9v0.8h-2.9v3.5h-1V7.6z"/> <path fill="#0095AA" d="M304.7,7.6h2.4c1.6,0,2.7,0.6,2.7,2.2c0,1.2-0.7,1.9-1.7,2.2l2,3.4H309l-1.9-3.3h-1.4v3.3h-1V7.6z M307,11.2 c1.2,0,1.9-0.5,1.9-1.5c0-1-0.7-1.4-1.9-1.4h-1.3v2.9H307z"/> <path fill="#0095AA" d="M310.9,11.4c0-2.5,1.4-4,3.3-4c1.9,0,3.3,1.5,3.3,4c0,2.5-1.4,4-3.3,4C312.2,15.4,310.9,13.9,310.9,11.4z M316.5,11.4c0-1.9-0.9-3.1-2.3-3.1c-1.4,0-2.3,1.2-2.3,3.1c0,1.9,0.9,3.2,2.3,3.2C315.6,14.6,316.5,13.3,316.5,11.4z"/> <path fill="#0095AA" d="M319.1,7.6h1.2l1.5,4.1c0.2,0.5,0.4,1,0.5,1.6h0c0.2-0.6,0.3-1.1,0.5-1.6l1.5-4.1h1.2v7.7h-0.9V11 c0-0.7,0.1-1.6,0.1-2.3h0l-0.6,1.8l-1.5,4H322l-1.4-4L320,8.7h0c0.1,0.7,0.1,1.6,0.1,2.3v4.3h-0.9V7.6z"/> <path fill="#0095AA" d="M331.7,8.4h-2.3V7.6h5.7v0.8h-2.3v6.9h-1V8.4z"/> <path fill="#0095AA" d="M336.4,7.6h1v3.2h3.6V7.6h1v7.7h-1v-3.6h-3.6v3.6h-1V7.6z"/> <path fill="#0095AA" d="M344.1,7.6h4.5v0.8h-3.5v2.4h2.9v0.8h-2.9v2.8h3.6v0.8h-4.6V7.6z"/> <path fill="#0095AA" d="M352.7,7.6h1.2l1.5,4.1c0.2,0.5,0.4,1,0.5,1.6h0c0.2-0.6,0.3-1.1,0.5-1.6l1.5-4.1h1.2v7.7h-0.9V11 c0-0.7,0.1-1.6,0.1-2.3h0l-0.6,1.8l-1.5,4h-0.7l-1.4-4l-0.6-1.8h0c0.1,0.7,0.1,1.6,0.1,2.3v4.3h-0.9V7.6z"/> <path fill="#0095AA" d="M362.8,7.6h1.1l2.6,7.7h-1.1l-0.7-2.3H362l-0.7,2.3h-1L362.8,7.6z M362.2,12.1h2.3l-0.4-1.2 c-0.3-0.9-0.5-1.7-0.8-2.6h0c-0.2,0.9-0.5,1.7-0.8,2.6L362.2,12.1z"/> <path fill="#0095AA" d="M367.7,7.6h1v3.9h0l3.2-3.9h1.1l-2.4,2.9l2.8,4.8h-1.1l-2.3-4l-1.3,1.6v2.4h-1V7.6z"/> <path fill="#0095AA" d="M374,7.6h4.5v0.8H375v2.4h2.9v0.8H375v2.8h3.6v0.8H374V7.6z"/> <path fill="#0095AA" d="M380.2,7.6h2.4c1.6,0,2.7,0.6,2.7,2.2c0,1.2-0.7,1.9-1.7,2.2l2,3.4h-1.1l-1.9-3.3h-1.4v3.3h-1V7.6z M382.5,11.2c1.2,0,1.9-0.5,1.9-1.5c0-1-0.7-1.4-1.9-1.4h-1.3v2.9H382.5z"/> <path fill="#0095AA" d="M386.4,14.3l0.6-0.6c0.6,0.6,1.4,0.9,2.2,0.9c1,0,1.6-0.5,1.6-1.3c0-0.8-0.6-1-1.3-1.4l-1.1-0.5 c-0.7-0.3-1.6-0.8-1.6-2c0-1.2,1-2.1,2.4-2.1c0.9,0,1.7,0.4,2.3,0.9L391,9c-0.5-0.4-1.1-0.7-1.7-0.7c-0.9,0-1.4,0.4-1.4,1.1 c0,0.7,0.7,1,1.3,1.3l1.1,0.5c0.9,0.4,1.6,0.9,1.6,2.1c0,1.2-1,2.2-2.6,2.2C388,15.4,387.1,15,386.4,14.3z"/> <path fill="#0095AA" d="M394.7,11.4c0-2.5,1.4-4,3.3-4c1.9,0,3.3,1.5,3.3,4c0,2.5-1.4,4-3.3,4C396.1,15.4,394.7,13.9,394.7,11.4z M400.3,11.4c0-1.9-0.9-3.1-2.3-3.1c-1.4,0-2.3,1.2-2.3,3.1c0,1.9,0.9,3.2,2.3,3.2C399.4,14.6,400.3,13.3,400.3,11.4z"/> <path fill="#0095AA" d="M403,7.6h4.5v0.8H404V11h2.9v0.8H404v3.5h-1V7.6z"/> <path fill="#0095AA" d="M411.1,7.6h1.7l1.3,3.8c0.2,0.5,0.3,0.9,0.4,1.5h0c0.1-0.6,0.3-1,0.4-1.5l1.3-3.8h1.7v7.7h-1.3v-3.5 c0-0.7,0.1-1.8,0.2-2.5h0l-0.6,1.9l-1.3,3.4H414l-1.2-3.4l-0.6-1.9h0c0.1,0.7,0.2,1.8,0.2,2.5v3.5h-1.3V7.6z"/> <path fill="#0095AA" d="M421.2,7.6h1.7l2.5,7.7h-1.5l-0.6-2.1h-2.6l-0.6,2.1h-1.4L421.2,7.6z M421,12.1h1.9l-0.3-0.9 c-0.2-0.8-0.5-1.7-0.7-2.5h0c-0.2,0.8-0.4,1.7-0.7,2.5L421,12.1z"/> <path fill="#0095AA" d="M426.6,8.8h-2.2V7.6h5.8v1.2H428v6.5h-1.4V8.8z"/> <path fill="#0095AA" d="M431,7.6h1.4v3.1h3.1V7.6h1.4v7.7h-1.4v-3.4h-3.1v3.4H431V7.6z"/> <path fill="#0095AA" d="M438.4,7.6h4.7v1.2h-3.3v1.9h2.8v1.2h-2.8v2.2h3.4v1.2h-4.8V7.6z"/> <path fill="#0095AA" d="M444.3,7.6h1.7l1.3,3.8c0.2,0.5,0.3,0.9,0.4,1.5h0c0.1-0.6,0.3-1,0.4-1.5l1.3-3.8h1.7v7.7h-1.3v-3.5 c0-0.7,0.1-1.8,0.2-2.5h0l-0.6,1.9l-1.3,3.4h-0.9l-1.2-3.4l-0.6-1.9h0c0.1,0.7,0.2,1.8,0.2,2.5v3.5h-1.3V7.6z"/> <path fill="#0095AA" d="M454.3,7.6h1.7l2.5,7.7H457l-0.6-2.1h-2.6l-0.6,2.1h-1.4L454.3,7.6z M454.2,12.1h1.9l-0.3-0.9 c-0.2-0.8-0.5-1.7-0.7-2.5h0c-0.2,0.8-0.4,1.7-0.7,2.5L454.2,12.1z"/> <path fill="#0095AA" d="M460,8.8h-2.2V7.6h5.8v1.2h-2.2v6.5H460V8.8z"/> <path fill="#0095AA" d="M464.7,7.6h1.4v7.7h-1.4V7.6z"/> <path fill="#0095AA" d="M467.4,11.5c0-2.5,1.6-4,3.5-4c1,0,1.7,0.4,2.2,1l-0.7,0.9c-0.4-0.4-0.9-0.6-1.5-0.6c-1.2,0-2.1,1-2.1,2.8 c0,1.7,0.8,2.8,2.1,2.8c0.7,0,1.2-0.3,1.6-0.7l0.8,0.8c-0.6,0.7-1.5,1.1-2.4,1.1C468.9,15.4,467.4,14,467.4,11.5z"/> <path fill="#0095AA" d="M475.8,7.6h1.7l2.5,7.7h-1.5l-0.6-2.1h-2.6l-0.6,2.1h-1.4L475.8,7.6z M475.7,12.1h1.9l-0.3-0.9 c-0.2-0.8-0.5-1.7-0.7-2.5h0c-0.2,0.8-0.4,1.7-0.7,2.5L475.7,12.1z"/> <path fill="#0095AA" d="M300.5,20.7h1.1l2.6,7.7h-1.1l-0.7-2.3h-2.8l-0.7,2.3h-1L300.5,20.7z M299.8,25.2h2.3l-0.4-1.2 c-0.3-0.9-0.5-1.7-0.8-2.6h0c-0.2,0.9-0.5,1.7-0.8,2.6L299.8,25.2z"/> <path fill="#0095AA" d="M305.1,20.7h1.1l2.8,4.8c0.3,0.5,0.6,1.1,0.8,1.7h0c-0.1-0.8-0.1-1.7-0.1-2.5v-4h0.9v7.7h-1.1l-2.8-4.8 c-0.3-0.5-0.6-1.1-0.8-1.7h0c0.1,0.8,0.1,1.6,0.1,2.4v4.1h-0.9V20.7z"/> <path fill="#0095AA" d="M312.4,20.7h1.9c2.4,0,3.7,1.4,3.7,3.8c0,2.5-1.3,3.9-3.6,3.9h-2V20.7z M314.3,27.6c1.8,0,2.7-1.1,2.7-3.1 c0-1.9-0.9-3-2.7-3h-0.9v6.1H314.3z"/> <path fill="#0095AA" d="M321.4,20.6l1.4,0l0.6,3.9c0.1,0.8,0.2,1.6,0.3,2.5l0,0c0.2-0.9,0.3-1.7,0.5-2.5l1-3.9l1.3,0l0.9,3.9 c0.2,0.8,0.3,1.6,0.5,2.5l0,0c0.1-0.9,0.2-1.7,0.4-2.5l0.7-3.9l1.3,0l-1.6,7.7l-1.8,0l-0.8-4.1c-0.1-0.6-0.2-1.2-0.3-1.9l0,0 c-0.1,0.7-0.2,1.2-0.3,1.9l-0.9,4l-1.8,0L321.4,20.6z"/> <path fill="#0095AA" d="M330.8,24.4c0-2.5,1.5-3.9,3.5-3.9c2,0,3.4,1.5,3.3,4c0,2.5-1.5,4-3.5,4C332.2,28.5,330.8,26.9,330.8,24.4z M336.2,24.5c0-1.7-0.7-2.7-1.9-2.8c-1.2,0-2,1-2,2.7c0,1.7,0.7,2.8,1.9,2.9C335.4,27.3,336.2,26.3,336.2,24.5z"/> <path fill="#0095AA" d="M338.8,20.6l1.4,0l-0.1,6.5l3.2,0.1l0,1.2l-4.6-0.1L338.8,20.6z"/> <path fill="#0095AA" d="M344.4,20.6l4.7,0.1l0,1.2l-3.3-0.1l0,2.2l2.8,0l0,1.2l-2.8,0l-0.1,3.2l-1.4,0L344.4,20.6z"/> <path fill="#0095AA" d="M350,20.6l2.6,0c1.6,0,2.8,0.6,2.8,2.3c0,1.2-0.6,1.9-1.6,2.2l1.8,3.2l-1.6,0l-1.6-3l-1.1,0l-0.1,3l-1.4,0 L350,20.6z M352.4,24.3c1,0,1.6-0.4,1.6-1.3c0-0.9-0.5-1.2-1.6-1.2l-1.1,0l0,2.5L352.4,24.3z"/> <path fill="#0095AA" d="M358.4,20.7l1.7,0l2.4,7.8l-1.5,0l-0.6-2.1l-2.6,0l-0.6,2.1l-1.4,0L358.4,20.7z M358.2,25.2l1.9,0l-0.2-0.9 c-0.2-0.8-0.4-1.7-0.7-2.5l0,0c-0.2,0.8-0.5,1.7-0.7,2.5L358.2,25.2z"/> <path fill="#0095AA" d="M363.5,20.6l1.7,0l1.3,3.8c0.2,0.5,0.3,0.9,0.4,1.5l0,0c0.2-0.6,0.3-1,0.5-1.5l1.4-3.8l1.7,0l-0.1,7.7l-1.3,0 l0.1-3.5c0-0.7,0.1-1.8,0.3-2.5l0,0l-0.6,1.9l-1.3,3.4l-0.9,0l-1.2-3.5l-0.6-1.9l0,0c0.1,0.7,0.2,1.8,0.2,2.5l-0.1,3.5l-1.3,0 L363.5,20.6z"/> <path fill="#0095AA" d="M371.8,19l0.9,0L372.5,30l-0.9,0L371.8,19z"/> <path fill="#0095AA" d="M376.1,20.7l1.7,0l2.4,7.8l-1.5,0l-0.6-2.1l-2.6,0l-0.6,2.1l-1.4,0L376.1,20.7z M375.8,25.2l1.9,0l-0.2-0.9 c-0.2-0.8-0.4-1.7-0.7-2.5l0,0c-0.2,0.8-0.5,1.7-0.7,2.5L375.8,25.2z"/> <path fill="#0095AA" d="M380.9,20.6l1.4,0l-0.1,6.5l3.2,0.1l0,1.2l-4.6-0.1L380.9,20.6z"/> <path fill="#0095AA" d="M386.6,20.6l2.4,0c1.7,0,3,0.7,3,2.4c0,1.7-1.3,2.5-3,2.4l-1.1,0l0,2.8l-1.4,0L386.6,20.6z M388.9,24.5 c1.1,0,1.7-0.4,1.7-1.4c0-0.9-0.6-1.3-1.7-1.3l-0.9,0l0,2.7L388.9,24.5z"/> <path fill="#0095AA" d="M393,20.6l1.4,0l-0.1,3.1l3.1,0.1l0.1-3.1l1.4,0l-0.1,7.7l-1.4,0l0.1-3.4l-3.1-0.1l-0.1,3.4l-1.4,0L393,20.6z "/> <path fill="#0095AA" d="M402,20.7l1.7,0l2.4,7.8l-1.5,0l-0.6-2.1l-2.6,0l-0.6,2.1l-1.4,0L402,20.7z M401.8,25.2l1.9,0l-0.2-0.9 c-0.2-0.8-0.4-1.7-0.7-2.5l0,0c-0.2,0.8-0.5,1.7-0.7,2.5L401.8,25.2z"/> </g> </g> <a href="https://www.wolfram.com/mathematica/"><rect x="296.2" y="0.1" style="fill:#ffffff00;" width="183.8" height="16"/></a> <a href="https://wolframalpha.com/"><rect x="296.2" y="16.4" style="fill:#ffffff00;" width="123.4" height="13.6"/></a> <a href="/"><rect x="1" y="0.1" style="fill:#ffffff00;" width="292.4" height="29.9"/></a> </svg> <form method="get" action="/search/" name="search" id="search" accept-charset="UTF-8"> <input type="text" name="query" placeholder="Search" id="searchField"> <img src="/images/header/search-icon.png" width="18" height="18" class="search-btn" title="Search" alt="Search"> <img src="/images/header/menu-close.png" width="16" height="16" id="search-close" class="close-btn" title="Close" alt="Close"> </form> </header> <section class="left-side"> <img src="/images/sidebar/menu-close.png" width="16" height="16" id="dropdown-topics-menu-close" class="close-btn"> <form method="get" action="/search/" name="search" id="search-mobile" accept-charset="UTF-8"> <input type="text" name="query" placeholder="Search" id="searchFieldMobile"> <img src="/images/header/search-icon.png" width="18" height="18" id="mobile-search" class="search-btn" title="Search" alt="Search" onclick="submitForm()"> </form> <nav class="topics-nav"> <a href="/topics/Algebra.html" id="sidebar-algebra"> Algebra </a> <a href="/topics/AppliedMathematics.html" id="sidebar-appliedmathematics"> Applied Mathematics </a> <a href="/topics/CalculusandAnalysis.html" id="sidebar-calculusandanalysis"> Calculus and Analysis </a> <a href="/topics/DiscreteMathematics.html" id="sidebar-discretemathematics"> Discrete Mathematics </a> <a href="/topics/FoundationsofMathematics.html" id="sidebar-foundationsofmathematics"> Foundations of Mathematics </a> <a href="/topics/Geometry.html" id="sidebar-geometry"> Geometry </a> <a href="/topics/HistoryandTerminology.html" id="sidebar-historyandterminology"> History and Terminology </a> <a href="/topics/NumberTheory.html" id="sidebar-numbertheory"> Number Theory </a> <a href="/topics/ProbabilityandStatistics.html" id="sidebar-probabilityandstatistics"> Probability and Statistics </a> <a href="/topics/RecreationalMathematics.html" id="sidebar-recreationalmathematics"> Recreational Mathematics </a> <a href="/topics/Topology.html" id="sidebar-topology"> Topology </a> </nav> <nav class="secondary-nav"> <a href="/letters/"> Alphabetical Index </a> <a href="/whatsnew/"> New in MathWorld </a> </nav> </section> <section id="content"> <!-- Begin Subject --> <nav class="breadcrumbs"><ul class="breadcrumb"> <li> <a href="/topics/FoundationsofMathematics.html">Foundations of Mathematics</a> </li> <li> <a href="/topics/Logic.html">Logic</a> </li> <li> <a href="/topics/Decidability.html">Decidability</a> </li> </ul><ul class="breadcrumb"> <li> <a href="/topics/MathWorldContributors.html">MathWorld Contributors</a> </li> <li> <a href="/topics/Strzebonski.html">Strzebonski</a> </li> </ul></nav> <!-- End Subject --> <!-- Begin Title --> <h1>Tarski's Theorem</h1> <!-- End Title --> <hr class="margin-t-1-8 margin-b-3-4"> <!-- Begin Total Content --> <!-- Begin Content --> <div class="entry-content"> <p> Tarski's theorem says that the <a href="/First-OrderLogic.html">first-order</a> theory of reals with <img src="/images/equations/TarskisTheorem/Inline1.svg" class="inlineformula" style="max-height:100%;max-width:100%" border="0" width="11" height="21" alt="+" />, <img src="/images/equations/TarskisTheorem/Inline2.svg" class="inlineformula" style="max-height:100%;max-width:100%" border="0" width="8" height="21" alt="*" />, <img src="/images/equations/TarskisTheorem/Inline3.svg" class="inlineformula" style="max-height:100%;max-width:100%" border="0" width="13" height="21" alt="=" />, and <img src="/images/equations/TarskisTheorem/Inline4.svg" class="inlineformula" style="max-height:100%;max-width:100%" border="0" width="11" height="21" alt="&gt;" /> allows <a href="/QuantifierElimination.html">quantifier elimination</a>. Algorithmic quantifier elimination implies <a href="/Decidable.html">decidability</a> assuming that the truth values of sentences involving only constants can be computed. However, the converse is not true. For example, the first-order theory of reals with <img src="/images/equations/TarskisTheorem/Inline5.svg" class="inlineformula" style="max-height:100%;max-width:100%" border="0" width="11" height="21" alt="+" />, <img src="/images/equations/TarskisTheorem/Inline6.svg" class="inlineformula" style="max-height:100%;max-width:100%" border="0" width="8" height="21" alt="*" />, and <img src="/images/equations/TarskisTheorem/Inline7.svg" class="inlineformula" style="max-height:100%;max-width:100%" border="0" width="13" height="21" alt="=" /> is decidable, but does not allow <a href="/QuantifierElimination.html">quantifier elimination</a>. </p> <p> Tarski's theorem means that the solution set of a <a href="/QuantifiedSystem.html">quantified system</a> of real algebraic equations and inequations is a <a href="/SemialgebraicSet.html">semialgebraic set</a> (Tarski 1951, Strzebonski 2000). </p> <p> Although Tarski proved that <a href="/QuantifierElimination.html">quantifier elimination</a> was possible, his method was totally impractical (Davenport and Heintz 1988). A much more efficient procedure for implementing <a href="/QuantifierElimination.html">quantifier elimination</a> is called <a href="/CylindricalAlgebraicDecomposition.html">cylindrical algebraic decomposition</a>. It was developed by Collins (1975) and is implemented as <tt><a href="http://reference.wolfram.com/language/ref/CylindricalDecomposition.html">CylindricalDecomposition</a></tt>[<i>ineqs</i>, <i>vars</i>]. </p> </div> <!-- End Content --> <hr class="margin-b-1-1-4"> <div class="c-777 entry-secondary-content"> <!-- Begin See Also --> <h2>See also</h2><a href="/CylindricalAlgebraicDecomposition.html">Cylindrical Algebraic Decomposition</a>, <a href="/Decidable.html">Decidable</a>, <a href="/QuantifiedSystem.html">Quantified System</a>, <a href="/Quantifier.html">Quantifier</a>, <a href="/QuantifierElimination.html">Quantifier Elimination</a>, <a href="/SemialgebraicSet.html">Semialgebraic Set</a> <!-- End See Also --> <!-- Begin CrossURL --> <!-- End CrossURL --> <!-- Begin Contributor --> <p class="contributor"> <i>Portions of this entry contributed by <a target="_blank" href="/topics/Strzebonski.html">Adam Strzebonski</a></i> </p> <!-- End Contributor --> <!-- Begin Wolfram Alpha Pod --> <h2>Explore with Wolfram|Alpha</h2> <div id="WAwidget"> <div class="WAwidget-wrapper"> <img alt="WolframAlpha" title="WolframAlpha" src="/images/wolframalpha/WA-logo.png" width="136" height="20"> <form name="wolframalpha" action="https://www.wolframalpha.com/input/" target="_blank"> <input type="text" name="i" class="search" placeholder="Solve your math problems and get step-by-step solutions" value=""> <button type="submit" title="Evaluate on WolframAlpha"></button> </form> </div> <div class="WAwidget-wrapper try"> <p class="text-align-r"> More things to try: </p> <ul> <li><a target="_blank" href="https://www.wolframalpha.com/input/?i=Anger+J">Anger J</a></li> <li><a target="_blank" href="https://www.wolframalpha.com/input/?i=domain+of+sqrt%28sin%28x%29%29">domain of sqrt(sin(x))</a></li> <li><a target="_blank" href="http://www.wolframalpha.com/input/?i=minimize+x%5E4-x">minimize x^4-x</a></li> </ul> </div> </div> <!-- End Wolfram Alpha Pod --> <!-- Begin References --> <h2>References</h2><cite>Collins, G.&nbsp;E. &quot;Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition.&quot; In <i>Proc. 2nd GI Conf. Automata Theory and Formal Languages.</i> New York: Springer-Verlag, pp.&nbsp;134-183, 1975.</cite><cite>Davenport, J. and Heintz, J. &quot;Real Quantifier Elimination Is Doubly Exponential.&quot; <i>J. Symb. Comput.</i> <b>5</b>, 29-35, 1988.</cite><cite>Marker, D. &quot;Model Theory and Exponentiation.&quot; <i>Not. Amer. Math. Soc.</i> <b>43</b>, 753-759, 1996.</cite><cite>Strzebonski, A. &quot;Solving Algebraic Inequalities.&quot; <i>Mathematica J.</i> <b>7</b>, 525-541, 2000.</cite><cite>Tarski, A. &quot;Sur les ensembles d&eacute;finissables de nombres r&eacute;els.&quot; <i>Fund. Math.</i> <b>17</b>, 210-239, 1931.</cite><cite>Tarski, A. <i>A Decision Method for Elementary Algebra and Geometry.</i> Manuscript. Santa Monica, CA: RAND Corp., 1948. Republished as <i><a href="http://www.amazon.com/exec/obidos/ASIN/B0007E4QTK/ref=nosim/ericstreasuretro">A Decision Method for Elementary Algebra and Geometry, 2nd ed.</a></i> Berkeley, CA: University of California Press, 1951.</cite><h2>Referenced on Wolfram|Alpha</h2><a href="http://www.wolframalpha.com/entities/mathworld/tarski%E2%80%99s_theorem/yj/6e/er/" title="Tarski's Theorem" target="_blank">Tarski's Theorem</a> <!-- End References --> <!-- Begin CiteAs --> <h2>Cite this as:</h2> <p> <a href="/topics/Strzebonski.html">Strzebonski, Adam</a> and <a href="/about/author.html">Weisstein, Eric W.</a> &quot;Tarski's Theorem.&quot; From <a href="/"><i>MathWorld</i></a>--A Wolfram Web Resource. <a href="https://mathworld.wolfram.com/TarskisTheorem.html">https://mathworld.wolfram.com/TarskisTheorem.html</a> </p> <!-- End CiteAs --> <h2>Subject classifications</h2><nav class="breadcrumbs"><ul class="breadcrumb"> <li> <a href="/topics/FoundationsofMathematics.html">Foundations of Mathematics</a> </li> <li> <a href="/topics/Logic.html">Logic</a> </li> <li> <a href="/topics/Decidability.html">Decidability</a> </li> </ul><ul class="breadcrumb"> <li> <a href="/topics/MathWorldContributors.html">MathWorld Contributors</a> </li> <li> <a href="/topics/Strzebonski.html">Strzebonski</a> </li> </ul></nav> <!-- End Total Content --> </div> </section> </section> <!-- /container --> </div> </main> <aside id="bottom"> <style> #bottom { padding-bottom: 65px; } #acknowledgment { display:none; } .attribution { font-size: .75rem; font-style: italic; } footer ul li:not(:last-of-type)::after { background: #a3a3a3; margin-left: .3rem; margin-right: .1rem; } @media all and (max-width: 900px) { .attribution { font-size: 12px; } } @media (max-width: 600px) { footer { max-width: 360px; } footer ul { max-width: 360px; } footer ul:nth-child(1) li:nth-child(2):after { content: ""; height: 11px; } footer ul:nth-child(1) li:nth-child(3):after { content: ""; height: 0px; } } </style> <footer> <ul> <li><a href="/about/">About MathWorld</a></li> <li><a href="/classroom/">MathWorld Classroom</a></li> <li><a href="/contact/">Contribute</a></li> <li><a href="https://www.amazon.com/exec/obidos/ASIN/1420072218/ref=nosim/weisstein-20" target="_blank">MathWorld Book</a></li> <li class="display-n display-ib__600"><a href="https://www.wolfram.com" target="_blank">wolfram.com</a></li> </ul> <ul> <li class="display-n__600"><a href="/whatsnew/">13,209 Entries</a></li> <li class="display-n__600"><a href="/whatsnew/">Last Updated: Tue Nov 26 2024</a></li> <!-- <li><a href="https://www.wolfram.com" target="_blank">&copy;1999&ndash;<span id="copyright-year-end"> Wolfram Research, Inc.</a></li> --> <li><a href="https://www.wolfram.com" target="_blank">&copy;1999&ndash;2024 Wolfram Research, Inc.</a></li> <li><a href="https://www.wolfram.com/legal/terms/mathworld.html" target="_blank">Terms of Use</a></li> </ul> <ul class="wolfram"> <li class="display-n__600 display-n__900"><a href="https://www.wolfram.com" target="_blank" aria-label="Wolfram"><img src="/images/footer/wolfram-logo.png" alt="Wolfram" title="Wolfram" width="121" height="28"></a></li> <li class="display-n__600"><a href="https://www.wolfram.com" target="_blank">wolfram.com</a></li> <li class="display-n__600"><a href="https://www.wolfram.com/education/" target="_blank">Wolfram for Education</a></li> <li class="attribution">Created, developed and nurtured by Eric Weisstein at&nbsp;Wolfram&nbsp;Research</li> </ul> </footer> <section id="acknowledgment"> <i>Created, developed and nurtured by Eric Weisstein at Wolfram Research</i> </section> </aside> <script type="text/javascript" src="/scripts/scripts.js"></script> <script src="/common/js/c2c/1.0/WolframC2C.js"></script> <script src="/common/js/c2c/1.0/WolframC2CGui.js"></script> <script src="/common/js/c2c/1.0/WolframC2CDefault.js"></script> <link rel="stylesheet" href="/common/js/c2c/1.0/WolframC2CGui.css.en"> <style> .wolfram-c2c-wrapper { padding: 0px !important; border: 0px; } .wolfram-c2c-wrapper:active { border: 0px; } .wolfram-c2c-wrapper:hover { border: 0px; } </style> <script> let c2cWrittings = new WolframC2CDefault({'triggerClass':'mathworld-c2c_above', 'uniqueIdPrefix': 'mathworld-c2c_above-'}); </script> <style> #IPstripe-outer { background: #47a2af; } #IPstripe-outer:hover { background: #0095aa; } </style> <div id="IPstripe-wrap"></div> <script src="/common/stripe/stripe.en.js"></script> </body> </html>

Pages: 1 2 3 4 5 6 7 8 9 10