10 GCLC 2015 Manual

User Manual:

Open the PDF directly: View PDF .
Page Count: 109

Download
Open PDF In Browser	View PDF

GCLC 2015
(Geometry Constructions → LATEX Converter)
Manual
Predrag Janičić
Faculty of Mathematics
Studentski trg 16
11000 Belgrade
Serbia

url: www.matf.bg.ac.rs/~janicic
e-mail: janicic@matf.bg.ac.rs
GCLC page: www.matf.bg.ac.rs/~janicic/gclc
October 2015

c 1996-2015 Predrag Janičić

Contents
1 Briefly About GCLC
1.1 Comments and Bugs Report . . . . . . . . . . . . . . . . . . . . .
1.2 Copyright Notice . . . . . . . . . . . . . . . . . . . . . . . . . . .
2 Quick Start
2.1 Installation . . . . . . . .
2.2 First Example . . . . . . .
2.3 Basic Syntax Rules . . . .
2.4 Basic Objects . . . . . . .
2.5 Geometrical Constructions
2.6 Basic Ideas . . . . . . . .

5
7
7

.
.
.
.
.
.

9
9
10
11
11
12
12

3 GCLC Language
3.1 Basic Definition Commands . . . . . . . . . . . . . . . . .
3.2 Basic Constructions Commands . . . . . . . . . . . . . . .
3.3 Transformation Commands . . . . . . . . . . . . . . . . .
3.4 Calculations, Expressions, Arrays, and Control Structures
3.5 Drawing Commands . . . . . . . . . . . . . . . . . . . . .
3.6 Labelling and Printing Commands . . . . . . . . . . . . .
3.7 Low Level Commands . . . . . . . . . . . . . . . . . . . .
3.8 Cartesian Commands . . . . . . . . . . . . . . . . . . . . .
3.9 3D Cartesian Commands . . . . . . . . . . . . . . . . . .
3.10 Layers . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.11 Support for Animations . . . . . . . . . . . . . . . . . . .
3.12 Support for Theorem Provers . . . . . . . . . . . . . . . .

.
.
.
.
.
.
.
.
.
.
.
.

15
16
16
18
19
23
29
31
33
37
39
40
40

.
.
.
.
.
.

4 Graphical User Interface
43
4.1 An Overview of the Graphical Interface . . . . . . . . . . . . . . 43
4.2 Features for Interactive Work . . . . . . . . . . . . . . . . . . . . 44
5 Exporting Options
5.1 Export to Simple LATEX format . . . . . . . .
5.1.1 Generating LATEX Files and gclc.sty
5.1.2 Changing LATEX File Directly . . . . .
5.1.3 Handling More Pictures on a Page . .
5.1.4 Batch Processing . . . . . . . . . . . .
5.2 Export to PSTricks LATEX format . . . . . . .
5.3 Export to TikZ LATEX format . . . . . . . . .
3

.
.
.
.
.
.
.

49
49
50
50
51
51
52
53

CONTENTS
5.4
5.5
5.6
5.7
5.8

Export to Raster-based Formats and Export to Sequences of Images
Export to eps Format . . . . . . . . . . . . . . . . . . . . . . . .
Export to svg Format . . . . . . . . . . . . . . . . . . . . . . . .
Export to xml Format . . . . . . . . . . . . . . . . . . . . . . . .
Generating PostScript and pdf Documents . . . . . . . . . . .

6 Theorem Prover
6.1 Introductory Example . . . . . . . . . . . . . . . . . .
6.2 Basic Sorts of Conjectures . . . . . . . . . . . . . . . .
6.3 Geometry Quantities and Stating Conjectures . . . . .
6.4 Area Method . . . . . . . . . . . . . . . . . . . . . . .
6.4.1 Underlying Constructions . . . . . . . . . . . .
6.4.2 Integration of Algorithm and Auxiliary Points
6.4.3 Non-degenerative Conditions and Lemmas . . .
6.4.4 Structure of Algorithm . . . . . . . . . . . . . .
6.4.5 Scope . . . . . . . . . . . . . . . . . . . . . . .
6.5 Wu’s Method and Gröbner Bases Method . . . . . . .
6.6 Prover Output . . . . . . . . . . . . . . . . . . . . . .
6.6.1 Prover’s Short Report . . . . . . . . . . . . . .
6.6.2 Controlling Level of Output . . . . . . . . . . .
6.6.3 Proofs in LATEX format . . . . . . . . . . . . .
6.6.4 Proofs in xml format . . . . . . . . . . . . . .
6.7 Automatic Verification of Regular Constructions . . .
7 xml
7.1
7.2
7.3

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

54
54
55
55
55
57
58
58
59
62
62
62
63
63
65
65
65
65
66
66
68
69

Support
73
xml . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
xml Suite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
Using xml Tools . . . . . . . . . . . . . . . . . . . . . . . . . . . 75

A List of Errors and Warnings

B Version History

C Additional Modules

D Acknowledgements

E Examples
E.1 Example
E.2 Example
E.3 Example
E.4 Example
E.5 Example

(Simple Triangle) .
(Conics) . . . . . . .
(Parametric Curves)
(While-loop) . . . .
(Ceva’s theorem) . .

.
.
.
.
.

89
89
90
92
94
96

Chapter 1

Briefly About GCLC
What is GCLC? GCLC (from “Geometry Constructions → LATEX converter”)
is a tool for visualizing and teaching geometry, and for producing mathematical illustrations. Its basic purpose is converting descriptions of mathematical objects (written in the gcl language) into digital figures. GCLC
provides easy-to-use support for many geometrical constructions, isometric transformations, conics, and parametric curves. The basic idea behind
GCLC is that constructions are formal procedures, rather than drawings.
Thus, in GCLC, producing mathematical illustrations is based on “describing figures” rather than of “drawing figures”. This approach stresses
the fact that geometrical constructions are abstract, formal procedures
and not figures. A figure can be generated on the basis of abstract description, in Cartesian model of a plane. These digital figures can be
displayed and exported to LATEX or some other format.
Although GCLC was initially built as a tool for converting formal descriptions of geometric constructions into LATEX form, now it is much more than
that. For instance, there is support for symbolic expressions, for drawing
parametric curves, for program loops, user-defined procedures, etc; builtin theorem provers can automatically prove a range of complex theorems;
the graphical interface makes GCLC a tool for teaching geometry, and
other mathematical fields as well.
The main purposes of GCLC:
• producing digital mathematical illustrations of high quality;
• usage in mathematical education and as a research tool;
• storing mathematical contents;
• studies of automated geometrical reasoning.
The main features of GCLC:
• freely available;
• support for a range of elementary and advanced constructions, and
isometric transformations;
• support for symbolic expressions, second order curves, parametric
curves, loops, user-defined procedures, etc.

1 Briefly About GCLC
• user-friendly interface, interactive work, animations, tracing points,
watch window (“geometry calculator”), and other tools;
• easy drawing of trees;
• built-in theorem provers, capable of proving many complex theorems
(in traditional geometry style or in algebraic style);
• very simple, very easy to use, very small in size;
• export of high quality figures into LATEX, eps, svg, bitmap format;
• import from JavaView JVX format;
• available from http://www.matf.bg.ac.rs/~janicic/gclc and from
EMIS (The European Mathematical Information Service) servers:
http://www.emis.de/misc/software/gclc/.

Implementation and platforms: There are command-line versions and versions with graphical user interface (GUI) of GCLC for Windows and
for Linux. The version with graphical user interface provides a range of
additional functionalities, including interactive work, animations, traces,
“watch window”, etc. It gives GCLC a new, graphic user-friendly interface, and introduces some new features which are not available in the
command-line version. It is a kind of an “Integrated Development Environment” or IDE for GCLC. The version of GCLC with GUI for Windows is called WinGCLC.
GCLC can be also used via GeoThms (joint work with Pedro Quaresma,
University of Coimbra), a web-based framework for constructive geometry
(http://hilbert.mat.uc.pt/~geothms).
GCLC program is implemented in the C++ programming language.
Author: GCLC is being developed at the Faculty of Mathematics, University
of Belgrade, by Predrag Janičić and, in some parts, by Predrag Janičić
and his collaborators:
• Ivan Trajković (University of Belgrade, Serbia) — a co-author of the
graphical interface for WinGCLC 2003;
• prof. Pedro Quaresma (University of Coimbra, Portugal) — a coauthor of the theorem prover based on the area method built into
GCLC.
• Goran Predović (University of Belgrade, Serbia) — the main author
of the theorem prover based on the Wu’s method and Gröbner based
method built into GCLC.
• prof. Pedro Quaresma (University of Coimbra, Portugal), Jelena Tomašević (University of Belgrade, Serbia), and Milena Vujošević-Janičić
(University of Belgrade, Serbia) — co-authors of the xml support for
GCLC.
• Luka Tomašević (University of Belgrade, Serbia) — the main author
of the support for graph drawing.
• prof. Konrad Polthier and Klaus Hildebrandt (Technical University,
Berlin, Germany) — coauthors of JavaView → GCLC converter).

1.1 Comments and Bugs Report

Version history: GCLC programs is under development since 1996. and had
several releases since then. It has thousands of users and has been used for
producing digital illustrations for a number of books and journal volumes
and in a number of different high-school and university courses.
What others said about GCLC/WinGCLC: “... program WinGCLC...
is a very useful, impressive professional academic geometry program.”
(from an anonymous review for “Teaching Mathematics and its Applications”)
References: More on the background of GCLC can be found in [6, 9, 5, 10,
7, 8].

1.1

Comments and Bugs Report

Please send your comments and/or noticed bugs to the following e-mail address:
janicic@matf.bg.ac.rs. Your feedback would be very much appreciated and
would help in improving the future releases of GCLC.

1.2

This software is protected by the Creative Commons licence CC BY-ND
(https://creativecommons.org/licenses/by-nd/4.0/) Attribution-NoDerivatives 4.0 International. This license allows for redistribution, commercial and
non-commercial, as long as it is passed along unchanged and in whole, with
credit to the author.
You may install and run GCLC without any restrictions.
All output of this software is your property. You are free to use it in teaching,
studying, research, and in producing digital illustrations.
THIS SOFTWARE IS PROVIDED ”AS IS” AND WITHOUT ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, WITHOUT LIMITATION, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.
If you use GCLC, please let me know by sending an e-mail to Predrag
Janičić (janicic@matf.bg.ac.rs). You will be put on the GCLC mailing list
and be informed about new releases of GCLC.
If you used GCLC for producing figures for your book, article, thesis, I
would be happy to hear about that.
Your feedback would be very much appreciated and would help in improving
the future releases of GCLC.

1 Briefly About GCLC

Chapter 2

Quick Start
In GCLC one describes mathematical objects in the gcl language. This description can be visualized within the version with GUI (or within view previewer, see p 85) or can be converted into some other format, e.g., LATEX format.
In this chapter, we describe how to run GCLC and we give one very simple
figure description and discuss how it can be processed and give an illustration
in LATEX format.

2.1

Installation

There is no installation required for GCLC— just unzip the distribution archive
(to a folder of your choice) and you can run the program. For convenience, you
can add the path to this folder to the system path, so you can run GCLC from
any folder. You can associate GCLC (GUI version) with .gcl files, so you can
always open them with GCLC.
When the archive is unpacked, in the root folder there will be executable
programs – a command line version and a version with GUI, and LATEX packages
gclc.sty and gclcproofs.sty for processing figures and proofs generated by
GCLC. In addition, there will be the following folders:
• manual with the manual file and additional reference papers;
• samples with a range of .gcl samples, organized in the following subfolders:
– basic_samples with basic samples for GCLC;
– samples_prover with samples for the theorem prover;
– samples_gui with samples specific for GUI version;
• tools with additional tools (view and jv2gcl) (not included in the version
for Linux);
• working_example with a self-contained example ready to be processed by
LATEX;
• LaTeX_packages with LATEX packages (developed by other authors) required for the prover output or for support for colors.

2 Quick Start
• XML_support xml suite for different processing of xml files generated by
GCLC.

2.2

First Example

Using GCLC is very simple. Like many other programs, GCLC has its document type — *.gcl document type. *.gcl file is nothing more than a plain text
file (it has no special formatting inside), containing a list of gcl commands.
Consider the following text:
point A 40 85
point B 35 20
point C 95 20
cmark_lt A
cmark_lb B
cmark_rb C
drawsegment A B
drawsegment B C
drawsegment C A
It describes a triangle ABC via gcl commands. The command point A 40 85
introduces a point A with coordinates (40, 85). The command cmark_lt A denotes the point A by a small circle and prints its name in left-top direction.
The command drawsegment A B draws the segment AB. More details on gcl
commands can be found in Chapter 3
If you are using the command-line version of GCLC, type the above text
(gcl code) in any text editor and save it under the name, say, quick.gcl. The
figure in LATEX format can be generated using the following command:
> gclc quick.gcl quick.pic
where quick.pic is the name of a resulting file.
Within the GUI version, you can type the above code directly to the builtin editor, save the file under the name, say, quick.gcl, and press the button
Build in the toolbar (or choose the option Picture/Build from the menu). Then,
you can export the picture to LATEX format by selecting the option File/Export
to.../LaTeX (and choosing the name, say, quick.pic).1 More details about the
GUI version can be found in Chapter 4.
The picture (contained in quick.pic) can be included in your LATEX document using the command:
\input{quick.pic}
in an appropriate position in your LATEX document. In addition, you have to
include (by the LATEX command \usepackage{gclc}) the package gclc (provided within the gclc distribution) in the preamble of your document,2 and
1 Within this chapter, we comment only on the simple L
AT X format, supported by
E
gclc.sty. However, GCLC can export to other LATEX formats, see Chapter 5.
2 You also have to put the file gclc.sty (providing the gclc package) in the current folder
(where your LATEX document is) or in the folder with other LATEX packages.

2.3 Basic Syntax Rules

then you can process your LATEX document as usual. If everything is ok, within
your LATEX document you will get the illustration as shown in Figure 2.1. More
details about export to LATEX can be found in Chapter 5.

Figure 2.1: Illustration generated from the given GCLC code

2.3

Basic Syntax Rules

The syntax of the gcl language is very simple. Commands, identifiers, constants
etc. must be separated by at least one tab or space symbol or a new line.
Usually, each new command (with its argument) is in separate line and empty
lines separate different parts of the construction.

2.4

Basic Objects

There are five types of objects in the gcl language: number, point, line,
circle and conic. They are represented in the following manner:
number n
(n)
point (x, y)
(x, y)
line ax + by + c = 0
(a, b, c)
circle (x − x0 )(x − x0 ) + (y − y0 )(y − y0 ) = r2 (x0 , y0 , r)
conic ax2 + 2bxy + cy 2 + 2dx + 2ey + f = 0
(a, b, c, d, e, f )

2 Quick Start

While processing an input file, GCLC generates the transcript file gclc.log
(in the current directory) with the list of all warnings and the list of all defined
objects (with their names and parameters). Instead of writing to the log file,
the GUI version shows this list in its output window.

2.5

Geometrical Constructions

Geometrical constructions are the main area of GCLC. A geometrical construction is a sequence of specific, primitive construction steps. These primitive
construction steps are also called elementary constructions and they are:
• construction (by ruler) of a line such that two given points belong to it;
• construction of a point such that it is the intersection of two lines (if such
a point exist);
• construction (by compass) of a circle such that its center is one given point
and such that the second given point belongs to it;
• construction of intersections between a given line and a given circle (if
such points exist).
By using the set of primitive constructions, one can define more involved,
compound constructions (e.g., construction of right angle, construction of the
segment midpoint, construction of the segment bisector etc.). In describing
geometrical constructions, it is usual to use higher level constructions as well as
the primitive ones.
GCLC follows the idea of formal constructions. It provides easy-to-use support for all primitive constructions, but also for a range of higher-level constructions. (Although motivated by the formal geometrical constructions, GCLC
provides a support for some non-constructible objects too — for instance, in
GCLC it is possible to determine/use a point obtained by rotation for 1◦ ,
although it is not possible to construct that point by ruler and compass).

2.6

Basic Ideas

There is a need of distinguishing abstract (i.e., formal, axiomatic) nature of
geometrical objects and their usual models. A geometrical construction is a mere
procedure of abstract steps and not a picture. However, for each (Euclidean)
construction, there is its counterpart in the standard Cartesian model. While a
construction is an abstract procedure, in order to make its usual representation
in Cartesian model of Euclidean plane, we still have to make some link between
these two. For instance, given three vertices of a triangle we can construct a
center of its inscribed circle (by using primitive constructions), but in order to
represent this construction in Cartesian plane, we have to take three particular
Cartesian points as vertices of the triangle. A figure description in GCLC is
usually made by a list of definitions of several fixed points (defined in terms
of Cartesian plane, i.e., by pairs of coordinates) and then a list of construction
steps based on these points. Normally, there should be very few such fixed points
and all other points should depend on them. Afterwards, if one wants to vary a

2.6 Basic Ideas

figure, he/she would usually change only coordinates of fixed points and all other
objects will be recalculated automatically. For instance, if points A and B are
given by their coordinates, never introduce their midpoint M also by coordinates,
but always via the command midpoint M A B. This would give your GCLC
descriptions flexibility and would better reflect the mathematical/geometrical
meaning of the figure.

2 Quick Start

Chapter 3

GCLC Language
In the gc language, there are several entities: commands (source code statements), objects (scalar, point, line, conic), and constants. A source code line
will generally have a command and identifiers (as handles for an object or variable) and possibly constants (including constant text enclosed by brackets). The
syntax requires that entities be separated by at least one tab or space symbol.
Commands should be separated by at least one tab or space symbol, or, for
better readability, by new line.
The commands fall into ten categories, and the identifiers will be one of five
types of objects in GCLC: number, point, line, circle, and conic. The
types are not attached to variables explicitly, but implicitly (with respect to the
given context).
Notation conventions. This document uses the following notation to clarify
that an identifier is of a particular type. When writing the source code, always
leave out the < and > marks.
• a constant (a decimal number) or a simple numerical variable (of
type number);
• an identifier associated with a point;
• an identifier associated with a line;
• an identifier associated with a circle;
• an identifier associated with a conic;
• Constant text string beginning with the symbol { and ending with
the symbol }.
• denotes an arbitrary expression.
Identifiers can be one to 99 characters. Underscores, single-quotes or braces
are permissible, but not white spaces. Identifiers are case-sensitive. Names like
A_1 or Q_{a}’ (in usual TEX form) can be used.

3 GCLC Language

3.1

Basic Definition Commands

The first parameter for each of these commands is the identifier, the rest are
constants or variables. The identifier can have a previous definition which
is ignored, it just gets a new type and new value.
• number : Definition of a number. The object
is defined or re-defined as type number, and can be used in commands as a
segment length, measure of an angle (in degrees) or as a command specific
parameter (but cannot be used where a point, line, circle or conic
is expected). The variable’s value can be changed by another number
command, or by expression command. can be a constant or
another number identifier. Example: number left_bottom_x 80.
• point : Definition of a point. is defined
or re-defined as type point, where its x-coordinate value becomes
and its y-coordinate value becomes . and can
be constants or number variables.
• point : Extended definition
of a point within support of animations (relevant only for GUI version,
see 3.11), where (, ) is the starting location for the point,
and (,) is the final location. , , ,
can be constants or number variables.
• line : Definition of a line. Identifier
gets type line, determined by (already defined) points and .
• circle : Definition of a circle. Identifier
gets type circle, and represents a circle determined by two points: the
first point () is the center and the second () is anywhere
on the circle.
• set_equal : The object gets the type and the value
of the object .

3.2

Basic Constructions Commands

• intersec The object with the specified identifier becomes point and gets coordinates of the intersection of
two given lines.
This command can also be used in this form:
intersec
The object with the specified identifier becomes point and gets coordinates of the intersection of two given lines given by
and by .
The full name, intersection, can also be used for this command.
• intersec2 The objects with the specified identifiers and become points and get coordinates

3.2 Basic Constructions Commands

of the intersection of two given circles, of a given circle and a line, or of a
given line and a circle.
The full name, intersection2, can also be used for this command.
• midpoint The object with the specified identifier becomes point and gets coordinates of the midpoint of the
segment determined by two given points.
• med The object with the specified identifier
becomes line and gets the parameters of the line that bisects (and
is perpendicular to) the segment determined by the two given points.
The full name, mediatrice, can also be used for this command.
• bis The object with the specified
identifier becomes line and gets the parameters of the line that
bisects the angle determined by three given points. Example:
bis s A B C
makes object s to become line with parameters of the bisector of the
angle 6 ABC.
The full name, bisector, can also be used for this command.
• perp The object with the specified identifier
becomes line and gets the parameters of the line that is perpendicular to the given line and contains the given point.
The full name, perpendicular, can also be used for this command.
• foot The object with the specified identifier
becomes point and gets the parameters of the foot of the perpendicular from the point to the line .
• parallel The object with the specified identifier becomes line and gets the parameters of the line that is
parallel to the given line and contains the given point.
• getcenter The object with the specified identifier
becomes point and gets the parameters of the center of the given circle.
• onsegment The object with the specified identifier becomes point, placed randomly on the line segment determined by the two given points.
• online The object with the specified identifier
becomes point, placed randomly on the line determined by the
two given points (more precisely, a random point is chosen between points
X and Y such that X is symmetrical to with respect to
and Y is symmetrical to with respect to ). (This command is suitable for describing constructions with properties to be proved
by the theorem provers.)

3 GCLC Language
• oncircle The object with the specified identifier becomes point, placed randomly on the circle with center and with the point . (This command is suitable
for describing constructions with properties to be proved by the theorem
provers.)

3.3

Transformation Commands

• translate The object with the specified identifier becomes point and gets the parameters of the point
that is an image of the third point () in a translation for the vector
determined by the first and the second given point. Example:
translate A2 X Y A1
makes object A2 to become point such that T (A1)=A2, where T is translation for the vector XY.
• rotate The object with the specified identifier becomes point and gets the parameters of the point that
is an image of the second given point in a rotation around the first given
point and for the given (positive or negative) angle (determined by the
given constant or number). Example:
rotate A2 O 90 A1
makes object A2 to become point such that R(A1)=A2, where R is rotation around the point O for the angle of 90◦ .
• rotateonellipse The
object with the specified identifier becomes point and gets the
parameters of the point Y such that the angle X Y is equal to
n, where X is the intersection of the half-line and the
ellipse determined by .
• sim The object with the specified identifier
becomes point and gets the parameters of the point that is an image of
the given point in a half-turn, line-reflection or inversion (depending of
the type (point, line, or circle) of the second argument). Example:
If l is line,
sim A2 l A1
makes object A2 to become point such that S(A1)=A2 where S is line
reflection determined by the line l.
The full name, symmetrical, can also be used for this command.
• turtle The object with the specified identifier becomes point. Its segment length from
will be . The segment determined by and will make
an angle (in degrees) with the segment from to .
Example:
turtle A X Y 90 10.00
makes object A to become point such that YA=10.00 and 6 XYA=90◦ .

3.4 Calculations, Expressions, Arrays, and Control Structures

• towards The object with the specified
identifier becomes point, placed on the line determined by the
two given points. The distance from to the new point
is a fraction of the distance from to . Thus, if
0 < < 1, then the point will be between points
and ; if > 1, the point will be between points
and ; if < 0, the point will be between
points and . Example:
towards O A B 0.9
makes object O to become point such that AO=0.9 ·AB and O is between
A and B.

3.4

Calculations, Expressions, Arrays, and Control Structures

• getx : The object with the specified identifier becomes number and gets the value of the x-coordinate of the given point
.
• gety The object with the specified identifier becomes number and gets the value of the y-coordinate of the given point
.
• distance : The object with the specified identifier becomes number and gets the value of the distance between
two given points.
• angle : The object with the specified
identifier becomes number and gets the measure of the angle
determined by three given points. Example:
angle alpha A B C
makes object alpha to get type number and its value will be the measure
of the (oriented) angle 6 ABC (in degrees).
• angle_o : The same as the command
angle, but takes orientation into account, so the angle can have positive
and negative values. Therefore, this version is compatible with the command rotate.
• random The object with the specified identifier gets type
number and gets a (pseudo)random value between 0 and 1.
• expression {exp}: The object with the specified identifier
gets type number and gets the value of the expression exp. Example:
expression e {sin(3)*(5+2)}
After the above command, e will have the value 0.366352.
Defined variables of the type number can be used in expressions. No
other variables can be used in expressions. For instance,

3 GCLC Language
expression e {n+5}
makes object e to become number equal to n+5, if n is of the type number.
The following standard functions, operators and relations are supported in
expressions: + (addition), - (subtraction), * (multiplication), / (division),
== (equality), != (inequality), <, <=, >, >=, && (and), || (or), abs, ceil
(rounding up), floor (rounding down), sin, cos, tan (with arguments
expressed in radians), sinh, cosh, tanh, asin, acos, atan, sqrt, exp, pow
(exponentiation), log, log10, min (two arguments), max (two arguments).
For example,
expression m { pow(n+1,2)}
makes object m equal (n+1)2 (note that the operator ^ is not used for
exponentiation).
The ite operator (from if-then-else) is also supported. For example,
expression E {ite(n>0,1,2)}
makes object E to become number equal to 1 if n is greater than zero,
and 2 otherwise.
Blank spaces in expressions are allowed and ignored.
• array { ... }: Definition of an (multidimensional) array. The values ... are dimensions of the array. There can be up to 10 dimensions. All elements of
the array initially have type number and value 0. Indexing is 1-based, i.e.,
the first element of the array has all indices equal 1. Indices are written
in separate angle brackets.
Examples:
array A { 4 3 }
defines 4 × 3 = 12 elements of the array A — A[1][1], A[1][2], . . ., A[4][3].
All these elements initially have the type number and value 0, but both
of these can be changed, as for any other variable. So, different elements
of the same array can have different types.
Indices of an array element can be arbitrary expressions, that can also involve other array elements (of type number). For instance, if all elements
of an (one-dimensional) array A are numbers, one can use the following
construction: A[5 + A[5]] (in any position that requires a number).
An array with the same name can be defined more than once. If the numbers of dimensions are same, and if all dimensions are same, then all old
elements are reset to have type number and value 0. If some dimensions
are different, new elements may be added (if some new dimensions are
greater then the old ones), but old elements (those not covered by the
new definition) are never destroyed (even if some new dimensions are less
then the old ones). If the numbers of dimensions (in two definitions) are
different, then these two arrays are considered different and there are no
resetting of the old elements.

3.4 Calculations, Expressions, Arrays, and Control Structures

• while {} { }: is a sequence of
commands. This sequence will be repeatedly executed as long as
condition is true (nonzero). Example:
point A 0 0
number n 0
while { n<30 }
{
point B n 30
drawsegment A B
expression n { n+1 }
}

Both syntax and run-time errors encountered within a while-block are
reported only as Invalid while block error and no other (more detailed)
information on the error is provided. Also, all warnings encountered within
a while-block are suppressed and are not written to the log.
The sequence of commands in the while-block behaves as any GCLC
sequence. It shares the defined variables and the environment (defined
by commands ang_picture and ang_origin etc) with the outer GCLC
context.
If the condition is never fulfilled, this leads to non-termination (i.e.,
infinite loop). In order to prevent this, the system enables only a limited
number (10000) of executions of blocks within while-loops. If this number
is exceeded, then the error Too many while-block executions (more
than 10000). Possible infinite loop is reported and the processing
is stopped.
Procedures cannot be defined within while-blocks.
• if_then_else {} { } { }:
is a sequence of commands. This sequence will be executed
if condition is true (nonzero). is a sequence of commands. This sequence will be executed if condition is false (zero).
Example:
distance d1 C A
distance d2 C B
if_then_else { d1 and
are reported only as Invalid if-then-else block error
and no other (more detailed) information on the error is provided. Also,
all warnings encountered within a if-then-else-block are suppressed and
are not written to the log.
The sequence of commands in the blocks behaves as any GCLC sequence.
It shares the defined variables and the environment (defined by commands
ang_picture and ang_origin etc) with the outer GCLC context.
Procedures cannot be defined within if-then-else-blocks.
• procedure { } { }:
is the name of the procedure. is a list of the procedure’s arguments. Arguments are separated by blank spaces. In GCLC,
arguments are passed by their names, which means that they may be
changed by the procedure. is a sequence of commands. It inherits the environment form the outer context, but not the
variables from the outer context. Within a block, only arguments and
variables defined within it can be used. The definition of a procedure
must precede calling it. Procedures cannot be defined within while-blocks
or within definitions of other procedures.
Example:
procedure drawtriangle { X Y Z }
{
drawsegment X
drawsegment Y
drawsegment Z
}

• call { } is the name of the procedure.
is a list of the arguments that will be passed to the procedure. Arguments are separated by blank spaces. In GCLC, variables are
passed to procedures as arguments by names and they may be changed by
a procedure. Argument of a procedure call can also be a constant (and, of
course, it is passed by value). If a variable that is argument is not defined
before (i.e., with an intention that it receives the resulting value of the
function), by default it get the type number and the value 0. If a single
variable is used for several arguments, it will get the value of the last of
such arguments (when returning from the procedure).
Procedures can be called from other procedures.
Example:
call drawtriangle { A B C }

3.5 Drawing Commands

• include Reads/consults the contents of another .gcl file.
After this command, variables and procedures defined in that another file
can be used (as they were defined within the current file). Both syntax and
run-time errors encountered within the consulted file are reported only as
Invalid include file error and no other (more detailed) information on
the error is provided. Also, all warnings encountered within the consulted
file are suppressed and are not written to the log.

3.5

Drawing Commands

All drawn figures are clipped against the defined picture area. The current area
can be changed by the area command.
• drawpoint Generates a (export–specific) command for drawing
the specified point.
• drawsegment Generates a command for drawing the
segment determined by endpoints named and .
• drawdashsegment Generates commands for drawing
the dashed segment connecting points named and . The
length of dashes can be changed by the dash command.
• drawline Generates a command for drawing the given line.
• drawline Generates a command for drawing the line
determined by the points and .
• drawdashline Generates a command for drawing the given line
dashed.
• drawdashline Generates a command for drawing the
dashed line determined by the points and .
• drawvector Generates a command for drawing the
vector determined by points and .
• drawarrow Generates commands for drawing an
arrow on the line segment (the line segment itself is not
drawn). The ratio between the distance from to the end of the
arrow and the distance from to is equal to . The
default shape of the arrow can be changed by the command arrowstyle.
• drawcircle Generates commands for drawing the given circle.
In figures exported to the simple LATEX format, GCLC draws circles and
arcs segment by segment. The number of segments can be changed by
the circleprecision command. By the default, a circle of radius 10mm
has 72 segments, while the number of segments depends (linearly) on the
circle size.

3 GCLC Language
• drawcircle Generates commands for drawing the circle determined by center and one point .
In figures exported the simple LATEX format, GCLC draws circles and
arcs segment by segment. The number of segments can be changed by the
circleprecision command.
• drawdashcircle Generates commands for drawing the
circle determined by center and one point , and made
of dashes. In this mode, GCLC draws circles arc by arc and every third
arc will not be drawn, so the length of these arcs can be changed by the
circleprecision command.
• drawarc Generates commands for drawing the arc
determined by center , one point and the measure of
angle equal ( is constant or number).
• drawarc_p The same as drawarc, but always draws
the arc in positive (counterclockwise) direction.
• drawdasharc Generates commands for drawing
the dashed arc determined by center , one point and
the measure of angle equal ( is constant or number). GCLC
draws arcs segment by segment and by this command every third segment
will not be drawn, so the length of dashes by command circleprecision.
• drawdasharc_p The same as drawdasharc, but
always draws the arc in positive (counterclockwise) direction.
• drawellipse Generates commands for drawing the ellipse determined by center and two points and
, such that a line determined by points and is
one of the ellipse’s axis. GCLC draws ellipses segment by segment. The
number of segments can be changed by the circleprecision command.
• drawdashellipse Generates commands for
drawing the dashed ellipse determined by center and two points
and , such that a line determined by points
and is one of the ellipse’s axis. Picture of ellipse is made of dash
segments. GCLC draws circles and ellipses segment by segment and for
this dash command every third segment will not be drawn, so the length
of dashes can be changed by the circleprecision command.
• drawellipsearc Generates commands
for drawing the arc (with a starting point ) of the ellipse determined by center and two points and , such that
a line determined by points and is one of the ellipse’s
axis and is the measure of the angle ( is constant or number).
There is a similar command drawellipsearc1.
• drawdashellipsearc Generates commands
for drawing the arc (with a starting point ) of the ellipse determined by center and two points and , such that
a line determined by points and is one of the ellipse’s axis

3.5 Drawing Commands

and is the measure of the angle ( is constant or number). GCLC
draws arcs segment by segment and in this arc every third segment will not
be drawn, so the length of dashes can be changed by the circleprecision
command. There is a similar command drawdashellipsearc1.
• drawellipsearc1 Generates commands for drawing the arc (with a starting point ) of the ellipse
determined by center and two points and , such
that a line determined by points and is one of the ellipse’s axis and is the measure of the angle ( is constant or constant).
• drawdashellipsearc1 Generates commands for drawing the arc (with a starting point ) of
the ellipse determined by center and two points and
, such that a line determined by points and is
one of the ellipse’s axis and is the measure of the angle ( is constant or number). GCLC draws arcs segment by segment and in this
arc every third segment will not be drawn, so the length of dashes can be
changed by the circleprecision command.
• drawellipsearc2 Generates commands for drawing the elliptical arc X Y, where X and Y are points on the
ellipse determined by the points , the angle
X is equal to n1, and the angle Y X is equal
to n2.
• drawdashellipsearc2 Generates commands for drawing the elliptical arc X Y, where X and Y are
points on the ellipse determined by , the angle
X is equal to n1, the angle Y X is equal to
n2. GCLC draws arcs segment by segment and in this arc every third
segment will not be drawn, so the length of dashes can be changed by the
circleprecision command.
• drawbezier3 Generates commands for drawing the quadratic Bézier curve determined by points , ,
(it goes from to , while is a control
point). GCLC draws Bézier curves segment by segment. The number of
segments can be changed by the bezierprecision command.
• drawdashbezier3 Generates commands for
drawing the quadratic Bézier curve determined by points , ,
(it goes from to , while is a control
point). GCLC draws Bézier curves segment by segment and in this mode
every third segment will not be drawn, so the length of dashes can be
changed by the bezierprecision command.
• drawbezier4 Generates commands
for drawing the cubic Bézier curve determined by points , ,
, (it goes from to , while and

3 GCLC Language
are control points). GCLC draws Bézier curves segment by segment. The number of segments can be changed by the bezierprecision
command.
• drawdashbezier4 Generates commands for drawing the cubic Bézier curve determined by points ,
, , (it goes from to , while
and are control points). GCLC draws Bézier curves
segment by segment and in this mode every third segment will not be
drawn, so the length of dashes can be changed by the bezierprecision
command.
• drawpolygon Generates commands for drawing the
regular polygon determined by center , one vertex , and
number of sides ( is constant or number).
• drawtree Generates commands for drawing the tree with the given point as a root.
The numerical parameters and give the width and height of
the tree (in millimeters), determines the style for drawing tree, and
gives a rotation angle (in degrees) with the root as a center, and
a vertical, top-down direction as a reference direction (corresponding the
angle 0◦ ). There are four drawing styles (1, 2, 3 and 4).
A tree description is of the form { node_name ... .
All node names are printed in appropriate positions. If a tree node should
not be labelled, its name should start with the symbol _. Empty subtree,
written { } is not drawn or labelled, but it takes one position of subtrees
in the same level.
All tree nodes are defined as points and get names built from the name
of the reference point and their label. In the example given below, one
can use points Proot, Pleft, etc.
Example:
drawtree P 90 70 1 10
{
root
{ left
{ }
{ left-right }
}
{ right
{ _
{ a }
{ b }
{ c }
}
{ right-right }
}
}

3.5 Drawing Commands

• drawgraph_a
Generates commands for drawing the graph using the arc-layered method.1
The given reference point will be the center of the graph image.
The numerical parameter gives the width of the graph image, while
gives a rotation angle (in degrees) with the point as the
center.
The list of nodes is of the form
{ node_name1 node_name2 ... node_name_n }. All node names in the
figure are printed in left-top positions. If a graph node should not be
labelled, its name should start with the symbol _.
The list of edges is of the form
{ node_name1_1 node_name1_2 ... node_name_n_1 node_name_n_2 },
where all node names must already appear in the list of nodes.
If the graph is not connected, then none of its nodes or edges will not be
drawn.
All graph nodes are defined as points and get names built from the name
of the reference point and their label. In the example given below, one
can use points P_a, Pb, etc.
Example:
point P 30 50
drawgraph_a P 40 0
{ _a b c d e }
{
_a b
_a c
_a d
b d
b e
}

• drawgraph_b Generates commands for drawing the graph using the barycenter method. The given
reference name is used just to identify graph nodes, it does not need
to refer to any point or other object.
The list of nodes is of the form
{ node_name1 p_id1 node_name2 p_id2 ... node_name_n p_id_n}.
The node names represent the names of the graph nodes, while the point
identifiers associate graph nodes to already defined points. If a graph
node is not initially associated to an already defined point, then the point
identifier should be _, or can begin with _. The set of used defined points
(serving as fixed nodes) must form a convex polygon.
All node names in the figure are printed in left-top positions. If a graph
node should not be labelled, its name should start with the symbol _.
1 The

main author of support for graph drawing is Luka Tomašević (University of Belgrade).

3 GCLC Language
The list of edges is of the form
{ node_name1_1 node_name1_2 ... node_name_n_1 node_name_n_2 },
where all node names must already appear in the list of nodes.
If the graph is not connected, then none of its nodes or edges will not be
drawn.
All graph nodes are defined as points and get names built from the name
of the reference point and their label. In the example given below, one
can use points P_a, Pb, etc.
Example:
point A 80 50
point B 100 50
point C 90 55
drawgraph_b G
{ _a A
b B
c C
d _
}
{
_a b
_a c
_a d
b d
b c
}

• filltriangle Fills the triangle determined
by the given points with the current color. This command is ignored when
exporting to the simple LATEX format.
• fillrectangle Fills the rectangle determined by the
given points ( is the left-bottom corner, p_id2 is the right-top
corner) with the current color. This command is ignored when exporting
to the simple LATEX format.
• fillcircle Fills the circle with the current color. This
command is ignored when exporting to the simple LATEX format.
• fillcircle Fills the circle determined by the given
points ( is the center, p_id2 lies on the circle) with the current
color. This command is ignored when exporting to the simple LATEX format.
• fillellipse Fills the ellipse determined by
the given points ( is the center, is one of the
ellipse’s axis) with the current color. This command is ignored when
exporting to the simple LATEX format.

3.6 Labelling and Printing Commands

• fillarc Fills the circular arc determined by the
given points ( is the center, p_id2 lies on the circle, n is the
measure of the angle) with the current color. This command is ignored
when exporting to the simple LATEX format.
• fillarc0 The same as fillarc, except that the
area determined by the circle center and the arc endpoints is not filled.
• fillellipsearc Fills the elliptical arc
determined by the given points ( is the center of the ellipse with
axes parallel to coordinate axes, is the half-width, is the halfheight of the ellipse, n3 is the start central angle, and n4 is the measure
of the angle that corresponds to the arc). This command is ignored when
exporting to the simple LATEX format.
• fillellipsearc0 This command has the
same effect as fillellipsearc, except that the area determined by the
ellipse center and the arc endpoints is not filled.

3.6

Labelling and Printing Commands

• cmark Denotes the given point by a small empty circle (with radius 0.4mm) at its coordinates.
• cmark_lt
cmark_l

cmark_lb
cmark_t

cmark_b

cmark_rt
cmark_r

cmark_rb
Generates commands for denoting the given point by its name and by
small empty circle (with radius 0.4mm) at its coordinates. The name of
the point is written (in LATEX mode — in size \footnotesize) in one of
eight directions (left-top, left, left-bottom, top, bottom, right-top, right,
right-bottom).
• mark Generates commands for printing the name of the given
point at its coordinates (without denoting it by a circle).
• mark_lt
mark_l

mark_lb
mark_t

mark_b

mark_rt

3 GCLC Language
mark_r

mark_rb
Generates commands for printing the name of the given point at its coordinates (without denoting it by a circle) in one of eight directions. These
commands could be used for denoting lines and circles, too (of course,
first, some point with a line or circle name has to be defined).
• printat
Generates commands for printing given text
at coordinates of the given point. Text must begin with symbol { and
end with symbol }. These two symbols are not part of the text and will
not be printed. Text can have at most 100 characters. Text can include
all characters including {, } and blank space. In LATEX mode, the text is
printed in math mode, so for ordinary text, LATEX command \mbox{...}
should be used.
printat_lt
printat_l

printat_lb
printat_t

printat_b

printat_rt
printat_r

printat_rb
Generates commands for printing given text in one of eight directions with
respect to the given point. Example:
printat_l A {A=S_a(B) \mbox{($a$ is the bisector of $AB$)}}
will generate a command for printing the given text left from the point A.
• printvalueat Generates commands for printing value of a
given object at coordinates of the given point . The object
can be of any type. The value is printed in the format given in
Section 2.4. In LATEX mode, the text is printed in math mode, so for
ordinary text, LATEX command \mbox{...} should be used.
printvalueat_lt
printvalueat_l

printvalueat_lb
printvalueat_t

printvalueat_b

printvalueat_rt
printvalueat_r

printvalueat_rb
Generates commands for printing value of a given object in one of
eight directions with respect to the given point . Example:
printvalueat_b A A

3.7 Low Level Commands

will generate a command for printing the coordinates of the point A on
bottom from the point A.

3.7

Low Level Commands

• % A comment is marked by the symbol % (like in TEX). Characters in the
line after the symbol % will not be read.
• dim Defines dimensions of the picture. This command can
be at any position in the figure description file. If there is more than
one occurrence of this command, only the first one is used. The default
dimensions of a picture are 140mm×100mm. The rectangle defined by
this command also defines the visible area.
• area Defines the visible area of the picture. The
area is defined by the lower-left corner (the first two numbers) and its
upper-right corner (the second pair of numbers). There is always at most
one active area. All objects are clipped with respect to the active, current
area. If there is no defined area, the default area is the whole of the
picture.
• color Changes the current color. The parameters are
rgb (red/green/blue) components of the color. Each of them should
range between 0 and 255. For instance, 255 0 0 defines (pure) red color,
0 255 0 defines (pure) green color, 0 0 255 defines (pure) blue color,
255 255 0 defines yellow, 255 0 255 defines magenta, 0 255 255 defines
cyan, 127 127 127 defines grey color, 0 0 0 defines black and 255 255 255
white color.
Figures using this command exported to LATEX require using the package
color in your LATEX document. Note that this support for colors might
not work properly in conjunctions with some LATEX distributions (i.e.,
with some dvi drivers).
• background Sets the background color. The parameters
are rgb (red/green/blue) components of the color. This command is
ignored when exporting to the simple LATEX format.
• fontsize Changes the current font size. Font size is given in pts.
The default value is 8. In export to LATEX, this command can change the
current fontsize to one of the values: \tiny (1pt-5pt), \scriptsize (6pt7pt), \footnotesize (8pt), \small (9pt), \normalsize (10pt), \large
(11pt-12pt), \Large (13pt-14pt), \LARGE (15pt-17pt), \huge (18pt-20pt),
\Huge (over 21pt).
• arrowstyle Defines a shape of arrows drawn by the
command drawarrow. The angle between outer line segments in arrows
is given, in degrees, by (the default value is 15◦ , maximal value is
180◦ ). The length of outer line segments is given, in millimeters, by
(the default value is 3). Inner line segments meet the central line at the
point that is determined by — if X is the intersection of the central
line with the line determined by the endpoints of the outer line segments,

3 GCLC Language
if Y the point where the inner line segments meet the central line, and if
Z is the endpoint of the arrow, then XY /XZ = (the default value
is 0.667).
• circleprecision When exporting to LATEX, GCLC draws circles
and ellipses segment by segment. The default value is 72 segments for
a circle of a radius 10mm, more for larger circles (while there is linear
dependency). The number of segments can be changed by this command.
It will linearly depend on the circle radius, but it will be no less than the
given value . This command is irrelevant for export into formats other
than LATEX.
• bezierprecision GCLC draws Bézier curves segment by segment.
The default value is 36 segments for a curve. The number of segments can
be changed by this command.
• linethickness The line thickness can be changed by this command.
Thickness is expressed in millimeters. The default value is 0.16mm. If the
given value is negative, then the line thickness is product of the absolute
value of the argument and the default value.
• double This command makes all subsequent lines to be drawn with double
thickness.
• normal This command makes all subsequent lines to be drawn with normal
thickness.
• dash The length of dash lines (in dash drawn lines and line segments)
can be changed by this command. Length is expressed in millimeters.
The default value is 1.5mm. The length of space between dash lines is
/2. This command cancels the effect of previous dash and dashstyle
commands.
• dashstyle This command provides more expressive way of describing dashed lines and segments layout than given by the
command dash. The pattern defined by this command is as follows:
dash line — empty space — dash line — empty space. All
lengths are expressed in millimeters. The default values are: 1.5 0.75 1.5
0.75. This command cancels the effect of previous dash and dashstyle
commands.
• dmc The distance between point and its name or associated text can
be changed by this command. The default value is 1mm.
• mcr The radius of circle marking point can be changed by this command. The default value is 0.4mm.
• mcp When exporting to the simple LATEX format, draws circles marking points segment by segment. The default value is 9 segments for a
circle. The number of segments can be changed by this command. This
command is irrelevant for export into formats other than LATEX.

3.8 Cartesian Commands

• mcp When exporting to the simple LATEX format, draws circles marking points segment by segment. The default value is 9 segments for a
circle. The number of segments can be changed by this command. This
command is irrelevant for export into formats other than LATEX.
• export_to_latex {} When exporting to the simple LATEX format,
PSTricks LATEX format, or TikZ LATEX format, the given text is directly
exported to the output file (normally this should be a sequence of LATEX
commands).
• export_to_latex {} When exporting to the simple LATEX format,
PSTricks LATEX format, or TikZ LATEX format, the given text is directly
exported to the output file (normally this should be a sequence of LATEX
commands).
• export_to_simple\_latex {} When exporting to the simple LATEX
format, the given text is directly exported to the output file.
• export_to_pstricks {} When exporting to PSTricks LATEX format, the given text is directly exported to the output file.
• export_to_tikz {} When exporting to TikZ LATEX format, the
given text is directly exported to the output file.
• export_to_eps {} When exporting to eps format, the given text
is directly exported to the output file.
• export_to_svg {} When exporting to svg format, the given text
is directly exported to the output file.

3.8

Cartesian Commands

• ang_picture Defines a rectangular area for Cartesian picture (ang is from “ANalytical Geometry”). The first two parameters determine its lower left corner, and last two parameters determine its
upper right corner. If there is no defined area, the default area is empty
(i.e., it is defined by lower left and upper right corner equal to (0, 0)). This
area is relevant only for Cartesian commands (ang_...).
• ang_origin Defines an origin of the coordinate system. The
default value is (0, 0).
• ang_unit Defines the unit of the coordinate system in millimeters.
The default value is 10mm.
• ang_scale Defines the scale between y and x coordinates.
The parameter determines if the coordinate system is regular (value
1) or logarithmic (value 2). In logarithmic system, x axis is set on y = 1.
The parameter determines the multiplication factor for y coordinates.
It must be positive. If a negative value or zero is given, the value 1 is
assumed.

3 GCLC Language
These values determines the coordinate system and all consequent drawings. The default values are 1 and 1.
Note that, if logarithmic system is used, the commands doing with lines
(ang_tangent, ang_drawline, ang_drawline_p) will not work properly.
Other commands (including, for instance, commands ang_drawdashconic
and ang_draw_parametric_curve) can be used.
• ang_drawsystem_p
for drawing coordinate axes.

Generates commands

The parameter controls denoting the integer points on the axes: with
parameter value 1, integer points are denoted by small circles, with value
2 by small dashes, and with value 3 they are not denoted at all.
The parameter controls the step for denoting integer points on x
axis. For instance, if is equal to 1, then each integer point on x axis
is denoted (in a way defined by the parameter ); if is equal to
2, then every second integer point is denoted.
The parameter controls the step for denoting integer points on y
axis.
The parameter controls denoting the axes: with parameter value
1, the axes are denoted by x and y, and with value 2 the axes are not
denoted.
The parameter controls drawing arrows at the endpoints of the system: with parameter value 1, there are arrows at both positive and negative endpoints, with parameter value 2, there are arrows only at positive,
and with parameter value 3, there are no arrows at all.
This command can replace all other variants of ang_drawsystem... commands (however, they are kept for simplicity and for the reasons of vertical
compatibility).
• ang_drawsystem Generates commands for drawing the axes and denotes
(by small circles) integer points on them.
• ang_drawsystem0 Generates commands for drawing the axes and doesn’t
denote integer points on them.
• ang_drawsystem1 Generates commands for drawing the axes and denotes
by small dashes integer points on them.
• ang_drawsystem_a Same as ang_drawsystem, but denotes the axes by x
and y.
• ang_drawsystem0_a Same as ang_drawsystem0, but denotes the axes by
x and y.
• ang_drawsystem1_a Same as ang_drawsystem1, but denotes the axes by
x and y.
• ang_point Definition of an ang point. A difference
from the standard command point is that the ang_point command introduces point by coordinates given with respect to a defined origin and
unit of Cartesian system.

3.8 Cartesian Commands

• ang_getx The object with the specified identifier
becomes number and gets the value of the x-coordinate of the given point
in the active Cartesian system ( was not necessarily defined
by the command ang_point).
• ang_gety The object with the specified identifier
becomes number and gets the value of the y-coordinate of the given point
in the active Cartesian system ( was not necessarily defined
by the command ang_point).
• ang_line Introduces a line by given parameters in the form ax + by + c = 0, with respect to a defined origin and
unit.
• ang_conic Definition of
a conic. A conic is determined by the given parameters a, b,
c, d, e and f in the following form: ax2 + 2bxy + cy 2 + 2dx + 2ey + f = 0,
with respect to a defined origin and unit. An object defined in such a
manner gets type conic, and can not be used as number, point, line
or circle (unless its type is changed by another definition).
• ang_intersec2
ang_intersec2
Objects with specified identifiers and become points and
get coordinates of the intersection of a given line and a conic, or of a given
conic and line. If there is just one intersection point, then both and
have the same value. If there are no intersection points, then the
program reports a run-time error.
The full name, ang_intersec2, can also be used for this command.
• ang_tangent Introduces a line which
is tangent to a conic at a point .
• ang_drawline Generates commands for drawing a line
within the defined area.
• ang_drawline_p Generates commands for drawing the
line determined by points and , within the defined area.
• ang_drawconic
Generates commands for drawing the conic .
• ang_drawdashconic
Generates commands for drawing the conic and made of dash
segments. GCLC draws conics segment by segment and by this command
every third segment will not be drawn, and you can change length of dash
segments by the command ’conicprecision’. The default number of
segments is 144 on x-axis.
• ang_draw_parametric_curve
{;;}{;}

3 GCLC Language
The object with the specified identifier becomes number and serves
as a (iterating) curve parameter. A curve is being drawn in iterations.
is the initial value for the parameter, is the (while) condition that the (changing) parameter has to meet, and is the expression for recalculating the parameter in each iteration. The pair ,
determines the pair (x, y) of coordinates of a point on the curve.
In building expressions, one can use the same functions, operators and
relations as in command expression, described in §3.4.
Examples:
ang_draw_parametric_curve x {-5;x<10;x+0.1}{x;x*sin(x)}
ang_draw_parametric_curve t {0;t<30;t+0.3}{sin(t)*t;-cos(t)*t}
The curve drawing is reset if in some iteration an undefined expression is
encountered. For instance,
ang_draw_parametric_curve x {-5;x<10;x+0.1}{x;d/x}
will produce two pieces of a line with the discontinuity point at (0, 0).
However,
ang_draw_parametric_curve x {-5;x<10;x+0.3}{x;d/x}
will produce a single line since the discontinuity point (0, 0) is missed. The
system does not determine parameter values for which a resulting point
is undefined, but can only detect such situation if encountered in some
iteration. However, in order to provide expected output, the system does
not draw segment between subsequent point on the line if both of them
are out of the picture area.
As explained above, the system skips points in which expressions giving
(x, y) is not defined. So, it is not reported if one of these expressions is not
defined in some iterations. Moreover, it is also not reported if expressions
involve undefined functions or are ill-formed. Because of that, in case of
a problem, it is a good practice to check the expressions separately, as
arguments to the expression command.
• ang_conicprecision GCLC draws conics segment by segment. The default value is 144 segments on x-axis. This number can be changed by
this command.
• ang_plot_data { } Draws the graph
of the function given by its points. The number is equal to 0 if the
points are not to be denoted, and is equal to 1 if the points are to be
denoted by small circles. The points are given as a sequence of their
coordinates.
Example:
ang_plot_data 1
{
1.0 1.0
2.0 1.0
3.0 2.0
}

3.9 3D Cartesian Commands

3.9

3D Cartesian Commands

• ang3d_picture Defines a rectangular area for 3D
Cartesian picture. The first two parameters determine its lower left corner,
and last two parameters determine its upper right corner. If there is no
defined area, the default area is empty (i.e., it is defined by lower left and
upper right corner equal to (0, 0)).
• ang3d_origin Defines a 3D Cartesian coordinate
system, shown using normal projection. and give a position of
the origin of the system. The default value is (0, 0). and give
the angles (in radians) that determine the viewing angle to the coordinate
system. In the default position of the system, x axis is screen-horizontal
with respect to the screen, y axis is perpendicular to the screen, z axis is
screen-vertical. This default position corresponds to the values 0 and 0
of and . For other values, the rotation around the z axis, for
radians, is first applied (the new and the old x axes build the angle
). After that, the rotation around the default x axis, for radians
is applied (the new and the old z axes build the angle ).
• ang3d_unit Defines the unit of the coordinate system in millimeters.
The default value is 10mm.
• ang3d_scale Defines the scale between y and x coordinates and between z and x coordinates.
The parameter determines if the coordinate system is regular (value
1) or logarithmic (value 2). In logarithmic system, x and y axes are set
on z = 1.
The parameter determines the multiplication factor for y coordinates.
It must be positive. If a negative value or zero is given, the value 1 is
assumed.
The parameter determines the multiplication factor for z coordinates.
It must be positive. If a negative value or zero is given, the value 1 is
assumed.
These values determines the coordinate system and all consequent drawings. The default values are 1, 1, and 1.
Note that, if logarithmic system is used, the commands doing with lines
will not work properly.
• ang3d_axes_drawing_range Sets the
range for drawing awes. On x axis the interval [¡n1¿ ¡n2¿] will be drawn,
on y axis the segment [¡n3¿ ¡n4¿], and on z axis the segment [¡n5¿ ¡n6¿].
This command should be used before drawing the system (i.e., before the
command ang3d_drawsystem_p.
• ang3d_drawsystem_p Generates commands for drawing coordinate axes.
The parameter controls denoting the integer points on the axes: with
parameter value 1, integer points are denoted by small circles, with value
2 by small dashes, and with value 3 they are not denoted at all.

3 GCLC Language
The parameter controls the step for denoting integer points on x
axis. For instance, if is equal to 1, then each integer point on x axis
is denoted (in a way defined by the parameter ); if is equal to
2, then every second integer point is denoted.
The parameter controls the step for denoting integer points on y
axis.
The parameter controls the step for denoting integer points on z
axis.
The parameter controls denoting the axes: with parameter value 1,
the axes are denoted by x, y, and z, and with value 2 the axes are not
denoted.
The parameter controls drawing arrows at the endpoints of the system: with parameter value 1, there are arrows at both positive and negative endpoints, with parameter value 2, there are arrows only at positive,
and with parameter value 3, there are no arrows at all.
• ang3d_point Definition of an ang3d point by
coordinates in the current 3D Cartesian system.
• ang3d_getx The object with the specified identifier
becomes number and gets the value of the x-coordinate of the given point
in the 3D Cartesian system (and it gets the value 0 if was
not defined by the command ang3d_point).
• ang3d_gety The object with the specified identifier
becomes number and gets the value of the y-coordinate of the given point
in the 3D Cartesian system (and it gets the value 0 if was
not defined by the command ang3d_point).
• ang3d_getz The object with the specified identifier
becomes number and gets the value of the z-coordinate of the given point
in the 3D Cartesian system (and it gets the value 0 if was
not defined by the command ang3d_point).
• ang3d_drawline_p Generates commands for drawing
the line determined by points and , within the defined
area.
• ang3d_draw_parametric_surface
{;;}
{;;}
{;;}
This commands draws a surface given by two parameters. The objects
with the specified identifiers and become numbers and serve
as a (iterating) surface parameters. A surface is drawn in iterations. For
the first parameter (id1), is the initial value, is the (while)
condition that the (changing) parameter has to meet, and is the
expression for recalculating the parameter in each iteration. For the second parameter (id2), is the initial value, is the (while)
condition that the (changing) parameter has to meet, and is the

3.10 Layers

expression for recalculating the parameter in each iteration. The triple
, , determines the triple (x, y, z) of coordinates of
a point on the surface. In building expressions, one can use the same
functions, operators and relations as in command expression, described
in §3.4.
Example (drawing a torus):
ang3d_draw_parametric_surface u v
{0; u<=6.43; u+0.15}
{0; v<=6.43; v+0.15}
{ (4+2*sin(v))*cos(u); (4+2*sin(v))*sin(u); b*cos(v) }

Drawing of the surface is reset if in some iteration an undefined expression
is encountered (see explanation for ang_draw_parametric_curve command)
• ang3d_draw_parametric_curve
{;;}{;;}
The object with the specified identifier becomes number and serves
as a (iterating) curve parameter. A curve is being drawn in iterations.
is the initial value for the parameter, is the (while) condition that the (changing) parameter has to meet, and is the expression for recalculating the parameter in each iteration. The triple ,
, determines the triple (x, y, z) of coordinates of a point
on the curve. In building expressions, one can use the same functions,
operators and relations as in command expression, described in §3.4.
Example:
ang3d_draw_parametric_curve u
{0; u<=5; u+0.05}
{ u*sin(u*u); u*cos(u*u); u }

Drawing of the curve reset if in some iteration an undefined expression
is encountered (see explanation for ang_draw_parametric_curve command)

3.10

Layers

• layer Declares the layer: all subsequent drawing, labelling commands, commands for changing color or line thickness, etc. will be considered to belong to this layer. Layers are irrelevant for construction
commands. The parameter can have values between 0 and 1000.
• hide\_layer Hides contents of the layer will not be shown. The
parameter can have values between 0 and 1000.
• hide_layers_from Hides contents of all layers higher than , including the layer .

3 GCLC Language
• hide_layers_to Hides contents of all layers lower than , including
the layer .

3.11

Support for Animations

Animations are supported in GUI version of GCLC version only.
Within animations, the entire gcl descriptions runs for every frame. The
only difference between frames occurs with moving points. If the animation is
defined to have, say, 100 frames, then there will be 100 runs of the script with
100 tuples of values for moving points. The first run (giving the first frame) will
give the output for the initial values for all points. The 100th run will give the
output for the ending values for all points. Each moving point moves uniformly
and linearly from its initial to its ending position. Having all frames built, they
are just shown one by one.
• animation_frames Defines the total number of frames in the
animation and the number of frames per second. The default value for the
total number of frames is 0. This command is ignored when producing
e.g.,LATEX or bitmap images. The command is used only in animation
mode in WinGCLC version. In other modes/releases this command has
no effects.
This command should not be used within while-blocks.
• point This is a five-arguments version of
the point command. The point will move from the position determined
by the first pair of coordinates to the position determined by the second
pair of coordinates. The command is used in this form only in animation
mode in the GUI version. In other modes, the last two arguments are
ignored.
trace Defines the point for which the trace (or
locus) will be drawn during the animation. The three given numbers give
rgb components of the color for the trace.
The command is used only in animation mode in the GUI version. In
other modes/releases this command has no effects.
Tracing spans all animation frames so it can have only a global scope.
Thus, it is ignored if invoked within an user-defined procedure or a conditional block of commands.
Traces for a selected frame are also exported to output files.

3.12

Support for Theorem Provers

Theorem proving is supported in both the command-line and in GUI version.
There are several automated theorem provers built-in GCLC, the specific prover
is selected either by a command line parameter (for GCLC) or by appropriate
button (in the GUI version).
• prove { } After the processing of construction description,
the theorem prover will be called on the given statement. The output of

3.12 Support for Theorem Provers

the prover will be exported to LATEX format or to xml format, in the
current directory.
• prooflevel Controls the output level of the prover. A level can be
an integer between 0 and 7. The default value is 1.
• prooflimit Controls the maximal number of proof steps. The default
value is 10000.
• prover_timeout Sets the time (in seconds) available to the prover.
The default value is 10 seconds.
• theorem_name Sets the name of the theorem (it is used in prover’s
output documents).
More detailed description of the build-in theorem provers are given in Chapter 6.

3 GCLC Language

Chapter 4

Graphical User Interface
The graphical user interface for GCLC does not provide only a a new, userfriendly interface, but also introduces some features which are not available in
command-line version (e.g., moving points, building and playing animations,
tracing points, watch window etc). It is a kind of an “Integrated Development
Environment” or IDE for GCLC.

4.1

An Overview of the Graphical Interface

The graphical interface consists of these main parts (see Figure 4.1):
1 Editor window.
2 Picture window
3 Debug/Log window
4 Menus and toolbar
5 Status bar
6 Watch window

Editor window is provided here for writing source files (i.e., descriptions of a
geometric construction) in it. It has standard features which are expected
from an text editor, find/replace, and some additional features like coloring
syntax and error/warning locating.
The Picture window is used for showing the processed figure. One can interactively work in this window by selecting and moving fixed points, zooming
the picture, etc. (Note: “Fixed point” is a point defined by gcl command
point.)
Debug/Log window is a notifying window. It displays messages about the
status of the most recent operation such as compiling, exporting etc.

4 Graphical User Interface

Figure 4.1: Screenshot of the program with GUI
Menus and toolbars are standard parts of almost every program with GUI
program. There is a standard menu with a toolbar that provides shortcuts
for menu items. Most items on the menu have an equivalent on some
toolbar. The menu items can also be activated by appropriate keyboard
shortcuts — for instance, Build (compiles a picture or builds animation)
can be activated by the keys Ctrl+B.
• The toolbar has a number of items, including those for creating,
opening and saving files, for zooming picture in and out, for theorem proving (for turning on and off the prover based on the area
method, for turning on and off the prover based on Wu’s method, for
turning on and off the prover based on Gröbner bases method, for
turning deduction control on and off, for generating proofs in LATEX,
for generating proofs in xml.
• The status bar displays some real-time information like current line
and column in editor window, current x and y coordinates of the
mouse pointer in the picture window, whether the file has been saved
or processed, and the zoom factor.

4.2

Features for Interactive Work

Creating/Opening: In the beginning, one can created a new or open an existing *.gcl file. From the File menu, select the item New and the blank
new document window should appear. Type a few gcl commands in the
editor window. For instance, try this set of commands:
point A 20 20

4.2 Features for Interactive Work

point B 90 30
point C 40 90
drawsegment A B
drawsegment B C
drawsegment C A
cmark_b A
cmark_b B
cmark_t C
If you are not familiar with gcl, explore some of the samples and learn
about commands of gcl.
Editing: You can type gcl commands in the editor window just like in any
other programming language.
Building: After entering of the source, select the item Build from the Picture
menu and start the compilation and building of the picture. If there were
no errors, a figure corresponding to the description given by the source
code will appear in the picture window (see Figure 4.2).

Figure 4.2: After building the image
Modifying the picture: Modifying the figure can be achieved by editing the
source manually (which gives more control over the picture), or by moving
“free” points directly on the picture. After successful compilation, you can
select the item Show Free Points from the Picture menu. Now, every free
point will have a green circular mark which can be selected (picked-up)
and dragged to another position (also changing the coordinates of the
point in the editor). In a similar way, destination points for animations
can be dragged (while they have orange circular marks) (see Figure 4.3).
Export: GUI GCLC can export a compiled picture (or a particular frame from
an animation) to the following formats:

4 Graphical User Interface

Figure 4.3: Moving a fixed point
• simple LATEX format (supported by gclc.sty
• PSTricks LATEX format
• TikZ LATEX format
• Bitmap
• eps (Encapsulated PostScript)
• svg (Scalable Vector Graphics)
• raster formats: bitmap, PNG, JPG
• xml (textual description of the figure given as xml file).
Also, an animation can be exported to a sequence of bitmaps (which can
be further used for making animations by some other tool). These features
are available in the File/Export menu. More about export options can be
found in Chapter 5.
Import: GUI GCLC can import JavaView .jvx files. This feature is available
in the File/Import from menu.
Theorem proving: Options for the built-in theorem proving can be accessed
via the option group Source or via the Source toolbar. If the source file
contains a conjecture, GCLC will automatically invoke the built-in theorem prover, if the option Theorem proving is checked (i.e., if this button
is turned on). If the option Deductive control is checked, when a run-time
error occurs (during processing the source), GCLC will run the prover
to check whether this error occurs in all situations (i.e., whether it is a
deductive consequence of the given construction) (see Section 6.7). Theorem prover can generate proofs in LATEX and in xml form. If at least
one of the options Theorem proving and Deductive control is checked, then
the options Generate Proofs in LATEX and Generate Proofs in xml can
be selected. If neither of these two options were selected, then the prover
works without generating files with the proofs. More about the theorem
proving and the deduction control can be found in Chapter 6.

4.2 Features for Interactive Work

Miscellaneous: GUI GCLC provides some additional useful features, including
• Watch window: Gives information about type and values of specified
objects in the generated picture or in any particular animation frame.

4 Graphical User Interface

Chapter 5

Exporting Options
On the basis of a (valid) figure description in the file in.gcl, a figure can be
generated by the command-line version of GCLC using the following command:
> gclc in.gcl out.pic -option
where out.pic is the name of a resulting file (it can have any extension, not
necessarily .pic), and -option controls the output format. If the option is
omitted, the output format is the simple LATEX format (supported by gclc.sty).
For PSTricks LATEX format, -pst is used, for TikZ LATEX format, -tikz is used,
for eps, -eps is used, for svg, -svg is used, and for xml, the option -xml is
used. Command line version of GCLC does not support export to bitmap.
Within the GUI version of GCLC, a picture exported in some of supported
formats can be obtained by selecting one of the option available in the group
File/Export to... (see Chapter 4). When exporting a particular frame from an
animation, traces are also saved to output files.
File exported to vector formats (LATEX, svg, xml) contain comments —
explanations for portions of code for easier understanding and modifying.
By using the export_to... GCLC commands, arbitrary text can be exported directly to files containing specific vector formats (LATEX, svg, xml).
Note that mathematical formulae written within a GCLC file will be formatted properly only when exported to LATEX formats. If a figure is exported
to, say, eps format, it will not have properly formatted formulae. In order to
obtain an eps file with properly formatted formulae, one must first export the
file to LATEX, then process a LATEX file that contains only this figure, then export
the obtain document to a ps document, and then finally, convert the ps to a
eps file.
When exported to LATEX, the text is printed in math mode and in the size
footnotesize.

5.1

Export to Simple LATEX format

By ”simple export LATEX format“ we mean the format based on the gclc.sty
package. Good sides of this choice are: there is just one file required (gclc.sty),
it can be stored in standard folder for LATEX packages or in the current folder,
it can be easily shared with others to make LATEX documents portable, or it can

5 Exporting Options

even be copied to LATEX documents (since it is just few lines long). This package
insignificantly slows down processing LATEX documents that use it. Bad sides
of choosing this LATEX format are: in most systems producing pdf documents
has to be performed via PostScript format. In addition, this format does not
support some features of GCLC, like filling polygons.

5.1.1

Generating LATEX Files and gclc.sty

On the basis of a (valid) figure description in the file in.gcl, a picture in
LATEX format can be generated by the command-line version of GCLC using
the following command:
> gclc in.gcl out.pic
where out.pic is the name of a resulting file (it is not necessary for it to have
the extension .pic). If the extension of the input file is not given, then the
assumed extension is .gcl. If the name of the output file is not given, then the
assumed name is built from the input file name (e.g., in.pic).
Within the GUI version of GCLC, a picture exported in LATEX format can
be obtained by selecting the option File/Export to.../LaTeX.
The picture can be included in a LATEX document using the command:
\input{out.pic}
in appropriate position in your LATEX document.
The package gclc must be included (by \usepackage{gclc}) in the preamble of your document, or you can add the following lines in the preamble:
\def\gclcpicture#1{%
\def\gclcline##1##2##3##4##5##6##7{%
\put(##1,##2){\special{em:point #1##3}}%
\put(##4,##5){\special{em:point #1##6}}%
\special{em:line #1##3,#1##6,##7mm}}}
\gclcpicture{1}
If the command color is used in the gcl file, a LATEX document including
the corresponding picture (.pic file) should also use the package color.1

5.1.2

Changing LATEX File Directly

A position of the picture in your document can be changed by changing (within
any editor) appropriate parameters in the GCLC output file. For example,
\begin{picture}(140.00,100.00)
can be changed to
\begin{picture}(180.00,100.00)(10.00,10.00)
in order to change picture dimensions and its position. (All values in both input
and output file are expressed in units of 1 millimeter.)
1 For convenience, the package color.sty (developed by other authors), is distributed with
GCLC.

5.1 Export to Simple LATEX format

5.1.3

Handling More Pictures on a Page

If you want to put two or more pictures generated by GCLC on one page, you
might need to take care about point numbers, otherwise dvi... programs might
report the warning duplicate point numbers and only your first picture on a
page will be drawn correctly. This is so because (many) dvi programs can (in
an appropriate mode) address a limited number of points each of which has its
own index. These indices can go from 1 to 32767. If there are several pictures,
each of their points should have an index which is unique; indices of points in
different pictures thus could differ in the first digit. So, before each, there should
be one \gclcpicture command with the number of the picture (you can omit
\gclcpicture{1} before the first picture):
\input{sample1.pic}
\gclcpicture{1}
\input{sample2.pic}
This way, point indices are built by concatenating picture indices and original
point indices. Add command \gclcpicture{1} after a sequence of pictures
supposed to be on the same page. Note that if pictures have thousands of
points this approach can fail (for instance, if there are three pictures on a page,
each with 3000 points).
There is also another solution for this problem: GCLC can create pictures
with indices of points starting with a given number. Therefore, for example,
if GCLC reports Ending point number: 99 after successfully processing an
input file, starting point number for the second picture should be 100 or more:
> gclc in.gcl out.pic 100
If this parameter is omitted, the starting point number is 1.

5.1.4

Batch Processing

If GCLC (the command line version) is called the option -b, then the batch
processing is used. It expects a LATEX file with blocks of GCLC commands,
given in gclc environment, and it outputs a single LATEX file with GCLC
commands replaced by corresponding LATEX drawing commands (based on the
gclc.sty style). This output file then should be processed (only) by LATEX
processor. If the option -b is used, then all other options are ignored (the
theorem prover and deduction control are off, and only exporting to LATEX is
enabled).
The batch processing is used as in the following example:
> gclc in.tex out.tex -b
If the extension of the input file is not given, then the assumed extension is
.tex. If the option -b is used and if the name of the output file is not given,
then the assumed name is built from the input file name (e.g., in-gclc.tex).
For example, an input LATEX file (in.tex) can be

5 Exporting Options

\documentclass{article}
\usepackage{gclc}
\begin{document}
Here goes a triangle...
\begin{figure}[h]
\begin{gclc}
dim 100 35
point A 10 10
point B 80 10
point C 30 30
drawsegment A B
drawsegment A C
drawsegment B C
\end{gclc}
\caption{Triangle}
\end{figure}
...and here goes a parametric curve...
\begin{gclc}
dim 100 35
ang_picture 0 0 100 35
ang_origin 10 10
ang_drawsystem
ang_draw_parametric_curve x
{ 0; x<8; x+0.05}
{ x; sin(pow(x,2))*cos(x) }
\end{gclc}
\end{document}

5.2

Export to PSTricks LATEX format

PSTricks is a collection of PostScript-based TEX macros that is compatible with
LATEX (but also most TEX macro packages, including plaint TEX). It enables
creating high quality graphics in an inline manner. PSTricks package is not
distributed with GCLC.2 Good sides of PSTricks choice are: it is very popular,
very expressive, it is understandable and can be relatively easily modified by
hand. Bad sides of choosing this LATEX format are: it takes several megabytes,
it required installing dozens of LATEX packages, it is impossible to share LATEX
documents with those who do not have PSTricks installed, it slows down a bit
processing LATEX documents that use it, in order to produce pdf document, an
intermediate PostScript document has to be generated.
On the basis of a (valid) figure description in the file in.gcl, a picture in
PSTricks format can be generated by the command-line version of GCLC using
2 It

can be found on http://tug.org/PSTricks.

5.3 Export to TikZ LATEX format

the following command:
> gclc in.gcl out.pst -pst
where out.pst is the name of a resulting file. If the extension of the input file
is not given, then the assumed extension is .gcl. If the option -pst is used and
if the name of the output file is not given, then the assumed name is built from
the input file name (e.g., in.pst).
Within the GUI version of GCLC, a picture exported in PSTricks format
can be obtained by selecting the option File/Export to.../LaTeX-PSTricks.
A picture in PSTricks format can be included in a LATEX document using
the command:
\input{out.pst}
in appropriate position in your LATEX document or the whole picture in PSTricks
format can be copied to the document (the package pstricks must be included.
Batch processing is supported for this format. If GCLC (the command line
version) is called the option -b, then the batch processing is used. It expects a
LATEX file with blocks of GCLC commands, given in gclc environment, and it
outputs a single LATEX file with GCLC commands replaced by corresponding
LATEX PSTricks drawing commands. This output file then should be processed
(only) by LATEX processor. If the option -b is used, then all other options are
ignored (the theorem prover and deduction control are off).
The batch processing is used as in the following example:
> gclc in.tex out.tex -b -pst

5.3

Export to TikZ LATEX format

The pgf package (pgf is supposed to mean ,,portable graphics format“), is
a package for creating graphics in an inline manner. It defines a number of
TEX commands that draw graphics. TikZ is the natural frontend for pgf. It
gives access to all features of pgf, but it is intended to be easy to use. The
syntax is a mixture of metafont and pstricks and some additional ideas. The
pgf package, supporting TikZ format, is not distributed with GCLC.3 Good
sides of TikZ choice are: it is very expressive, it is understandable and can be
relatively easily modified by hand, it enables directly producing pdf documents
with figures directly from the LATEX source (there is no need for PostScript
intermediate step). Bad sides of choosing this LATEX format are: it takes several
megabytes, it required installing dozens of LATEX packages, it is impossible to
share LATEX documents with those who do not have pgf installed, it slows down
processing LATEX documents that use it.
On the basis of a (valid) figure description in the file in.gcl, a picture in
TikZ format can be generated by the command-line version of GCLC using the
following command:
> gclc in.gcl out.tkz -tikz
3 It

can be found on http://sourceforge.net/projects/pgf.

5 Exporting Options

where out.tkz is the name of a resulting file. If the extension of the input file
is not given, then the assumed extension is .gcl. If the option -tikz is used
and if the name of the output file is not given, then the assumed name is built
from the input file name (e.g., in.tkz).
Within the GUI version of GCLC, a picture exported in TikZ format can
be obtained by selecting the option File/Export to.../LaTeX-TikZ.
A picture in TikZ format can be included in a LATEX document using the
command:
\input{out.tkz}
in appropriate position in your LATEX document or the whole picture in TikZ
format can be copied to the document (the package tikz must be included).
Batch processing is supported for this format. If GCLC (the command line
version) is called the option -b, then the batch processing is used. It expects a
LATEX file with blocks of GCLC commands, given in gclc environment, and it
outputs a single LATEX file with GCLC commands replaced by corresponding
LATEX TikZ drawing commands. This output file then should be processed (only)
by LATEX processor. If the option -b is used, then all other options are ignored
(the theorem prover and deduction control are off).
The batch processing is used as in the following example:
> gclc in.tex out.tex -b -tikz

5.4

Export to Raster-based Formats and Export
to Sequences of Images

Within WinGCLC, there is available export to bitmap format (option File/Export
to.../LaTeX). The picture can be generated for the following resolutions 75, 150,
300 and 600 dpi. The new GUI version supports also export to JPEG and PNG
formats.
Within the GUI version, an animation can be exported to a sequence of
bitmaps (option File/Export to...) which can be further used for making animations by some other tool.

5.5

Export to eps Format

On the basis of a (valid) figure description in the file in.gcl, a picture in eps
(Encapsulated PostScript Format) format can be generated by the commandline version of GCLC using the following command:
> gclc in.gcl out.eps -eps
where out.eps is the name of a resulting file. If the extension of the input file
is not given, then the assumed extension is .gcl. If the option -eps is used and
if the name of the output file is not given, then the assumed name is built from
the input file name (e.g., in.eps).
Within the GUI version of GCLC, a picture exported in eps format can be
obtained by selecting the option File/Export to.../EPS.

5.6 Export to svg Format

A picture in eps format can be included in a LATEX document using the
command:
\includegraphics[width=0.5\textwidth]{out.eps}
in appropriate position in your LATEX document (the package graphicx must
be included (by \usepackage{graphicx}) in the preamble of your document).

5.6

Export to svg Format

On the basis of a (valid) figure description in the file in.gcl, a picture in
svg (Scalable Vector Graphics) format can be generated by the command-line
version of GCLC using the following command:
> gclc in.gcl out.svg -svg
where out.svg is the name of a resulting file. If the extension of the input file
is not given, then the assumed extension is .gcl. If the option -svg is used and
if the name of the output file is not given, then the assumed name is built from
the input file name (e.g., in.svg).
Within the GUI version of GCLC, a picture exported in svg format can
be obtained by selecting the option File/Export to.../SVG. A picture in svg
format can be directly open by modern web browsers. For more details about
xml and svg see Chapter 7.

5.7

Export to xml Format

On the basis of a (valid) figure description in the file in.gcl, a textual description as xml file can be generated by the command-line version of GCLC using
the following command:
> gclc in.gcl out.xml -xml
where out.xml is the name of a resulting file. If the extension of the input file
is not given, then the assumed extension is .gcl. If the option -xml is used and
if the name of the output file is not given, then the assumed name is built from
the input file name (e.g., in.xml).
Within the GUI version of GCLC, a figure description exported in xml
format can be obtained by selecting the option File/Export to.../XML. A figure
description in xml format can be directly open by modern web browsers. For
more details about xml and svg see Chapter 7.

5.8

Generating PostScript and pdf Documents

LATEX files with figures generated by GCLC should be normally converted to
dvi format (by the LATEX processor), and then to PostScript (by some dvi
to PostScript converter, e.g., dvi2ps).

5 Exporting Options

LATEX files with figures generated by GCLC might not properly get converted to pdf documents in some environments (neither by LATEX to pdf processor, nor by dvi to pdf converter, e.g., dvi2pdf). If this is the case, then first
produce the dvi file, then convert it to PostScript, and then, finally, to pdf
(by some PostScript to pdf converter, e.g., ps2pdf).

Chapter 6

Theorem Prover
There are three theorem provers built into GCLC:
• a theorem prover based on the Chou’s area method1 [3]; the prover produces traditional (i.e., geometric, not algebraic, coordinate-based), readable proofs; the proofs are expressed in terms of higher-level geometry
lemmas and expression simplifications.
• theorem provers based on the Wu’s method [12, 4] and on the Gröbner
bases method [1, 2];2 these provers are algebraic theorem provers; they are
based on manipulating polynomials and they do not produce traditional
geometrical proofs.
The theorem prover to be used is selected in the following way:
• in the command line version, by an appropriate parameter: -a for the
area method (default), -w for the Wu’s method, -g for the Gröbner bases
method.
• in the GUI version, the theorem prover is selected by checking appropriate
button in the toolbar or by checking the option Deduction Control.
All provers can prove a range of non-trivial theorems, including theorems
due to Ceva, Menelaus, Gauss, Pappus, Thales etc, but they are still a subject
of further improvements.
Support for the provers involves only a few commands:
• prove (for providing a conjecture);
• prooflevel (for setting the level of proof details);
• prooflimit (for setting maximal size of a proof).
• prover_timeout (for setting the timeout for the prover).
1 This theorem prover based on the area method was developed in collaboration with
prof. Pedro Quaresma, Department of Mathematics, University of Coimbra, Portugal. This
work was partially supported by CISUC/FCT, Centro International de Matemática (CIM),
under the programme “Research in Pairs”, while on visit to Coimbra University under the
Coimbra Group Hospitality Scheme.
2 The main author of these theorem provers is Goran Predović (University of Belgrade).

6 Theorem Prover
• theorem_name (for setting the theorem’s name).

The provers work in both command line version and in GUI version (and
they do not use any specific functionalities of the GUI). Proofs of theorems
can be generated in LATEX or in xml form and saved in a file. For the area
method, each deduction step is accompanied by its semantics counterpart —
corresponding numeric values in Cartesian plane.
The theorem provers are very efficient. Many conjectures are proved in
only milliseconds. However, some conjecture may take several seconds, several
minutes, or in some specific cases even several hours. The maximal number of
proof steps can be set by the command prooflimit. The default value is 10000
proof steps.3 If the prover perform more proof steps, the proving process is
stopped. Similarly, the time available to the prover (in seconds) can be set by
the command prover_timeout. The default value is 10 seconds.

6.1

Introductory Example

The theorem prover is tightly integrated into GCLC. This means that one
can use the prover to reason about a GCLC construction (i.e., about objects
introduced in it), without any required adaptations required for the deduction
process. Of course, only the conjecture itself has to be added.
The example GCLC code given in Figure 6.1 describes a triangle and midpoints of two of triangle’s sides. This GCLC code produces the Figure 6.2.
It holds that the lines AB and A1 B1 are parallel and this can be proved by
the theorem prover. The conjecture ,,AB and A1 B1 are parallel“ is given as
argument to the prove command in the following way:
prove { parallel A B A_1 B_1 }
At the end of the processing of the GCLC file, the theorem prover is invoked;
it can produce a proof in LATEX and in xml form (in the current directory) and,
within the GCLC report, a report about the proving process: whether the
conjecture was proved or disproved, data about CPU time spent, etc.

6.2

Basic Sorts of Conjectures

Statements for the basic sorts of conjectures are given in the following table:
points A and B are identical:
points A, B, C are collinear:
AB is perpendicular to CD:
AB is parallel to CD:
O is the midpoint of AB:
AB has the same length as CD:
points A, B, C, D are harmonic:

identical A B
collinear A B C
perpendicular A B C D
parallel A B C D
midpoint O A B
same_length A B C D
harmonic A B C D

All these sorts of conjectures can also be expressed in terms of geometry
quantities. Geometry quantities provide more general way for stating conjectures.
3 On

a modern PC computer, 10000 steps are performed in less then 1 minute.

6.3 Geometry Quantities and Stating Conjectures

point A 20 10
point B 70 10
point C 35 40
midpoint B_1 B C
midpoint A_1 A C
drawsegment
drawsegment
drawsegment
drawsegment
cmark_b
cmark_b
cmark_t
cmark_l
cmark_r

A B
A C
B C
A_1 B_1

A
B
C
A_1
B_1

prove { parallel A B A_1 B_1 }
Figure 6.1: Description of a triangle and midpoints of two of triangle’s sides and
the conjecture of midpoint theorem

6.3

Geometry Quantities and Stating Conjectures

The theorem prover deals with the following geometry quantities:
ratio of directed segments: for four collinear points P , Q, A, and B such
−−→
PQ
that A 6= B, it is the ratio −−→ ;
AB
signed area: it is the signed area SABC of a triangle ABC or the signed area
SABCD of a quadrilateral ABCD;
Pythagoras difference: for three points, PABC is defined as follows:
PABC = AB 2 + CB 2 − AC 2 .
Pythagoras difference for four points, PABCD is defined as follows:
PABCD = PABD − PCBD .
real number: it is a real number, constant.
In GCLC, geometry quantities are written as in the following examples:

6 Theorem Prover

Figure 6.2: Illustration generated from the GCLC code from Figure 6.1
−−→
PQ
−−→
AB
SABC
SABCD
PABC
PABCD

ratio of directed segments
signed area (arity 3)
signed area (arity 4)
Pythagoras difference (arity 3)
Pythagoras difference (arity 4)

sratio P Q A B
signed_area3 A B C
signed_area4 A B C D
pythagoras_difference3 A B C
pythagoras_difference4 A B C D

A conjecture to be proved is given as argument to the prove command. It
has to be some of the basic sorts of conjectures (see Section 6.2), or it has to be of
the form L = R, where L and R are expressions over geometry quantities. The
conjecture can involve geometry quantities (only) over points already introduced
(by a subset of commands) within the current construction. Geometry quantities
can be combined together into more complex terms by operators for addition,
multiplication and division. Operators are written in textual form as in the
following table:
=
+
·
/

equality
sum
mult
ratio

The conjecture and all its subterms are written in prefix form, with brackets
if needed. For instance,
SA1 B1 A = SA1 B1 B
is given to be proved in the following way:
prove { equal { signed_area3 A_1 B_1 A }
{ signed_area3 A_1 B_1 B }
}
and

−→
AF
−−→
FB

−−→ !
BD
· −−→ ·
DC

is given to be proved in the following way:

−−→ !
CE
−→ = 1
EA

6.3 Geometry Quantities and Stating Conjectures

prove { equal { mult { mult { sratio A F F B }
{ sratio B D D C } }
{ sratio C E E A } }
1 }
A range of geometry conjectures can be stated in terms of geometry quantities. The representations for the basic sorts of conjectures is are given in the
following table:
points A and B are identical
points A, B, C are collinear
AB is perpendicular to CD
AB is parallel to CD

iff
iff
iff
iff

O is the midpoint of AB

iff

AB has the same length as CD

iff

points A, B, C, D are harmonic

iff

PABA = 0
SABC = 0
PACD = PBCD
SACD = SBCD
−→
AO
−−→ = 1
OB
PABA = PCDC
−−→
−→
DA
AC
−−→ = −−→
CB
DB

Note that the command
prove { parallel A B A_1 B_1 }
(from Section 6.1) is equivalent to
prove { equal { signed_area3 A_1 B_1 A }
{ signed_area3 A_1 B_1 B }
}
The prover transforms the basic sorts of conjectures into statements given
in terms of geometric quantities: if a conjecture of a basic sort is given, the very
first step in the proof is its formulation in terms of geometric quantities.
The conjecture can involve geometry quantities only over points and lines
already introduced within the current construction, and by using (only) the
following commands:
• point
• line
• intersec
• midpoint
• med
• perp
• foot
• parallel
• translate
• towards

6 Theorem Prover
• online

The prover cannot prove conjectures about object constructed by using some
other commands. For instance, if a line a is constructed by the command
bis, then the prove cannot prove conjectures involving a or involving points
constructed by using a.

6.4

Area Method

One of the theorem prover built into GCLC is based on the algorithm described
in [3]. The basic idea of the algorithm is to express a theorem in terms of
geometry quantities, to eliminate (by appropriate lemmas) all occurrences of
constructed point and to simplify the expression, yielding a trivial equality.

6.4.1

Underlying Constructions

In [3], a construction is expressed in terms of commands INTER, PRATIO, TRATIO
and FOOT:
INTER Y ln1 ln2 : Point Y is the intersection of line ln1 and line ln2 .
PRATIO Y W U V r : Point Y is a point such that W Y = rU V , where r is a real
number.
UY
TRATIO Y U V r : Point Y is a point on line l, such that r = U
V , where r is a
real number and l is a line such that U lies on l and l is perpendicular to
UV .

FOOT Y P U V : Point Y is a foot from P to line U V (i.e., Y P is perpendicular
to U V and Y lies on U V .
For each point X constructed by the above constructions and for each geometry quantity g involving X, there is a suitable lemma that enables replacing
g by an expression with no occurrences of X. Thanks to these lemmas, all
constructed points can be eliminated from the conjecture.

6.4.2

Integration of Algorithm and Auxiliary Points

In order to be tightly integrated into GCLC, the prover uses standard GCLC
construction commands and, if needed, transforms them internally into form
required by the algorithm and/or introduces some auxiliary points:
midpoint is expressed in terms of PRATIO, it does not introduce new points;
foot is expressed in terms of FOOT, it does not introduce new points;
med introduces two auxiliary points: for instance, med m A B introduce a point
Mm as the midpoint of AB and a point Tm on the bisector of AB (such
that TRATIO Tm Mm A 1); the line m is then determined by the points Mm
and Tm ;

6.4 Area Method

perp introduces one auxiliary point: if A lies on the line q, then perp p A q introduces a point Tp on a line perpendicular to q (such that TRATIO Tp A Q1 1;
where the line q is determined by points Q1 and Q2 ); in this case, the line
p is determined by the points A and Tp ; if A does not lie on the line q,
then perp p A q introduce a point Fp which is a foot of the normal from
A to the line q; in this case, the line p is determined by the points A and
Fp ;
parallel introduces one auxiliary point: for instance, parallel p A q introduces a point Pp on a line parallel to q (such that PRATIO Pp A Q1 Q2 1;
the line p is then determined by the points A and Pp ;
translate is expressed in terms of PRATIO, it does not introduce new points;
towards is expressed in terms of PRATIO, it does not introduce new points;
online is expressed in terms of PRATIO, it does not introduce new points, but
introduces a (indeterminate) constant r: for instance, online X A B is
interpreted as PRATIO X A A B r.
Definitions of auxiliary points are given at the beginning of the proof.

6.4.3

Non-degenerative Conditions and Lemmas

Some constructions are possible only if certain conditions are met. For instance,
the construction inter X a b is possible only if the lines a and b are not parallel.
For such constructions non-degenerative conditions are store for future possible
use and listed at the end of the proof.
Some non-degenerative conditions can also be introduced during the proving
process:
• some lemmas have two cases (for instance, ,,if A belongs to CD“ and ,,if
A does not belong to CD“); if a condition for one case can be proved (as a
lemma), then that case is applied, otherwise, a condition for one case (the
one of the form L 6= R) is assumed and introduced as a non-degenerative
condition.
• in the cancellation rule, if all summands on both sides of the equality have
the same multiplication factor X, the rule tries to prove (as a lemma) that
X = 0; if this fails, a condition X 6= 0 is assumed and introduced as a
non-degenerative condition and the equality is cancelled by X.
Lemmas are being proved as separate conjectures, but, of course, sharing
the construction and non-degenerative conditions with outer context.

6.4.4

Structure of Algorithm

The algorithm has one main while loop — it process the sequence of all (relevant)
constructions in backward manner (from last to first construction step) and
transforms the current goal as follows:
• the current goal is initially the given conjecture;

6 Theorem Prover
• while there are construction steps do:
– apply geometric simplifications to the current goal;
– apply algebraic simplifications to the current goal;
– if the current construction step introduce a new point P , then eliminate (using the elimination rules) one of occurrences of P (from the
current goal) and go to the top of the while loop; otherwise, go to
next construction step.
• apply geometric simplifications to the current goal;
• apply algebraic simplifications to the current goal.
• if the current goal is a equality trivially true, then the conjecture has been
proved, if the current goal is a equality trivially false, then the conjecture
has been disproved, otherwise, the conjecture has been neither proved nor
disproved.

The reasoning steps, as seen from the above overall algorithm, are divided
into three groups:
algebraic simplifications: applies simplification rewrite rule (not directly related to geometry) such as:

x+0

→ x

0+x

→ x

x·1

→ x

x·0
x u
+
y
v
...

→ 0
x·v+u·y
→
y·v

geometric simplifications: applies simplification rewrite rule, directly related
to geometry quantities such as:

SAAB

→ 0

SABC

→ SBCA

PAAB

→ 0

...
elimination simplifications: applies elimination lemmas for eliminating constructed points for the current goal; for instance, if the point Y is introduced by as the intersection of lines l1 (determined by U and V ) and l2
(determined by P and Q), then Y can be eliminated from expression of
−→
AY using the following equality:
the form −
−→
CD
−→ ( SAP Q
AY
SCP DQ , if A ∈ U V
−−→ =
SAU V
CD
SCU DV , if A 6∈ U V

6.5 Wu’s Method and Gröbner Bases Method

Full details about all used lemmas and rewrite rules are given in the technical report “Framework for constructive geometry (based on the area method)”
(written by Pedro Quaresma and Predrag Janičić) [11]. This technical report is
a part of GCLC distribution.

6.4.5

Scope

The theorem prover can prove any geometry theorem expressed in terms of geometry quantities, and involving only points introduced by using the commands
point, line, intersec, midpoint, med, perp, foot, parallel, translate,
towards, online. This can be proved following the ideas from [3]. However,
some of the proofs can be very long and can take lot of time.

6.5

Wu’s Method and Gröbner Bases Method

One of the theorem prover built into GCLC is based on the Wu’s method
[12, 4] and one is based on the Gröbner bases method [1, 2]. These methods
are algebraic methods and they prove geometrical statements by manipulating
polynomials corresponding to the constructions and given conjectures. These
methods can also detect non-degenerative conditions, described in Section 6.4.

6.6

Prover Output

Whenever there was a conjecture given in the input gcl file, the prover produces
a short report. The prover can also generate proofs in LATEX format, or in xml
format. The level of details given in generated proof can be controlled by the
user.

6.6.1

Prover’s Short Report

The prover produces a short report (if there was a conjecture given in the gcl
file). In the command line version, this short report is shown and written in the
log file, while the GUI version shows this report in its output window. For the
area method, this report consists of information on number of steps performed,
on CPU time spent and whether or not the conjecture has been proved. For
example:
Number of elimination proof steps:
Number of geometric proof steps:
Number of algebraic proof steps:
Total number of proof steps:

3
6
23
32

Time spent by the prover: 0.002 seconds
The conjecture successfully proved.
The prover output is written in the file ceva_proof.tex.

6 Theorem Prover

6.6.2

Controlling Level of Output

For the area method, the level of generated proof output is controlled by the
command prooflevel. This command has one argument (an integer from 0 to
7) which provides the output level:
0 : no output (except the statement);
1 : elimination steps plus grouped geometric steps and algebraic steps;
2 : elimination steps plus geometric steps plus grouped algebraic steps;
3 : as level 2, plus statements of lemmas;
4 : as level 3, plus elimination steps plus grouped geometric steps and algebraic steps in lemmas;
5 : as level 4, plus geometric steps in lemmas;
6 : as level 5, plus algebraic steps at proof level 0;
7 : as level 6, plus algebraic steps in lemmas.
The default output level is 1.
For the algebraic theorem provers, the output is always given in a standard
form and the command prooflevel is ignored.

6.6.3

Proofs in LATEX format

The proof in LATEX form is generated by the command line version of GCLC, if
the option -eps (for export to eps format) is used, or, if there no export option
is used (when the figure is exported to LATEX format).
The proof in LATEX form is generated by the GUI version of GCLC, if the
option Deduction/Proof Export to LaTeX is checked.
In these cases, the proof is exported to the file name_proof.tex (in the
current directory, name is the name of the input file). If there is no prove
command within the construction, then the file with a proof will not be created.
For proofs generated by the area method, at the beginning of the proof, the
auxiliary points are defined, for instance:
Let Ma0 be the midpoint of the segment BC.
Let Ta1 be the point on bisector of the segment BC (such that TRATIO Ta1
Ma0 B 1).
The proof consists of proof steps. In each proof step, the current goal is
changed. For each proof step, there is an explanation and (optionally) its semantics counterpart. This semantic information is calculated for concrete points
used in the construction (note that these coordinates are never used in the proof
itself); it can serve as a semantic test, especially for conjectures for which is not

6.6 Prover Output

known whether or not they are theorems. Proof step are enumerated. For
example:
−→ −−→ −−→
AF BD
CE
= 1 by the statement (value 1=1)
−−→ · −−→ · −→
F B DC EA

−−→
−−→
−→
AF · BD · CE = 1 by geometric simplifications (value 1=1)
−1 · −
−→
−−→
−→
BF
DC
EA
Lemmas are proved within the main proof (making nested proof levels), and
the beginning and the end of a proof for a lemma is marked by a horizontal
solid line.
At the end of a proof, it is reported if the conjecture is proved (“Q.E.D.”
— lat. Quod Erat Demonstrandum — which was required to prove), if the
conjecture is disproved (if it was shown that it is invalid), or neither of these
two.
At the end of the main proof all non-degenerative conditions are listed. For
instance:
SMa0 Mb2 Tb3 6= STa1 Mb2 Tb3 i.e., lines Ma0 Ta1 and Mb2 Tb3 are not parallel (construction based assumption)
For proofs generated by the Wu’s and Gröbner bases method, the output
consist of a summary of processing steps over the relevant set of polynomials.
See one complete example in the appendix (Section E.5).
Modifying LATEX Output
The prover exports proofs in LATEX form. These LATEX files require LATEX package gclcproof.sty.
Once generated, the proof in LATEX form can still be parameterized. Namely,
data in the file can be formatted in several ways, giving different layouts. Also,
semantics part can be omitted. Parameters for proof formatting are given as
options for the package gclcproof.sty. There are three parameters:
style: defines the layout; available choices are:
• portrait — uses the package longtable to generate a multi-page
table.4
• portraitbreqn — uses the package breqn to try to break the equations. Problems with extra large fractions.
• landscape — uses the packages lscape, amsmath (with option leqno),
and breqn, to generate the list of equations in landscape mode, with
numbers on the left, and with automatic equation breaking.
The default value for style is portrait.
size: defines the font size in the proof. It uses the LATEX font size names of,
from tiny up to large. The default value is small.
4 For convenience, the required packages breqn.sty, flexisym.sty, mathstyle.sty,
cmbase.sim (developed by other authors), are distributed with GCLC. The packages
longtable.sty, lscape,sty, amsmath.sty (developed by other authors) are not distributed
with GCLC, but are widely available, most often as part of a TEX distribution.

6 Theorem Prover

semantic values: controls if the semantics values will be shown. If the option
semantics is used, the semantic values of both sides of equations will be
shown. The default value is NULL, i.e., without any value. The semantics
values are only generated by the area method.
According to the above,
\usepackage{gclcproof}
is equivalent to
\usepackage[portrait,small]{gclcproof}
(which gives a proof in portrait style, small size, without semantics style).
For example,
• \usepackage[tiny]{gclcproof}
retains the portrait mode (default value), but decrease the size of the fonts
used in the proof to tiny. No semantic values displayed.
• \usepackage[portraitbreqn,sematics]{gclcproof}
uses the breqn package of the AMSTeX to try to break automatically
the equations. Portrait form, small size fonts, semantic values displayed.
Note: the breqn package may fail (not being able to process the document)
if the proof contains large fractions, breqn it is unable to break them into
lines.
• \usepackage[landscape]{gclcproof}
uses the packages lscape, amsmath (with option leqno), and breqn to
produce a proof in landscape mode. It is the mode that provides the larger
environment for proofs, so in some proofs it will be the only one to be able
to display the proofs without overlapping of the different elements. Note:
the rotation of the proof to landscape mode it is done with Postscript
specials, so it may not display properly in some viewers. The size of the
fonts it is small, and the sematic values are not displayed.
In the generated proofs, there is always \usepackage{gclcproof} used (in
the preamble) and the layout can be changed by using options for this command,
as discussed above.

6.6.4

Proofs in xml format

The proof in xml form is generated by the command line version of GCLC, if
the option -xml (for export to xml format) or if the option -svg (for export to
svg format) is used.
The proof in xml form is generated by the GUI version of GCLC, if the
option Deduction/Proofs Export to XML is checked.
In these cases, the proof is exported to the file name_proof.xml (in the
current directory, name is the name of the input file). If there is no prove
command within the construction, then the file with a proof will not be created.
Proofs stored in xml are formatted analogously as in LATEX format.
The proofs in xml format fulfil restrictions posed by GeoCons_proof.dtd (as
stated in the line in each
of these files). For any xml file, it can be checked if it meets these restrictions.

6.7 Automatic Verification of Regular Constructions

It can be done using a xml processor, such as AltovaXML (copyrighted by Altova
GmbH). For instance:
> AltovaXML /v GeoCons_proof.dtd thm_proof.xml
verifies if the file thm_proof.xml is valid.
A proof in xml format (valid with respect to GeoCons_proof.dtd) can be
converted to a html form, for example:
>AltovaXML.exe /xslt1 GeoCons_proof.xsl /in thm_proof.xml /out thm_proof.html

A file with a proof in xml format can also be open directly by web browsers.
See one example in the appendix (Section E.5).
For more details about proofs represented in xml format, see Chapter 7.

6.7

Automatic Verification of Regular Constructions

A geometrical construction is associated with some fixed points (with concrete
Cartesian coordinates). In such environments, some constructions (e.g., if they
attempt to use intersection of parallel lines), but the question if such construction is always illegal or it is illegal only for given particular fixed points is not
trivial (if a construction is never illegal, i.e., if it is always possible, we will call
it regular). For answering such question, one has to use deductive reasoning,
and not only semantic check for the special case. Consider one simple example:
given (by Cartesian coordinates) three fixed distinct points A, B, C, we can
construct a point D as an image of the point C in translation TAB (in terms
of GCLC commands: translate D A B C); later on, if we try to construct an
intersection of lines AC and BD, we will discover that there is no such intersection (since these two lines are parallel). This holds not for some specific points
A, B, C, with D determined as above, but for all triples of points A, B, C. So,
this construction is illegal, and moreover, it is illegal not only for a given special
case, but always.
The system for automated testing whether a construction is regular or illegal
is built into GCLC and is based on the built-in theorem provers. All built-in
theorem provers can be used for this purpose. This verification mechanism can
be switched on or off:
• in the command line version, the verification mechanism is turned on by
using the option -d.
• in the GUI version, the verification mechanism is turned on by checking the button Deduction Control in the toolbar or the option Deduction/Deduction Control.
If the verification mechanism is turned on, while processing the input file
(with a description of a geometrical construction), GCLC provides to the theorem prover all construction steps performed. When GCLC encounters a construction step that cannot be performed (e.g., two identical points do not determine a line), it reports that the step is illegal with respect to a given set
of fixed points, and then it invokes the theorem prover. The prover is run on

6 Theorem Prover

the critical conjecture (e.g., it tries to prove that two points are identical) and,
if successful, it reports that the construction step is always illegal/impossible.
The prover generates the proof for the critical construction:
• in the command line version: in the format selected for conjectures (see
Chapter 5);
• in the GUI version: in LATEX and xml format if the options, respectively,
Proof Export to LATEX and Proof Export to xml are checked.
Realm. The verification deductive-check system currently covers the following
critical commands and constructions:
line — construction of a line given two points (error if the two points are
identical);
med — construction of a segment-bisector given two endpoints (error if the two
points are identical);
bis — constructing an angle-bisector of the angle determined by three points
A, B, C (error if A and B, or C and B are identical);
intersec — constructing an intersection of lines a and b (error if the two lines
are parallel);
angle — calculating an angle determined by three points A, B, C (error if A
and B, or C and B are identical);
Geometry objects that are subject to deductive verification have to be made
within using the following commands:
• point
• line
• intersec
• midpoint
• med
• perp
• foot
• parallel
• translate
• towards
• online

6.7 Automatic Verification of Regular Constructions

which are internally transformed into primitive constructions of the area method.
For more details see [11].
It is worth pointing out that although GCLC has support for a large number of constructions, only few of them can be illegal. The above list of critical
constructions almost exhaust them. The only possible illegal constructions that
are not covered by the current version of our system are constructions of intersection points of circle and line, and of two circles. Corresponding geometry
conjectures cannot be generally handled by the area method and the built-in
theorem prover.

6 Theorem Prover

Chapter 7

xml Support
GCLC has xml support, both for processing figures and proofs.1 xml is format
suitable for storing descriptions of geometrical constructions and proofs and as
interchange format:
• instead of raw, plain text representation, geometrical constructions are
stored in strictly structured files; these files are easy to parse, process,
and convert into different forms and formats;
• input/output tasks are supported by generic, external tools and different
geometry tools will communicate easily;
• growing corpora of geometrical constructions will be unified and accessible
to users of different geometry tools;
• easier communication and exchange of material with the rest of mathematical and computer science community;
• there is a wide and growing support for xml;
• different sorts of presentation (text form, LATEX form, html) easily enabled;
• strict content validation of documents with respect to given restrictions.

7.1

xml

Extensible Markup Language (xml) is a simple, very flexible text format derived
from SGML (ISO 8879) and with data structured using tags. Originally designed
to meet the challenges of large-scale electronic publishing, xml is also playing
an increasingly important role in the exchange of a wide variety of data on the
Web and elsewhere2 . It is called extensible because it is not a fixed format
like html (a single, predefined markup language), instead the tags indicate the
semantic structure of the data, rather than only its layout in a browser.
1 xml support was developed in collaboration with prof. Pedro Quaresma, Department of
Mathematics, University of Coimbra, Portugal, Jelena Tomašević (University of Belgrade,
Serbia), and Milena Vujošević-Janičić (University of Belgrade, Serbia).
2 http://www.w3.org/XML/

7 xml Support

However, xml is not just for Web pages: it can be used to store any kind
of structured information, and to enclose or encapsulate information in order
to pass it between different computing systems. An xml document can carry
both presentation (i.e., plausible visualisation) and content information. xml is
a project of the World Wide Web Consortium (W3C) and is a public format —
it is not a proprietary development of any company. Almost all browsers that
are currently in use support xml natively.
Data type definitions (dtds) provide a formal specification of the constraints
on the structure of data presented in xml form. A dtd is given as a formal
description in xml declaration syntax. It sets out what names are to be used
for the different types of element, where they may occur, and how they all fit
together. This formal description enables automatic verification (“validation”)
of whether a given document meets the given syntactical restrictions. This way,
groups sharing data with similar meanings can agree on different sets of tags
and dtds for representing different kinds of data.
Extensible stylesheet language transformation (xslt) is a document processing language that is used to transform the input xml documents i.e., the input
files to the desired output documents. An xslt style-sheet declares a set of rules
(templates) for an xslt processor to use when interpreting the contents of an
input xml document. These rules tell the xslt processor how that data should
be presented — as an xml document, as an html document, as plain text, or
in some other form.
Scalable Vector Graphics (svg) is a language for describing two-dimensional
graphics and graphical applications in xml3 . As xml, svg is a W3C recommendation.

7.2

xml Suite

GCLCxml suite for geometrical constructions and geometrical proofs consists
of the following components and tools:
• xml-based format for representing geometrical constructions with corresponding dtd, GeoCons.dtd;
• the option for conversion GCLC files to xml-based form;
• the option for generating figures from GCLC in svg form;
• the converter (implemented as xslt file, GeoConsGCLC.xlst) from xmlbased form to GCLC format;
• the converter (implemented as a xslt file, GeoConsHTML.xlst) from xmlbased form to a simple, readable html form (with syntax colouring features, provided for better readability);
• the converter (implemented as a xslt file, GeoConsNL.xlst) from xmlbased form to a natural language form (currently, only for English language);
3 http://www.w3.org/Graphics/SVG/

7.3 Using xml Tools

• the xml-based format for representing proofs of properties of geometrical
constructions with a corresponding dtd, GeoCons_proof.dtd; the format
is adapted for the area-method;
• the option for generating proofs in xml-based form;
• the converter (implemented as a xslt file, GeoCons_proof.xslt) for proofs
from xml-based form to a simple, readable html form (with syntax
colouring features, and other features for better readability).

7.3

Using xml Tools

A regular .gcl file (file without errors) can be converted to xml form in the
following way:
• in the command-line version — using the option -xml:
> gclc example.gcl example.xml -xml
• in the GUI version of GCLC, by selecting the option File/Export to.../XML.
Note that the xml file obtained in this way is not an image file, but also
textual representation of the construction described in the input file.
xml files obtained this way fulfil restrictions posed by GeoCons.dtd (as
stated in the line in each of these
files). For any xml, it can be checked if it meets these restrictions. It can be
done using a xml processor, such as AltovaXML (copyrighted by Altova GmbH).
For instance:
> AltovaXML /v GeoCons.dtd example.xml
verifies if the file example.xml is valid.
A xml file with geometrical contents (valid with respect to GeoCons.dtd)
can be converted to
• GCLC format, for example:
>AltovaXML.exe /xslt1 GeoConsGCLC.xsl /in example.xml /out example1.gcl

• to a simple, readable html form, for example:
>AltovaXML.exe /xslt1 GeoConsHTML.xsl /in example.xml /out example.html

• to a natural language (English) form (formatted in html):
>AltovaXML.exe /xslt1 GeoConsNL.xsl /in example.xml /out example.html

The geometrical xml files can be open directly by web browsers: For instance, if the second line in the xml file reads:

then the web-browser will render the contents of the file according to the file
GeoConsNL.xsl (see the example given in Figure 7.1).
GCLC files can be used for generating figures in svg format:

7 xml Support

Figure 7.1: Natural language presentation of a figure description stored in xml
form

• in the command-line version — using the option -svg:
> gclc example.gcl example.svg -svg
• in the GUI version of GCLC, by selecting the option File/Export to.../SVG.
A picture in svg format can be directly open by modern web browsers.
For .gcl files with conjectures, GCLC can generate proofs in xml form:
• in the command-line version — if the option -xmls or the option -svg is
used;
• in the GUI version of GCLC, by checking the option Source/Generate
proof in XML or the corresponding button in the source toolbar.
The xml files obtained in the above described way fulfil restrictions posed by
GeoCons_proof.dtd (as stated in the line
in each of these files). For any xml, it can be verified if it meets these restrictions
(by analogy with verifying files with constructions).
A xml file with a proof contents (valid with respect to GeoCons_proof.dtd)
can be converted to a html form, using GeoCons_proof.xsl, for example:
>AltovaXML.exe /xslt1 GeoCons_proof.xsl /in proof.xml /out proof.html
xml files with proofs can be also open directly by web browsers see one
example in the appendix (Section E.5).

Appendix A

List of Errors and Warnings
Syntax error: Number expected.
Syntax error: Two decimal points in number.
Syntax error: Identifier expected.
Syntax error: Identifier or number expected.
Syntax error: Undefined variable.
Syntax error: Wrong variable type.
Syntax error: Symbol ’{’ expected.
Syntax error: Symbol ’}’ expected.
Syntax error: Unrecognized definition or command.
Invalid or non-defined expression.
Symbol ’;’ expected.
Invalid while block.
Invalid if-then-else block.
Invalid procedure definition.
Too many while-block executions (more than 10000). Possible infinite loop.
The conjecture given to prove is ill-formed or includes a point
that is not constructed by commands supported by the prover.
Syntax error: Unknown procedure.
Syntax error: Parameters lists not matched.
Syntax error: Procedures cannot be defined within while-blocks or procedures
Syntax error: Invalid tree description.
Syntax error: Invalid graph description.
Invalid include file.
Input error: Invalid input.
Run-time
Run-time
Run-time
Run-time
Run-time
Run-time

error:
error:
error:
error:
error:
error:

Bad definition. Can not determine line.
Bad definition. Circle radius too small.
Bad definition. Can not determine intersection.
Bad definition. Can not determine angle.
Bad definition. Cannot determine ellipse.
Cannot export data.

Memory error: Cannot allocate enough memory.

78
Warning: Changing variable value
Warning: Changing variable type

A List of Errors and Warnings

Appendix B

Version History
1996 First release of GCLC (GCLC v1.0) ( c 1996-2009 Predrag Janičić);
1998 GCLC v2.0 : Cartesian commands (including conics) added. Full vertical
compatibility.
2000 GCLC v2.1 : Several bugs fixed.
2003 GCLC v3.0 : Commands
dim,
area,
color,
drawline,
getx,
gety,
fontsize,
animation_frames,
trace
added. Full vertical compatibility (for input format). New export format
and new LATEX style is used (gclc.sty). Since this version, commands
cmark do not have to precede other drawing commands.
WinGCLC— first release (graphical interface: c 2003-2009 Ivan Trajković, Predrag Janičić);
2004 GCLC v3.1: Several small bugs fixed.
WinGCLC 2004: export now supports exporting an animation to a sequence of bitmaps, which can then be used for generating animated gif
(by some other tool) or the animation in some other format. Import from
JavaView .jvx format is integrated in WinGCLC.
2005 GCLC v4.0: Commands
expression,
while,

B Version History
random,
ang_draw_parametric_curve,
ang_drawsystem1,
ang_drawsystem_a,
ang_drawsystem0_a,
ang_drawsystem1_a
added. Full vertical compatibility. A bug in drawing negative arcs fixed.
WinGCLC 2005: no changes in the Windows interface.

2006 GCLC v5.0: Theorem prover tightly built-in. Full vertical compatibility.
The commands
foot,
online,
angle_o,
drawdashline
ang_drawsystem_p,
ang_scale,
prove,
prooflevel,
prooflimit,
added. If not defined, area (a visible part of the picture) is, by default, the
whole of the picture (which is relevant for drawline and drawdashline
as they are applied only if there is defined area — now always). There
is support for colors for LATEX files, i.e., the command color is relevant
for exporting to LATEX too (not only for exporting to bitmap). The new
manual and the help file.
WinGCLC 2006: The behavior of changing line thickness (by the commands linethickness, normal, double) is fixed and improved for WinGCLC and for export to bitmap. New application icon and new file type
icon.
2006 GCLC v6.0: Full vertical compatibility. Added options for export to
eps (Encapsulated PostScript) and svg. Full support for xml (both for
construction descriptions and proofs). Added options for deductive verification of constructions.
The following commands were added:
procedure
call
(providing support for user-defined procedures),
ang3d_picture,
ang3d_origin,
ang3d_unit,

Version History

ang3d_scale,
ang3d_point,
ang3d_axes_drawing_range,
ang3d_drawline_p,
ang3d_drawsystem_p,
ang3d_draw_parametric_surface,
ang3d_draw_parametric_curve,
(providing support for 3D Cartesian system) and
drawarc_p
dradashwarc_p
set_equal
printvalueat_rb
background
ang_plot_data.
For the commands intersec, intersec2, bis, perp, med, sim, ang_intersec2,
full names (intersection, intersection2, bisector, perpendicular,
mediatrice, symmetrical, ang_intersection2) can also be used.
Using the theorem prover is simpler. Instead of stating conjectures in
terms of geometric quantities, one can also use the following basic sorts of
conjectures: identical A B, collinear A B C, perpendicular A B C D,
parallel A B C D, midpoint O A B, same_length A B C D, harmonic A B C D.
The sequence of commands in while-blocks now shares both the defined
variables and the environment with the outer context (In previous versions,
the environment, defined by commands ang_picture and ang_origin etc)
was reset in while-blocks).
In WinGCLC, there are new icons for easier use of the theorem prover.
In WinGCLC viewer and bitmap images (as well as in newly supported
formats, eps and svg) circles and arcs are not represented by small segments, but by proper circles and arcs.
WinGCLC 2006.1: New icons for easier using of the theorem prover.
When exporting a particular frame from an animation, traces are also
saved to output files.
2007 GCLC 7.0: Several small fixes were made and the following commands
were added:
drawtree
if_then_else
WinGCLC 2007: no changes in the Windows interface.
Support for hyperbolic geometry (through Poincaré disc model) is given
via a sample file, as illustration of the mechanism of user-defined procedures (sample21_hyp.gcl).

B Version History

2007.1 GCLC 7.1: Several small fixes were made.
Support for arrays (and the command array) added.
Support for export to another LATEX formats — PSTricks and TikZ.
Support for including other files (and the command include) added.
Arguments for procedure calls can now also be constants.
If a tree node should not be labelled, its name should start with the symbol
_ (in the previous version, its name had to be just the symbol _). All tree
nodes introduced by drawtree can be used as points.
If there is no defined area for ang_picture (or ang3d_picture), the default area is empty.
File exported to vector formats (LATEX, svg, xml) contain comments —
explanations for portions of code for easier understanding and modifying.
In the command line version, assumed file names are supported.
The batch processing option added.
The following commands were added:
filltriangle
fillrectangle
fillcircle
fillellipse
fillarc
fillellipsearc
dashstyle
drawarrow
arrowstyle
drawbezier3
drawdashbezier3
drawbezier4
drawdashbezier4
bezierprecision
drawellipsearc1
drawdashellipsearc1
drawellipsearc2
drawdashellipsearc2
rotateonellipse
onsegment
oncircle
mcp
WinGCLC 2007.1: no changes in the Windows interface.

Version History

2008 GCLC 8.0:
New theorem provers added: one based on the Wu’s method and one based
on the Gröbner bases method.
New form of intersection command (intersection of lines determined by
the given four points).
The following commands were added:
prover_timeout
theorem_name
layer
hide_layer
hide_layers_from
hide_layers_to
ang_getx
ang_gety
ang3d_getx
ang3d_gety
ang3d_getz
fillellipsearc0
fillarc0
Several bugs fixed.
WinGCLC 2008: New buttons added for additional theorem provers.
2008 GCLC 8.1:
The following commands were added:
drawgraph_a
drawgraph_b
2009 GCLC 9.0:
Several small fixes were made.
The following commands were added:
getcenter
export_to_latex
export_to_simple_latex
export_to_pstricks
export_to_tikz
export_to_eps
export_to_svg
New version of support for hyperbolic geometry (through Poincaré disc
model) is given via a new version of the sample file sample21_hyp.gcl
(co-authored with Zoran Lučić).
WinGCLC 2009: no changes in the Windows interface.

B Version History

Appendix C

Additional Modules
There are several additional modules that going with the basic GCLC program:
• WinGCLC ( c 2003-2015 Predrag Janičić, Windows interface: Ivan Trajković): MS Windows version of GCLC; user-friendly multi-document
interface, support for animations, traces, export to bitmaps etc.
• Command line version of GCLC for Linux ( c 1996-2005 Predrag Janičić).
• Simple previewer view for GCLC output files (there is no need to “latex”
them) ( c 1996-2003 Predrag Janičić). Supports both output formats (old,
based on emlines.sty and new, based on gclc.sty). A picture out.pic
generated by GCLC can be seen by:
> view out.pic
Program view has the following commands (they are similar to commands
in TEX viewers):
– → right ;
– ← left ;
– ↑ up ;
– ↓ down ;
– + zoom-in ;
– − zoom-out ;
– C increase step ;
– F decrease step ;
– Q quit.
• JavaView to GCLC converter jv2gcl ( c 2002 Predrag Janičić): converts files from JavaView to GCLC format.1

1 This program was developed in collaboration with prof. Konrad Polthier and Klaus Hildebrandt from Mathematical Institute, Technical University, Berlin. This work was partially
supported by daad grant form my visit to Technical University, Berlin (2003).

C Additional Modules

Appendix D

Acknowledgements
I am grateful to:
• Prof. Mirjana Djorić for the initial discussion which led to the first version
of GCLC (1996);
• Ivan Trajković, the main author of the Windows interface in WinGCLC
(2003);
• Prof. Neda Bokan and other members of the Group for geometry, education and visualization with applications (mostly based at the Faculty
of Mathematics, University of Belgrade) for their invaluable support in
developing the WinGCLC package (2003);
• daad (Germany) for funding my visit to Konrad Polthier’s group at Mathematical Institute of TU Berlin (2003), which I used for making a JavaView
→ GCLC converter. I also thank prof. Konrad Polthier and Klaus Hildebrandt for their hospitality and their collaboration in developing this converter;
• cim/cisuc (University of Coimbra, Portugal) for funding my visit to the
Department of Mathematics, University of Coimbra (2005), which I used
for developing the geometry theorem prover built into GCLC. I also thank
prof. Pedro Quaresma for his warm hospitality and his collaboration in
developing this prover;
• Prof. Pedro Quaresma (University of Coimbra), Jelena Tomašević, and
Milena Vujošević-Janičić, coauthors of the xml support for GCLC (2006);
• Prof. Bruno Buchberger (RISC, University of Linz, Austria), for kindly
inviting me to visit RISC and to present GCLC there (2006).
• emis (The European Mathematical Information Service) for mirroring
GCLC web page at http://www.emis.de/misc/software/gclc/ and
other emis locations.
• James Fry (New Albany, Indiana, USA) for careful revision of the GCLC/WinGCLC manual and help file and for many useful insights and comments (2005);

D Acknowledgements
• Aleksandar Samardžić for his advices in making Linux release of GCLC
(2003/2005/2006);
• Goran Predović (University of Belgrade, Serbia and Microsoft Development Center Belgrade) — the main author of the theorem provers based
on the Wu’s method and Gröbner based method (2008).
• Luka Tomašević (University of Belgrade, Serbia) — the main author of
the support for graph drawing (2008).
• Prof. Stefano Marchiafava (University ,,La Sapienza“, Rome, Italy), for
kindly inviting me to visit the University ,,La Sapienza“ and to present
GCLC there (2008).
• Colleagues who gave contributions and suggestions in earlier stages of development of WinGCLC: Nenad Dedić, Miloš Utvić, Nikola Begović, Ivan
Elčić, Jelena Grmuša, Aleksandra Nenadić, Marijana Lukić, Srdjan Vukmirović, Goran Terzić, Milica Labus, and Aleksandar Gogić (1999/2003);
• Konrad Polthier (TU Berlin), Zach (Temple University, USA), Vladimir
Baltić (University of Belgrade), Hristos Bitos (Greece), Aleksandar Gogić
(DTA, Belgrade), Bob Schumacher (Cedarville University, Ohio, USA),
Pedro Quaresma (University of Coimbra, Portugal), Zoran Lučić (University of Belgrade), Biljana Radovanović (University of Belgrade), Nedeljko
Stefanović (University of Belgrade), Milan Mitrović (Slovenia), Thomas
Speziale (USA), Ania Piktas (Poland), Bojan Radusinović (Serbia), Pierre
Larochelle (Florida Institute of Technology, USA), Robert Hartmann (TU
Clausthal, Clausthal-Zellerfeld, Germany), and Xavier Allamigeon for useful feedback and suggestions on different versions of GCLC/WinGCLC.
• All GCLC users for their support, feedback and suggestions.

Appendix E

Examples
E.1

Example (Simple Triangle)

point A 50 45
point B 45 15
point C 90 15
cmark_lt A
cmark_lb B
cmark_rb C
drawsegment A B
drawsegment B C
drawsegment C A
med a C B
med b A C
intersec O a b
drawcircle O A

E.2

E Examples

Example (Conics)

ang_picture 0 0 80 80
ang_origin 20.0 35.0
ang_drawsystem
ang_conic h 0 0 1 -1 0 -3
ang_conicprecision 75
ang_point A1 2 2
ang_point A2 3 2
line l A1 A2
ang_intersec2 P P2 h l
cmark_t P
ang_tangent p P h
color 32 192 32
ang_drawline p
color 32 32 192
ang_drawconic h
color 0 0 0
% -------------------------------------------------ang_unit 5
ang_picture 85 5 140 100
ang_origin 115.0 45.0
ang_drawsystem
ang_conic h -1 0.5 1 -1 0 -3
ang_conicprecision 50
ang_point A1 2 2
ang_point A2 3 2
line l A1 A2
ang_intersec2 P P2 h l
cmark_t P
ang_tangent p P h
color 32 192 32
ang_drawline p
color 192 32 32
ang_drawdashconic h

E.2 Example (Conics)

10
9
8
7
4

6
5

4
3

2
1

−1

−6 −5 −4 −3 −2 −1 0
−1
1

−2
−3

−1

−4
−5

−2

−6
−7

−3

−8

E.3

E Examples

Example (Parametric Curves)

ang_picture 5 5 112 92
ang_origin 45 35
ang_drawsystem_a
point X -0.5 0 0.5 0
point O 0 0
distance d X O
color 255 0 0
ang_draw_parametric_curve x {-3;x<8;x+0.1}{x;d/x}
color 0 0 255
ang_draw_parametric_curve x {-3;x<8;x+0.1}{x;d*x*sin(10*d*x)}
color 100 200 100
ang_draw_parametric_curve t {0;t<30;t+0.3}{sin(d*t)*t/6;-cos(d*t)*t/6}
animation_frames 50 5

E.3 Example (Parametric Curves)

y
5

−4

−3

−2

−1

0
−1

−2

−3

E Examples

E.4

Example (While-loop)

dim 120 80
ang_picture 5 5 115 70
ang_origin 45 25
ang_drawsystem_a
ang_draw_parametric_curve x {-3;x<5;x+0.05}{x;0.3*x*sin(3*x)}
% while loop in conjunction with parametric curves
number x -3
while { x<5 }
{
ang_picture 10 10 100 70
ang_origin 45 25
expression y { 0.3*x*sin(3*x) }
ang_point A x 0
ang_point B x y
drawsegment A B
expression x { x+0.05}
}

E.4 Example (While-loop)

y
4

−4

−3

−2

−1

0
−1

−2

x
7

E Examples

E.5
point
point
point
point

Example (Ceva’s theorem)
A
B
C
P

30
80
60
55

10
10
90
55

line a B C
line b A C
line c A B
line pa P A
line pb P B
line pc P C
intersec D a pa
intersec E b pb
intersec F c pc
drawsegment A B
drawsegment A C
drawsegment B C
drawsegment A D
drawsegment B E
drawsegment C F
cmark_b A
cmark_b B
cmark_t C
cmark_rt D
cmark_b F
cmark_lt E
cmark_r P
prove { equal { mult { mult { sratio A F F B }
{ sratio B D D C } }
{ sratio C E E A } }
1 }

E.5 Example (Ceva’s theorem)

D
E

Figure E.1: Output for Example E
LATEX output of the prover based on the area method:
−→
AF
−−→
FB

−−→ !
BD
· −−→ ·
DC

−→ !
AF
−1 · −−→ ·
BF

−−→ !
CE
−→
EA

by
the
statement
(0)
(value 1=1)

−−→ !
CE
−→
EA

by geometric simplifi(1)
cations (value 1=1)

−−→ !!!
CE
· −→
EA

by algebraic simplifica(2)
tions (value 1=1)

by Lemma 8 (point
F eliminated) (value (3)
1=1)

−−→ !!!!
CE
=
−1 · −→
AE

by geometric simplifi(4)
cations (value 1=1)

−−→ !
BD
−−→ ·
DC

−1 ·

−→
AF
−−→ ·
BF

−−→
BD
−−→
DC

−1 ·

SAP C
·
SBP C

−−→
BD
−−→
DC

−1 ·

SAP C
·
SBP C

−−→
BD
−−→ ·
DC

−−→ !!!
CE
· −→
EA

E Examples

−−→ −−→
BD · CE
−−→ −→
DC AE
SBP C
−−→

SCP B
· BD
·
−−→ SAP B
DC
SBP C

−−→
SCP B
·
·
−1 · BD
−−→
SAP B
CD
(−1 · SCP B )
−−→
· BD
−−→
CD

SAP C ·

by algebraic simplifica(5)
tions (value 1=1)

SAP C

by Lemma 8 (point
E eliminated) (value (6)
1=1)

by geometric simplifi(7)
cations (value 1=1)

by algebraic simplifica(8)
tions (value 1=1)

by Lemma 8 (point
D eliminated) (value (9)
1=1)

by geometric simplifi(10)
cations (value 1=1)

by algebraic simplifica(11)
tions (value 1=1)

SAP C

SAP B

SAP C ·

SBP A
SCP A

SAP B

SAP C ·

SBP A
(−1·SAP C )

(−1 · SBP A )
1

Q.E.D.
NDG conditions are:
SBP A 6= SCP A i.e., lines BC and P A are not parallel (construction based
assumption)
SAP B 6= SCP B i.e., lines AC and P B are not parallel (construction based
assumption)
SAP C 6= SBP C i.e., lines AB and P C are not parallel (construction based
assumption)
PF BF 6= 0 i.e., points F and B are not identical (conjecture based assumption)
PDCD 6= 0 i.e., points D and C are not identical (conjecture based assumption)
PEAE 6= 0 i.e., points E and A are not identical (conjecture based assumption)
Number of elimination proof steps: 3
Number of geometric proof steps: 6
Number of algebraic proof steps: 23
Total number of proof steps: 32

E.5 Example (Ceva’s theorem)

Time spent by the prover: 0.002 seconds

A fragment of the xml output of the prover based on the area method:

A fragment of the LATEX output of the prover based on the Wu’s method:

Creating polynomials from hypotheses
• Point A
no condition
• Point B
no condition
• Point C
no condition
• Point P
no condition
• Line a: B C
– point B is on the line (B, C)
no condition
– point C is on the line (B, C)
no condition
• Line b: A C
– point A is on the line (A, C)
no condition

100

E Examples
– point C is on the line (A, C)
no condition

• Line c: A B
– point A is on the line (A, B)
no condition
– point B is on the line (A, B)
no condition
• Line pa: P A
– point P is on the line (P , A)
no condition
– point A is on the line (P , A)
no condition
• Line pb: P B
– point P is on the line (P , B)
no condition
– point B is on the line (P , B)
no condition
• Line pc: P C
– point P is on the line (P , C)
no condition
– point C is on the line (P , C)
no condition
• Intersection of lines, D: a pa
– point D is on the line (B, C)
p33 = −u3 x2 + (u2 − u1 )x1 + u3 u1
– point D is on the line (P , A)
p34 = u5 x2 − u4 x1
• Intersection of lines, E: b pb
– point E is on the line (A, C)
p35 = −u3 x4 + u2 x3
– point E is on the line (P , B)
p36 = u5 x4 + (−u4 + u1 )x3 − u5 u1
• Intersection of lines, F : c pc
– point F is on the line (A, B) — true by the construction
no condition
– point F is on the line (P , C)
p37 = (u5 − u3 )x6 + (−u5 u2 + u4 u3 )

E.5 Example (Ceva’s theorem)

101

Creating polynomial from the conjecture
• Processing given conjecture(s).
Conjecture 1:
p38 = −2x6 x3 x1 + u3 x6 x3 + u3 x6 x1 + u1 x3 x1 − u3 u1 x3

Invoking the theorem prover
The used proving method is Wu’s method.
The input system is:
p0

= −u3 x2 + (u2 − u1 )x1 + u3 u1

= u5 x2 − u4 x1

= −u3 x4 + u2 x3

= u5 x4 + (−u4 + u1 )x3 − u5 u1

(u5 − u3 )x6 + (−u5 u2 + u4 u3 )

Triangulation, step 1
Choosing variable: Trying the variable with index 6.
Variable x6 selected: The number of polynomials with this variable is 1.
Single polynomial with chosen variable: No reduction needed.
The triangular system has not been changed.
Triangulation, step 2
Choosing variable: Trying the variable with index 5.
Choosing variable: Trying the variable with index 4.
Variable x4 selected: The number of polynomials with this variable is 2.
Minimal degrees: 3 polynomials with degree 1 and 2 polynomials with degree
1.
Polynomial with linear degree: Removing variable x4 from all other polynomials by reducing them with polynomial p3 .
Finished a triangulation step, the current system is:
p0

= −u3 x2 + (u2 − u1 )x1 + u3 u1

= u5 x2 − u4 x1

= u5 x4 + (−u4 + u1 )x3 − u5 u1

(u5 u2 − u4 u3 + u3 u1 )x3 − u5 u3 u1
(u5 − u3 )x6 + (−u5 u2 + u4 u3 )

102

E Examples

Triangulation, step 3
Choosing variable: Trying the variable with index 3.
Variable x3 selected: The number of polynomials with this variable is 1.
Single polynomial with chosen variable: No reduction needed.
The triangular system has not been changed.
Triangulation, step 4
Choosing variable: Trying the variable with index 2.
Variable x2 selected: The number of polynomials with this variable is 2.
Minimal degrees: 1 polynomials with degree 1 and 0 polynomials with degree
1.
Polynomial with linear degree: Removing variable x2 from all other polynomials by reducing them with polynomial p1 .
Finished a triangulation step, the current system is:

(u5 u2 − u5 u1 − u4 u3 )x1 + u5 u3 u1

= u5 x2 − u4 x1

= u5 x4 + (−u4 + u1 )x3 − u5 u1

(u5 u2 − u4 u3 + u3 u1 )x3 − u5 u3 u1
(u5 − u3 )x6 + (−u5 u2 + u4 u3 )

Triangulation, step 5
Choosing variable: Trying the variable with index 1.
Variable x1 selected: The number of polynomials with this variable is 1.
Single polynomial with chosen variable: No reduction needed.
The triangular system has not been changed.
The triangular system is:

(u5 u2 − u5 u1 − u4 u3 )x1 + u5 u3 u1

= u5 x2 − u4 x1

= u5 x4 + (−u4 + u1 )x3 − u5 u1

(u5 u2 − u4 u3 + u3 u1 )x3 − u5 u3 u1
(u5 − u3 )x6 + (−u5 u2 + u4 u3 )

E.5 Example (Ceva’s theorem)

103

Final remainder
Final remainder for conjecture 1
Calculating final remainder of the conclusion:
g = −2x6 x3 x1 + u3 x6 x3 + u3 x6 x1 + u1 x3 x1 − u3 u1 x3
with respect to the triangular system.
1. Pseudo remainder with p4 over variable x6 :
g = (−2u5 u2 + u5 u1 + 2u4 u3 − u3 u1 )x3 x1 +
(u5 u3 u2 − u5 u3 u1 − u4 u23 + u23 u1 )x3 + (u5 u3 u2 − u4 u23 )x1
2. Pseudo remainder with p3 over variable x4 :
g = (−2u5 u2 + u5 u1 + 2u4 u3 − u3 u1 )x3 x1 +
(u5 u3 u2 − u5 u3 u1 − u4 u23 + u23 u1 )x3 + (u5 u3 u2 − u4 u23 )x1
3. Pseudo remainder with p2 over variable x3 :
g = (u25 u3 u22 − 2u25 u3 u2 u1 + u25 u3 u21 − 2u5 u4 u23 u2 +
2u5 u4 u23 u1 + u5 u23 u2 u1 − u5 u23 u21 + u24 u33 − u4 u33 u1 )x1 +
(u25 u23 u2 u1 − u25 u23 u21 − u5 u4 u33 u1 + u5 u33 u21 )
4. Pseudo remainder with p1 over variable x2 :
g = (u25 u3 u22 − 2u25 u3 u2 u1 + u25 u3 u21 − 2u5 u4 u23 u2 +
2u5 u4 u23 u1 + u5 u23 u2 u1 − u5 u23 u21 + u24 u33 − u4 u33 u1 )x1 +
(u25 u23 u2 u1 − u25 u23 u21 − u5 u4 u33 u1 + u5 u33 u21 )
5. Pseudo remainder with p0 over variable x1 :
g=0

Prover report
Status: The conjecture has been proved.
Space Complexity: The biggest polynomial obtained during proof process
contained 13 terms.
Time Complexity: Time spent by the prover is 0.053 seconds.
NDG conditions are:
• PF BF 6= 0 i.e., points F and B are not identical (conjecture based
assumption).
• PDCD 6= 0 i.e., points D and C are not identical (conjecture based
assumption).
• PEAE 6= 0 i.e., points E and A are not identical (conjecture based
assumption).

104

E Examples

Bibliography
[1] B. Buchberger. An Algorithm for finding a basis for the residue class ring
of a zero-dimensional polynomial ideal. PhD thesis, Math. Inst. University
of Innsbruck, Austria, 1965.
[2] B. Buchberger and F. e. Winkler. Gröbner Bases and Applications. Cambridge University Press, 1998.
[3] C. C. Chou, O. X. S. Gao, and J. Z. Zhang. Automated production of
traditional proofs for constructive geometry theorems. In Eighth Annual
IEEE Symposium on Logic in Computer Science, 1993.
[4] S.-C. Chou. Mechanical Geometry Theorem Proving. D.Reidel Publishing
Company, Dordrecht, 1988.
[5] M. Djorić and P. Janičić. Constructions, instructions, interactions . Teaching Mathematics and its Applications, 23(2):69–88, 2004.
[6] P. Janičić. GCLC – A Tool for Constructive Euclidean Geometry and More
than That. In N. Takayama, A. Iglesias, and J. Gutierrez, editors, Proceedings of International Congress of Mathematical Software (ICMS 2006),
volume 4151 of Lecture Notes in Computer Science, pages 58–73. SpringerVerlag, 2006.
[7] P. Janičić and P. Quaresma. System description: Gclcprover + GeoThms.
In U. Furbach and N. Shankar, editors, International Joint Conference
on Automated Reasoning (IJCAR-2006), volume 4130 of Lecture Notes in
Artificial Intelligence, pages 145–150. Springer-Verlag, 2006.
[8] P. Janičić. Geometry Constructions Language. Journal of Automated Reasoning, 2009. to appear.
[9] P. Janičić and I. Trajković. WinGCLC — a Workbench for Formally Describing Figures. In Proceedings of the 18th Spring Conference on Computer
Graphics (SCCG 2003), pages 251–256, Budmerice, Slovakia, April, 24-26
2003. ACM Press, New York, USA.
[10] P. Quaresma and P. Janičić. Integrating dynamic geometry software, deduction systems, and theorem repositories. In J. Borwein and W. Farmer,
editors, Mathematical Knowledge Management (MKM-2006), volume 4108
of Lecture Notes in Artificial Intelligence, pages 280–294. Springer-Verlag,
2006.

106

BIBLIOGRAPHY

[11] P. Quaresma and P. Janičić. Framework for the Constructive Geometry.
Technical Report TR2006/001, Center for Informatics and Systems of the
University of Coimbra, 2006.
[12] W.-T. Wu. On the decision problem and the mechanization of theorem
proving in elementary geometry. Scientia Sinica, 21:157–179, 1978.

Index
%, 31
ang3d axes drawing range, 37
ang3d draw parametric curve, 39
ang3d draw parametric surface, 38
ang3d drawline p, 38
ang3d drawsystem p, 37
ang3d getx, 38
ang3d gety, 38
ang3d getz, 38
ang3d origin, 37
ang3d picture, 37
ang3d point, 38
ang3d scale, 37
ang3d unit, 37
ang conic, 35
ang conicprecision, 36
ang draw parametric curve, 35
ang drawconic, 35
ang drawdashconic, 35
ang drawline, 35
ang drawline p, 35
ang drawsystem, 34
ang drawsystem0, 34
ang drawsystem0 a, 34
ang drawsystem1, 34
ang drawsystem1 a, 34
ang drawsystem a, 34
ang drawsystem p, 34
ang getx, 34
ang gety, 35
ang intersec2, 35
ang intersection2, 35
ang line, 35
ang origin, 33
ang picture, 33
ang plot data, 36
ang point, 34
ang scale, 33
ang tangent, 35
ang unit, 33

angle, 19
angle o, 19
animation frames, 40
area, 31
array, 20
arrowstyle, 31
background, 31
batch processing, 51, 53, 54
bezierprecision, 32
bis, 17
bisector, 17
bitmap, 46, 49
call, 22
circle, 16
circleprecision, 32
cmark, 10, 29
color, 31
comments, 31, 49
control structures, 5
dash, 32
dashstyle, 32
deductive verification, 69
dim, 31
distance, 19
dmc, 32
double, 32
dradashwarc p, 24
drawarc, 24
drawarc p, 24
drawarrow, 23
drawbezier3, 25
drawbezier4, 25
drawcircle, 23
drawdasharc, 24
drawdashbezier3, 25
drawdashbezier4, 26
drawdashcircle, 24
drawdashellipse, 24

108
drawdashellipsearc, 24
drawdashellipsearc1, 25
drawdashellipsearc1, 25
drawdashline, 23
drawdashsegment, 23
drawellipse, 24
drawellipsearc, 24
drawellipsearc1, 25
drawellipsearc2, 25
drawgraph a, 27
drawgraph b, 27
drawline, 23
drawpoint, 23
drawpolygon, 26
drawsegment, 10, 23
drawtree, 26
drawvector, 23
eps, 33, 46, 49, 54, 66
export, 49
to LATEX, 46, 49, 52, 53, 66
to bitmap, 46, 54
to PSTricks, 52
to TikZ, 46, 53
to eps, 46, 54, 66
to svg, 46, 55, 68
to xml, 46, 55, 68
export to eps, 33
export to latex, 33, 49
export to pstricks, 33
export to simple latex, 33
export to svg, 33
export to tikz, 33
expression, 19
fillarc, 28
fillarc0, 29
fillcircle, 28
fillellipse, 28
fillellipsearc, 29
fillellipsearc0, 29
fillrectangle, 28
filltriangle, 28
fontsize, 31
foot, 17, 61
getcenter, 17
getx, 19
gety, 19
hide layer, 39

INDEX
hide layer from, 39
hide layers to, 39
if then else, 21
import
from JavaView, 6, 46
include, 22
installation, 9
intersec, 16, 61
intersec2, 16
intersection, 16
intersection2, 16
JavaView, 6, 46, 79, 85
LATEX, 5, 9, 10, 33, 44, 46, 47, 49–54,
66, 69
LATEX
package, 9, 11, 31, 50, 53–55, 67
layer, 39
line, 16, 61
linethickness, 32
log file, 12
loops, 5, 20
mark, 29
mcp, 32
mcr, 32
med, 17, 61
mediatrice, 17
midpoint, 17, 61
normal, 32
number, 16
oncircle, 17
online, 17, 61
onsegment, 17
parallel, 17, 61
pdf, 55
perp, 17, 61
perpendicular, 17
point, 10, 16, 34, 40, 43, 61, 65
PostScript, 55
printat, 30
printvalueat, 30
procedure, 22
procedures, 5, 22
prooflevel, 41, 57, 66
prooflimit, 41, 57

INDEX
prove, 40, 57, 58, 66, 68
prover timeout, 41, 57
PSTricks, 33, 46, 49, 52
Q.E.D., 67
random, 19
rotate, 18
rotateonellipse, 18
samples, 9
set equal, 16
sim, 18
svg, 33, 46, 49, 55, 68
symbolic expressions, 5, 16, 19
symmetrical, 18
theorem prover, 5, 40, 57
area method, 57, 62
Gröbner bases method, 57, 65
Wu’s method, 57, 65
theorem name, 41, 57
TikZ, 33, 46, 49, 53
towards, 18, 61
trace, 40
translate, 18, 61
turtle, 18
view, 9, 85
while, 20
WinGCLC, 5, 9, 43
xml, 44, 46, 47, 49, 55, 68, 69, 73
xml validation, 74

109

Source Exif Data:

File Type                       : PDF
File Type Extension             : pdf
MIME Type                       : application/pdf
PDF Version                     : 1.5
Linearized                      : No
Page Count                      : 109
Page Mode                       : UseOutlines
Author                          : 
Title                           : 
Subject                         : 
Creator                         : LaTeX with hyperref package
Producer                        : pdfTeX-1.40.13
Create Date                     : 2015:10:29 11:23:46+01:00
Modify Date                     : 2015:10:29 11:23:46+01:00
Trapped                         : False
PTEX Fullbanner                 : This is pdfTeX, Version 3.1415926-2.4-1.40.13 (TeX Live 2012/Debian) kpathsea version 6.1.0

EXIF Metadata provided by EXIF.tools

10 GCLC 2015 Manual

Navigation menu

Versions of this User Manual:

Views

Navigation