cmb33595 / open-geo-prover Goto Github PK
View Code? Open in Web Editor NEWAutomatically exported from code.google.com/p/open-geo-prover
Automatically exported from code.google.com/p/open-geo-prover
Currently OGP provides only construction of angle bisector for given angle.
However, it would be also useful to have a construction of congruent angle as
well.
Steps to do:
1. Create new construction type: construction of second angle ray for given
first ray, vertex and congruent angle. E.g. construct ray r=OB of angle <AOB
for given points A and O and given angle <DEF which is congruent to <AOB (and
with same orientation).
2. Create OGP XML Converter necessary for XML input of this type of
construction.
Please see attached picture: it is example of construction for proving Euler's
theorem - to construct point A from that example, OGP must provide the
construction of congruent angle.
Original issue reported on code.google.com by [email protected]
on 22 Jan 2012 at 3:40
Attachments:
Construction Protocol has to be improved to remove all unnecessary
constructions i.e. those constructions not required for theorem statement. That
way input system of polynomials will be much simpler and therefore theorem
proof will be faster.
This improvement has to be merged to GeoGebra dedicated trunk as well.
Original issue reported on code.google.com by ivan.petrovic.matf
on 4 Jun 2012 at 11:49
This issue document is for work to delete unnecessary directories and other
resources from main development project.
Original issue reported on code.google.com by [email protected]
on 4 Mar 2012 at 10:17
GeoGebra commands for all types of reflections have been converted to OGP
constructions. The same has to be done for other types of geometry
transformations supported by GeoGebra:
1. rotations,
2. translations and
3. dilatations.
Original issue reported on code.google.com by ivan.petrovic.matf
on 4 Jun 2012 at 11:57
Current term "Construction Protocol" should be replaced by "Theorem Protocol"
since it really contains information about entire theorem, not only about
construction steps for the theorem.
Therefore, all related classes and packages have to be properly renamed.
Original issue reported on code.google.com by ivan.petrovic.matf
on 9 Jun 2012 at 8:58
OGP already has logging facility provided by Apache's log4j library which is
compatible with GPL license.
However, it has to be replaced for GeoGebra's prover for two reasons:
1. GeoGebra needs only one .jar file of OGP and don't want to take other 3rd
party libs in order to keep its .jar file as small as possible.
2. GeoGebra already has its own logger and wants to use the same in its prover.
To achieve this it is required:
1. firstly to examine existing GeoGebra logger;
2. then to implement logger interface in OGP on main development trunk and
therefore provide the ability of easy replacement of logger implementations;
3. to download code for GeoGebra logger from GeoGebra source and put it into
single logger implementation class that implements the OGP logger interface.
This will be done only in OGP branch dedicated for GeoGebra.
Sub-stages of work where this issue belongs are:
A.2. and A.5.
Original issue reported on code.google.com by ivan.petrovic.matf
on 21 May 2012 at 8:12
It is necessary to implement API method for calling OGP prover from GeoGebra
code.
The method should receive input prover parameters and the theorem
(constructions and statement) in XML format and should return output results
with NDG conditions list.
Original issue reported on code.google.com by ivan.petrovic.matf
on 9 Jun 2012 at 11:30
It is required to add QDParser (quick and dirty parser) for parsing XML files
for input of geometry constructions. The same parser is used in GeoGebra code.
1. Take QDParser.java file from development trunk of GeoGebra and integrate in
OGP's branch for GeoGebra.
2. Take DocHandler.java interface from GeoGebra's development trunk and
integrate in OGP's branch for GeoGebra.
3. Implement custom document handler for purpose of parsing XML files with
constructions imported from GeoGebra side (XML input will be in GeoGebra's XML
format and only construction part will be present i.e. all between tags
<construction> and </construction> including these 2 tags).
Original issue reported on code.google.com by [email protected]
on 8 Apr 2012 at 11:37
In attachment there is theorem whose proving fails with following error:
Exception in thread "main" java.lang.StackOverflowError
at java.util.ArrayList.grow(ArrayList.java:242)
at java.util.ArrayList.ensureExplicitCapacity(ArrayList.java:216)
at java.util.ArrayList.ensureCapacityInternal(ArrayList.java:208)
at java.util.ArrayList.add(ArrayList.java:440)
at
com.ogprover.pp.tp.geoconstruction.PerpendicularLine.getInputLabels(Perpendicula
rLine.java:502)
Original issue reported on code.google.com by ivan.petrovic.matf
on 16 Jan 2015 at 7:55
Attachments:
1. Creation of new branch of OGP to be used within GeoGebra.
2. Cleanup of this new branch - removing unnecessary resources, adding new
resources etc.
Original issue reported on code.google.com by [email protected]
on 4 Mar 2012 at 11:20
There is a bug when running help of OGP project from command line:
When user normally executes OGP from command line with some prover parameters,
prover terminates normally and shows prompt line after execution. But when "-h"
or "--help" is put instead of plain prover parameters of command line, in order
to see prover help, the help contents is displayed but prompt line doesn't
appear - it is misleading and looks like user has to insert something, but
actually he has to type "Ctrl+C" to terminate the process.
Please provide normal process termination in case when project help is being
displayed.
Original issue reported on code.google.com by [email protected]
on 4 Mar 2012 at 10:27
Code for Area Method is merged from OGP branch for GeoGebra up to main
development trunk.
However, this method still cannot be tested and executed on main Dev trunk
since input methods do not support Area Method. On GeoGebra branch, there are
converters of GeoGebra input for algebraic and area methods and therefore Area
method can be tested and executed there.
It is required to implement necessary changes on non-GeoGebra branches in order
to provide conversion of input theorems to format suitable for Area Method in
order to be able to use it.
Original issue reported on code.google.com by ivan.petrovic.matf
on 2 Nov 2013 at 5:53
It is necessary to implement the converter of geometry theorem statements from
GeoGebra to OGP format.
Theorems are passed to OGP as strings in form "name[arg1, arg2, ..., argn]".
Later they could be passed in some other format and then new type of conversion
would be required.
Original issue reported on code.google.com by ivan.petrovic.matf
on 24 May 2012 at 10:37
This issue is for initial implementation of parametric sets of points and one
their version - conic sections.
Original issue reported on code.google.com by [email protected]
on 15 Feb 2012 at 5:37
1. First of all, implementation of Area Method will be merged from "OGP for
GeoGebra with Area Method" branch down to base "OGP for GeoGebra" branch.
2. Next, special branch for Area Method will be deleted.
3. Then implementation of Area Method will be merged up to main development
trunk of OGP.
4. Finally, implementation of Area Method will be merged down to other branches
(at this moment it is only branch for Full Angle Method which is cut from main
trunk).
Original issue reported on code.google.com by ivan.petrovic.matf
on 1 Nov 2013 at 6:17
NDG conditions will be represented in following way:
"ndgCondName[arg1, arg2, ..., argn]"
e.g. "collinearPoints[A, B, C]".
This representation is general and more suitable for conversion to other
formats (like textual representation, multilingual text representation,
constructions of special cases of theorems etc).
For OGP internal use there will be a method for conversion of this
representation to textual form.
For GeoGebra it will be enough just to send NDGs in this general format.
Unconverted NDGs from polynomial representation will be shown as polynomials.
For this purpose it is required to implement method for printing of polynomials
in ASCII character set without any special formatting e.g.:
(2*u1^3 - 5*u1)*x3^4*x2*x1^5 - 4*x2*x1^4 + x2 = 0.
Original issue reported on code.google.com by ivan.petrovic.matf
on 5 Jun 2012 at 12:13
1. All third party libraries have to be reviewed to see if their licenses are
GPL compatible.
2. Prompt message that appears on starting of OGP prover, when it is run from
command line, must be updated to match GPL v3 license.
3. Corresponding disclaimer has to be added to all source code.
Original issue reported on code.google.com by [email protected]
on 4 Mar 2012 at 10:31
This issue is main place to submit all changes that fix small bugs found in OGP
when it is run from GeoGebra prover. These small bugs are made in initial
development covered by other issue documents, but they cover implementation
tasks. So this is central place for all errors made in implementation of
various parts of integration.
If any reported bug requires significant change or even reimplementation of
some greater part of code that affects the logic of prover, then a separate
issue has to be created to address that problem.
Original issue reported on code.google.com by ivan.petrovic.matf
on 17 Jun 2012 at 1:20
Steps to reproduce the problem:
1. Start project compilation from <dist> target of Ant build file.
2. Notice the output messages in Eclipse - there is no [junit] task executed.
Task [junit] should appear in log messages in Eclipse console when that task is
executed. The issue is that it is not executed.
Original issue reported on code.google.com by [email protected]
on 18 Dec 2011 at 1:45
1. Creating new type of shortcut construction for list of simple constructions.
2. Fixing name of construction of reflected point.
Original issue reported on code.google.com by ivan.petrovic.matf
on 14 May 2012 at 10:17
This issue document is for initial implementation of support for solving
RC-constructibility problems. These problems will be solved by algebraic method
which uses simple triangulation algorithm (from Wu's method) to separate
variables.
Original issue reported on code.google.com by ivan.petrovic.matf
on 14 Jul 2012 at 10:47
1. Ant build.xml file has to be improved to create minimal .jar file that will
include only compiled classes, not additional resources like source code etc.
2. It is required to create a Linux shell script for compilation of OGP outside
of Eclipse IDE.
Original issue reported on code.google.com by ivan.petrovic.matf
on 9 Jun 2012 at 11:14
It would be nice if we could get the NDG conditions back with the same objects
as we send from GeoGebra.
Let's consider the following example:
...
d=Line[C,D]
e=Line[A,E]
...
h=ProveDetails[...]
Now we can get an NDG condition from OGP like this:
AreParallel[D,C,E,A]
But this is a little bit unelegant, and may be confusing for the GeoGebra
users. Instead, it would be more beautiful to get AreParallel[e,d], or even
better if the parameters would be alphabetically ordered (AreParallel[d,e]).
Original issue reported on code.google.com by [email protected]
on 14 Jul 2012 at 2:45
Documentation of OGP has to contain several examples of theorems proved with
simple Wu's method. Input is in OGP's internal XML format, while output is
generated TeX report translated to PDF.
Original issue reported on code.google.com by [email protected]
on 4 Mar 2012 at 4:57
Following constructions should be added to OGP:
1. Construction of angle of 60 degrees;
2. "Construction" of angle's trisector;
3. Construction of triple angle;
4. Construction of third addend for two given angles to angle of 60 degrees.
Also following theorem statements should be added:
1. Equilateral triangle;
2. Angle of specified size (e.g. 60 degrees);
3. Linear combination of squares of segments' lengths.
These constructions and statements are necessary to be able to prove several
well known geometry theorems, like Morley's theorem.
Original issue reported on code.google.com by [email protected]
on 19 Feb 2012 at 3:35
Construction of tangent line from given point to given circle/conic should implicitly construct a touch point of that line and specified circle/conic. Currently this is not the case and therefore conversion of construction protocol to algebraic form may fail assuming this point is implicitly constructed.
Workaround for this issue is to explicitly add construction of this touch point.
Example:
These construction steps will fail to convert to polynomial form:
<pfree label="$A$" />
<pfree label="$H_{a}$" />
<pfree label="$I$" />
<ltwopts label ="$h_{a}$" point1="$A$" point2="$H_{a}$" />
<lperp label ="$a$" point="$H_{a}$" baseline="$h_{a}$" />
<pfoot label ="$P_{\_G14517}$" origpt="$I$" baseline="$a$" />
<ccenterpt label ="$k(I,P_{a})$" center="$I$" point="$P_{\_G14517}$" />
<ltangent label ="$c$" basept="$A$" pointset="$k(I,P_{a})$" />
<ltangent label ="$b$" basept="$A$" pointset="$k(I,P_{a})$" />
<pintersect label ="$B$" set1="$c$" set2="$a$" />
<pintersect label ="$C$" set1="$a$" set2="$b$" />
In these steps, there is tangent line c which by construction has only one point A, the point from which it has been constructed as a tangent to circle k. We assume it also has a touch point with circle k but that point currently is not implicitly constructed in OGP and that is an issue. Similarly, tangent line b has only one point A explicitly constructed. Then in last construction steps, points B and C are constructed as intersection points of line a and one of these tangents (b and c respectively). But, to transform these steps to polynomial form, each of two lines that intersect each other have to have at least 2 points, which is not the case since both b and c have just 1 point each.
Workaround for this is to explicitly add touch point (in construction sample below they are marked with comments "add 1" and "add 2" before each of them):
<pfree label="$A$" />
<pfree label="$H_{a}$" />
<pfree label="$I$" />
<ltwopts label ="$h_{a}$" point1="$A$" point2="$H_{a}$" />
<lperp label ="$a$" point="$H_{a}$" baseline="$h_{a}$" />
<pfoot label ="$P_{\_G14517}$" origpt="$I$" baseline="$a$" />
<ccenterpt label ="$k(I,P_{a})$" center="$I$" point="$P_{\_G14517}$" />
<ltangent label ="$c$" basept="$A$" pointset="$k(I,P_{a})$" />
<!-- add 1 -->
<pintersect label ="$C1$" set1="$c$" set2="$k(I,P_{a})$" />
<ltangent label ="$b$" basept="$A$" pointset="$k(I,P_{a})$" />
<!-- add 2 -->
<pintersect label ="$B1$" set1="$b$" set2="$k(I,P_{a})$" />
<pintersect label ="$B$" set1="$c$" set2="$a$" />
<pintersect label ="$C$" set1="$a$" set2="$b$" />
Original issue reported on code.google.com by ivan.petrovic.matf
on 16 Jan 2015 at 7:51
This issue is about implementation of usage of log file whose destination
(path) and name are set by user.
Original issue reported on code.google.com by ivan.petrovic.matf
on 14 Jun 2012 at 9:02
If there are multiple Prove (or ProveDetails) commands in the XML given, then
GeoGebra should communicate which one to be proven by OpenGeoProver.
Maybe it would be a good solution to pass the name of the object as well. E.g. a
h=ProveDetails[AreEqual[C,D]]
could be selected by sending the object "h" to OGP.
Original issue reported on code.google.com by [email protected]
on 14 Jul 2012 at 2:39
1. XML of GeoGebra could have Prove command with input which is statement
command in infix notations that uses Unicode characters in UTF-8 format. They
are mainly used to express equality. Modify XML parsing of Prove command to
cover these cases.
2. New input parameters (like format of OGP report, path of log file etc.) have
to be defined for usage of OGP from GeoGebra.
Original issue reported on code.google.com by ivan.petrovic.matf
on 14 Jun 2012 at 9:00
GeoGebra command for intersection point can return more then one point (e.g.
intersections of two circles or of a circle and a line return 2 points each,
while intersection of two ellipses return 4 points in total).
Prover cannot distinguish between 2 intersection points if they are both
constructed in same way - to satisfy condition that belong to each of two point
sets. Instead of that, only one can be constructed this way, and another is
constructed differently:
1. If line intersects a circle, first construct foot of circle center to given
line and then construct central symmetric point of first intersection point
w.r.t. foot point.
2. If two circles intersect each other, reflect first intersection point about
central line (line which connects centers of given circles).
There are also issues when new intersection points are constructed (so with new
labels) but some of previous constructed points satisfy condition for
intersection point. In that case some of new points has to be renamed by label
of old point. GeoGebra offers coordinates of constructed points in its XML and
this can be used to compare points (when they are same but with different
labels). That way we can know what old point to use to rename new intersection
point. But this work is scheduled for next stage/phase of integration
development.
Original issue reported on code.google.com by ivan.petrovic.matf
on 20 Jun 2012 at 12:30
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.