Skip to content

Instantly share code, notes, and snippets.

@koba-e964
Created March 9, 2021 15:48
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save koba-e964/9e4d77785702a3dbc80dc463e3733306 to your computer and use it in GitHub Desktop.
Save koba-e964/9e4d77785702a3dbc80dc463e3733306 to your computer and use it in GitHub Desktop.
[todai-2021-1]
(a,b,x1,x2)
2
(X1 x1)(X1 x2)[
[x1^2 + a x1 + b = -x1^2 /\ -1 < x1 /\ x1 < 0] /\
[x2^2 + a x2 + b = -x2^2 /\ 0 < x2 /\ x2 < 1]
].
finish
$ bin/qepcadd <todai-2021-1.txt
=======================================================
Quantifier Elimination
in
Elementary Algebra and Geometry
by
Partial Cylindrical Algebraic Decomposition
Version B 1.69, 16 Mar 2012
by
Hoon Hong
(hhong@math.ncsu.edu)
With contributions by: Christopher W. Brown, George E.
Collins, Mark J. Encarnacion, Jeremy R. Johnson
Werner Krandick, Richard Liska, Scott McCallum,
Nicolas Robidoux, and Stanly Steinberg
=======================================================
Enter an informal description between '[' and ']':
[todai-2021-1]Enter a variable list:
(a,b,x1,x2)Enter the number of free variables:
2
Enter a prenex formula:
(X1 x1)(X1 x2)[
[x1^2 + a x1 + b = -x1^2 /\ -1 < x1 /\ x1 < 0] /\
[x2^2 + a x2 + b = -x2^2 /\ 0 < x2 /\ x2 < 1]
].
=======================================================
Before Normalization >
finish
An equivalent quantifier-free formula:
b < 0 /\ b + a + 2 > 0 /\ b - a + 2 > 0
===================== The End =======================
-----------------------------------------------------------------------------
0 Garbage collections, 0 Cells and 0 Arrays reclaimed, in 0 milliseconds.
350606 Cells in AVAIL, 500000 Cells in SPACE.
System time: 20 milliseconds.
System time after the initialization: 15 milliseconds.
-----------------------------------------------------------------------------
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment