With a large number of software tools dedicated to the visualisation and/or demonstration of properties of geometric constructions and also with the emerging of repositories of geometric constructions, there is a strong need of linking them, and making them and their corpora, widely usable. A common setting for interoperable interactive geometry was already proposed, the i2g format, but, in this format, the conjectures and proofs counterparts are missing. A common format capable of linking all the tools in the eld of geometry is missing. In this paper an extension of the i2g format is proposed, this extension is capable of describing not only the geometric constructions but also the geometric conjectures. The integration of this format into the Web-based GeoThms, TGTP and Web Geometry Laboratory systems is also discussed.
In many dynamic geometry software tools (DGSs), a geometric construction is speci ed using, explicitly, a formal language. In others, the construction is made interactively, by clicking speci c buttons and/or icons, but behind this approach there is also a formal geometric language, although usually hidden from the user. All these languages share many primitive commands (related to geometric constructions), but there are also di erences in the set of supported commands, and they follow di erent syntax rules.
Another important set of tools related to geometric constructions is given
by the geometry automated theorem proving software tools (GATPs). Given a
geometric construction (eventually created with a given DGS) and a conjecture
related to that construction, the GATPs are capable of proving or disproving
(although not always) the conjecture. Some of them aim at producing traditional,
human readable, geometric proofs [
With a large number of tools focusing on visualising geometric constructions, on proving properties of constructed objects (or both) and repositories of geometric problems (RGPs), there is an emerging need of linking them and making widely usable: constructions; conjectures and proofs generated with di erent tools. This would help in the progress of the eld of geometric constructions, including their role in education.
The i2g format [18] was designed to describe constructions created with a DGS allowing the exchange of geometric constructions between di erent DGSs. This format should be complemented in such a way that it can provide support for conjectures. The new format should be a superset of the former format, i.e. a DGS should be able to read the new format, ignoring all the extra information regarding conjectures and proofs. A GATP should be able to read the new format using, if needed, the geometric construction speci cation. In the following such an extension, the i2gatp format, is discussed.
Some of the most important motivating arguments for using xml in storing descriptions of geometric constructions and conjectures and as an interchange format are: strictly structured les, easy to parse, process, and convert into di erent forms and formats; a strict content validation of documents with respect to a given set of restrictions; easier communication and exchange of material between unrelated tools.
Paper overview. In Section 2 some background regarding DGSs, the i2g format, GATPs and RGPs is given. In Section 3 the overall structure of the new format is described. In Sections 4 implementations issues are discussed. Finally in Section 5 some nal conclusions are drawn and future work is discussed. 2
In this section some basic background information about geometric constructions, the intergeo format (i2g), geometric conjectures and proofs and repositories of geometric problems is given. 2.1
Dynamic geometry software tools (DGSs) allow an easy construction of geometric gures built from free objects, elementary constructions and constructed objects. The dynamic nature of such tools allows its users to manipulate the positions of the free objects in such a way that the constructed objects are also changed, yet preserving the geometric properties of the construction. These manipulations are not formal proofs, as the user is considering only a nite set of concrete positions. Neither the DGS are able to provide a proof of a given conjecture nor they are able to ensure the soundness of the constructions built by its users.
There are multiple DGSs available 1: GeoGebra, Cinderella, GeometerSketchpad, C.a.R., Cabri, GCLC to name some of the most used. 2.2
The Intergeo (i2g) le format is a speci cation based on the markup language xml designed to describe constructions created with a DGS. It is one of the main 1 www.geogebra.org, www.cinderella.de, www.dynamicgeometry.com/, zirkel.
sourceforge.net/, www.cabri.com/, www.emis.de/misc/software/gclc/
results of the intergeo project, an eContentplus European project dedicated to
the sharing of interactive geometry constructions across boundaries. For more
information about the project, visit the site http://i2geo.net and look into
the documentation available there, as well as to [
An intergeo le takes the form of a compress le package. The main le is intergeo.xml, which provides a textual description of the construction in three parts, the elements part describing a (static) initial instance of the con guration, the constraints part where the geometric relationships are expressed and the display part where the details regarding the rendering of the construction are placed. For more details on the le format see [18].
There are already a signi cant number of DGSs supporting the i2g format
(see [
The geometry automated theorem provers (GATPs) give its users the possibility
to reason about a given DGS construction, this is no longer a \proof by testing",
but an actual formal proof. Another link between the GATPs and the DGSs is
given by the automated deductive testing, by the GATP, of the soundness of
the constructions made by the DGS [
Automated theorem proving in geometry has two major lines of research:
synthetic proof style and algebraic proof style (see [
If the GATP is capable of producing synthetic proofs, the proof itself can be
an object of study, in other cases only the conclusion matters [
When considering repositories of geometric problems we are directly interested in a common format. If we want to provide a repository of geometric problems that can be used by DGSs and GATPs, then the constructions should be kept in a common format that can be converted to the DGS and/or GATP internal format whenever needed. The author of this paper is directly involved in this e orts having three di erent project that involve repositories of geometric problems.
The rst (chronologically) of the mentioned projects is GeoThms2, a Webbased framework for exploring geometric knowledge integrating DGSs, GATPs,
and a RGP. The GeoThms is a publicly accessible system with a growing body
of geometric constructions and formally proven geometric theorems, its users
can easily use/browse through existing geometric contents and build new
contents [17]. Within this project a common, xml-based, interchange format for
descriptions of geometric constructions, conjectures and proofs was developed [
A more recent project is the Thousands of Geometric problems for geometric
Theorem Provers (TGTP )3. This is a Web-based library of problems in
geometry. TGTP aims, in a similar spirit of TPTP and other libraries, to provide the
automated reasoning in geometry community with a comprehensive and
easily accessible library of GATP test problems [
In an educational setting, the project Web Geometry Laboratory (WGL)4 is an asynchronous/synchronous Web environment that integrates a DGS and a RGP (and it will integrate a GATP in a next version), aiming to provide an adaptative and collaborative blended-learning environment for geometry [19]. Here the need for a common interchange format is less important, nevertheless it will be useful to allow the system to be more easily con gurable, i.e. using a common format will allow choosing the DGS and/or the GATP more freely. 2.5
There are already some systems integrating a DGS with one, or more, GATP
and a set of examples (e.g. GCLC [
A common format for geometric constructions, conjectures and proofs should address the communication between DGSs and GATPs, to establish the soundness, by the GATP, of a construction made with the help of the DGS or to prove (or disprove) a given conjecture about a construction made in the DGS: { The communication between DGSs and GATPs, to establish the soundness, by the GATP, of a construction made with the help of the DGS or to prove (or disprove) a given conjecture about a construction made in the DGS.
{ The rendering of the proof. If the GATP uses an algebraic method only the nal result will be usable, but if the GATP uses a synthetic method, the proof itself can be an object of study.
Geometric proofs could appear in many di erent forms, for instance in axiomatic form (e.g., in Hilbert-style, sequent calculus style, etc.); representing higher-level proofs, produced by the area method; as algebraic proofs produced by the algebraic methods like the Grobner basis method, etc. The representation of the proof and/or its rendering will always be linked to the method used in its development. This will be addressed in Section 3.2. 3.1
In order to enable communication between the geometric tools (i.e DGSs and GATPs) and converting les between di erent formats a single target format should exist: a format that could de ne a common normal form for the di erent tools. The proposal is to extend the i2g format in such a way that the new format would complement the construction description (made by a DGS) with the conjecture description. This new format will be called the i2gatp format.
Converting from a DGS/GATP language to xml, would be performed by a speci c converter, naturally relying on the DGS/GATP's parsing mechanism. Converting from xml to a DGS/GATP language, will be implemented via xmlparsing tools.
Having converters from, and to, the i2gatp format for all DGSs and GATPs, we (indirectly) have converters from each tool to any other tool. Thus, in this way, the base for a common interchange format is provided. xml is a natural framework for such interchange format, because of its strict syntax, veri cation mechanisms, suitable usage on the Internet, and a large number of available supporting tools.
xml descriptions of constructions, conjectures and proofs can be, by means of xslt, also rendered into other formats that are convenient for human-readable display in browsers. It can also be transformed into di erent representations, such as natural language form.
A speci c xml scheme document could de ne syntactical restrictions for construction descriptions, conjectures and proofs. This document could then be used, in conjunction with the generic xml validation mechanism, for verifying whether a given le in the i2gatp format is correct (or not). 3.2
Following the ideas of the i2g common format all the les related to the i2gatp format will be packed in a single compressed le, the container, which is nothing more then a i2g container with three additional directories. The i2gatp format will be spread in four, at least, XML les (see Figure 1).
Apart from the intergeo.xml le, which is mandatory (see the i2g format speci cation [18]), the other les are optional.
I2GATP Format information construction (I2G) name description statement [bibrefs][keywords] elements constraints display bibentry keyword conjecture proofInfo hypothesis ndg conclusion
method status limits measures platform Information The information.xml le contains all the generic (human) information about the problem. The name of the problem; a brief, informal, description of the problem; an informal (rigorous) mathematical description (statement) of the problem; a list of bibliographic references; a list of keywords. Construction The intergeo.xml le contains the construction in the i2g format. The i2g format has as main tag the construction tag with three sub-nodes: elements for the free objects; constraints for the objects xed by construction constraints and display for the display details.
Conjecture This is the core of the i2gatp format. In here the hypothesis, the ndg (non-degenerate conditions) and the conclusion, establishing the conjecture to be proved, are speci ed. The non-degenerate conditions could be a side-e ect of the proving process, e.g. automatically generated by a GATP based in the area method, or provided manually.
Proofs For a given problem/conjecture we can have many proof attempts: different approaches, for instance synthetic proof versus algebraic proof; di erent methods, Grobner bases method versus Wu's method; di erent GATPs, GCLCprover versus CoqAM, and all the possible combinations of this three di erent aspects.
Each proof attempt will be kept in a le proofInfo.xml in a sub-directory of the proofs directory (see Section 3.3 for more details).
Each individual proof node will have: the information regarding the GATP, its version and method used; the status of the proof, e.g. proved; the computational constraint regarding the proof attempt made by the GATP, e.g. maximum CPU time and RAM space allowed by the system; the proof metrics, e.g. number of proof steps (area method) and the platform used when doing the proof, e.g. CPU, RAM, and other details about the computational platform.
For the proof status the SZS ontology [20] will be used as a base. The \Unsolved" branch will be used as it is, the \Solved" branch has to be adapted to the i2gatp settings.
Given the fact that the proofs produced by di erent GATPs/Methods are, and should continue to be, quite di erent we do not try to create a common formats for the proofs. The outcomes produced by the di erent GATPs will be kept as they are produced (see the container in Section 3.3). 3.3
As said above, the i2gatp container is a superset of the i2g container, with three additional directories: (information; conjecture and proofs). This means that it will be possible to extract the i2g container out of this le, it will be a simple question of unpacking the le, erasing the additional directories and repacking, if needed, the resulting les.
The structure of the container follows closely the structure of the i2gatp format. The information, construction and conjecture directories will contain the les information.xml, intergeo.xml and conjecture.xml respectively. The directory construction may also contain the rendering of the construction in various graphical formats (e.g. PDF, SVG, PNG, etc.).
The directory proofs will contain as many sub-directories as proofs attempts were made for the problem in question. The naming convention follows the ideas in the i2g format, that is, after the pre x \proof", the name of the GATP, its version and nally the method used. Given the fact that this is a directory identi er the strings used in these last elds should be conform to the standard naming conventions. In each of this sub-directories the le proofInfo.xml will contain the information regarding the proof attempt. This directory may also contain les with the rendering of the proof in di erent formats (e.g. PDF, HTML, etc.).
The remaining directories follow the structure of the i2g format and can be used to place additional contents produced by the GATPs.
Following the i2g conventions, the suggest naming convention to the container is problem<problem name>.zip.
In the next section the symbol lists, i.e. the tags proposed to this xml-format, are described. 3.4
As said above, the container will have \four" (main) xml les: information.xml; intergeo.xml; conjecture.xml and as many proofInfo.xml les as proof attempts were made for a given problem. The intergeo.xml is described in the i2g common le format, technical report D3.10 [18]. The other three are speci c for the i2gatp format and their symbol lists will be described in the next sections.
The symbol lists will be describe in a coarse fashion. For a more detailed account see [16].
Generic Information (information.xml) Generic information about the problem. All elds, except the name, may be empty.
The tags are: name; description; statement; bibrefs and bibentry; keywords and keyword.
The description will be a brief, informal, description of the problem in text
format and the statement will be an informal (rigorous) mathematical description
of the problem in MathML [
The bibrefs is a list (it may be empty) of bibliographic references in BibTEXml format5.
The contents of the description and bibrefs tags could be automatically converted from LATEX and BibTEX using, for example, tex4ht 6 and BibTEXml converters respectively.
The keywords is a list of keywords in text format. For the moment this eld is a free-form text eld. For better querying the repositories, an index or a geometric ontology should be considered. Maybe an \open classi cation", that
is, a classi cation index open to users additions and where the most chosen keywords became, in time, xed.
pothesis, ndg (for non-degenerate conditions) and conclusion. The three last tags can contain a large number of other tags used to write down the geometric (logical) statements.
Without pretending to be exhaustive we have: not equal; not parallel; equal; plus; mult; collinear; perpendicular; parallel; midpoint; same length; harmonic; segment ratio. The symbols of the intergeo format regarding the geometric construction can occur here.
Proofs Information proofInfo.xml Contains all the information regarding a proof attempt for given problem.
This is a record of the conditions under which the proof was attempted, i.e. the method used (method), the limits imposed to the GATP and the computer system used (limits and platform). Adding to this the proof outcome, i.e. proved, not proved, etc. and also, measures of e ciency, e.g. CPU time used, number of steps, etc. (status and measures).
In the list of symbols we have (among others): status; limits; time limit seconds; iterations limit; measures; CPU time; elimination steps; number terms largest polynomial; computer name; clock speed; RAM; operating system. 4
Having de ned a xml format for geometric constructions and conjectures its
usefulness depends on its support from other tools, i.e. the capability of tools
such as DGSs (see [
Using the TGTP project as a catalyst for this task I will try to provide (working in conjunction with the authors of the tools): { Converters from dynamic DGSs and GATPs tools (GCL language, Coq AM, etc.) to i2gatp format. { Converters from i2gatp format to DGSs and GATPs tools (GCL language, Coq AM, etc.).
The i2gatpformat will be backwards compatible with i2g format. DGSs should be able to read the i2gatp container ignoring the extra info. The GATPs should also be able to read the i2g format, adding information whenever needed.
The TGTP and GeoThms servers will use the i2gatp as its base format, providing converters to and from the di erent GATPs.
DGS code (GCLC) DGS code (GeoGebra) others
Graphical Rendering (SVG)
Human−Language
Rendering (HTML) 1 2 3 4 5
6 Container I2GATP
XML files TGTP
GeoThms
WGL others 7 8 9
GATP code (GCLC AM) GATP code (Coq AM) others 1 − From/to GCLC to/from I2G(ATP) 4 − SVG rendering 7 − From/to I2GATP to/from GCLC AM 2 − From/to GeoGebra to/from I2G(ATP) 5 − HTML rendering 8 − From/to I2GATP to/from Coq AM 3 − From/to DGS to/from I2G(ATP) 6 − other: proofs; bibrefs., etc. 9 − From/to I2GATP to/from GATP
Fig. 2. Conversions From/To i2gatp To/From Geometric Tools 5
A case for extending the i2g xml format to the description of geometric conjectures and as an interchange format for dynamic geometry software and geometry automated theorem proving tools was presented.
A brief description of the i2g format and the tools using it and also the tools that can bene t from the extended format was given. The overall architecture and physical organisation of the i2gatp format was described. Arguments justifying the usefulness of this extended format were discussed.
The work presented in this paper is related to work in other domains of
automated reasoning where joint e orts of numerous researchers led to standards
and libraries which are very fruitful for easier exchange of problems, proofs, and
even program code, contributing to the advance of the underlying eld (see [
This is a work-in-progress. Questions and future work to be addressed: { The xml format must be complemented with an extensive set of converters allowing the exchange of information between as many geometric tools as possible. { The databases queries, as in TGTP , raise the question of selecting appropriate keywords. A ne grain index and/or an appropriate geometry ontology should be addressed. { The i2gatp format does not address proofs. Should we try to create such a format? The GATPs produce proofs in quite di erent formats, maybe the construction of such unifying format it is not possible and/or desirable in this area.
The i2gatp format will allow to further extend the database of geometric constructions within GeoThms and TGTP and, hopefully lead then to a major public resource for geometric constructions, linking a signi cant number of geometry tools under this new format. 16. Pedro Quaresma. The i2gatp format. Technical report, CISUC, 2012. (http: //hilbert.mat.uc.pt/TGTP/Documents/Docs/cisucTRi2gatp.pdf). 17. Pedro Quaresma and Predrag Janicic. GeoThms { a Web System for euclidean constructive geometry. Electronic Notes in Theoretical Computer Science, 174(2):35 { 48, 2007. 18. E. Santiago, Maxim Hendriks, Yves Kreis, Ulrich Kortenkamp, and Daniel Marques. i2g Common File Format Final Version. Technical Report D3.10, The Intergeo Consortium, 2010. 19. Vanda Santos and Pedro Quaresma. Integrating DGSs and GATPs in an adaptative and collaborative blended-learning Web-environment. In First Workshop on CTP Components for Educational Software (THedu'11), volume 79 of EPTCS, 2012. 20. Geo Sutcli e. The SZS ontologies for automated reasoning software. In P Rudnicki, G. Sutcli e, B. Konev, R. Schmidt, and S. Schulz, editors, Proceedings of the Combined KEAPPA - IWIL Workshops, pages 38{49, 2008.