ALBERT

All Library Books, journals and Electronic Records Telegrafenberg

X
feed icon rss

Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
  • 1
    Unknown
    Mathematics mechanization and applications (2000)
    San Diego : Academic Press
    Details
    Keywords: DDC 511.3 ; LC QA218 ; Automatic theorem proving ; Equations - Numerical solutions - Data processing
    Pages: Online-Ressource (xix, 551 pages)
    ISBN: 9780127347608
    URL: http://www.sciencedirect.com/science/book/9780127347608
    Language: English
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    E-BOOK
  • 2
    Electronic Resource
    Electronic Resource
    On the automatic derivation of a set of geometric formulae (1995)
    Springer
    Journal of geometry 53 (1995), S. 79-88 
    Details
    ISSN: 1420-8997
    Source: Springer Online Journal Archives 1860-2000
    Topics: Mathematics
    Notes: Abstract Leta, b, andc be the three sides of a triangleABC, a i ,b i ,c i anda e ,b e , ce be the lengths of the three internal and external bisectors of the three anglesA, B, andC respectively. It is easy to express the bisectors as formulae of the sides. In this paper, we solve a problem proposed by H. Zassenhaus: for any three different bisectors in {ai, bi, ci, ae, be, ce}, finding the relations between each side of the triangle and the three chosen bisectors. We also prove that given any general values for three different bisectors (internal or external) of a triangle, we can not draw the triangle using a ruler and a pair of compasses alone. The formulae mentioned above are derived automatically using a general method of mechanical formula derivation.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF01224042
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 3
    Electronic Resource
    Electronic Resource
    On the parameterization of algebraic curves (1992)
    Springer
    Applicable algebra in engineering, communication and computing 3 (1992), S. 27-38 
    Details
    ISSN: 1432-0622
    Keywords: Geometric modeling ; Parameterization ; Algebraic curves ; Resolvents ; Ritt-Wu's decomposition algorithm ; Gröbner bases
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science , Mathematics , Technology
    Notes: Abstract In this paper, by using the concept of resolvents of a prime ideal introduced by Ritt, we give methods for constructing a hypersurface which is birational to a given irreducible variety and birational transformations between the hypersurface and the variety. In the case of algebraic curves, this implies that for an irreducible algebraic curveC, we can construct a plane curve which is birational toC. We also present a method to find rational parametric equations for a plane curve if it exists. Hence we have a complete method of parameterization for rational algebraic curves.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF01189021
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 4
    Electronic Resource
    Electronic Resource
    Automated generation of readable proofs with geometric invariants (1996)
    Springer
    Journal of automated reasoning 17 (1996), S. 325-347 
    Details
    ISSN: 1573-0670
    Keywords: automated reasoning ; automated geometry theorem proving ; area method ; multiple proof ; shortest proof ; 68T15
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract In this series of papers, we discuss how to use a fixed set of high level geometry lemmas or rules related to geometric invariants, such as area, full-angle, etc., to produce short and human-readable proofs in geometry, especially to produce multiple and shortest proofs of a given geometry theorem. These rules are proved to be much more effective and concise than the rules based on triangle congruence used in related work before. The success of our approach is partially due to a skillful selection of geometric invariants and the related rules. Control and search strategies are proposed and experimented with to enhance the efficiency of the pover. In part I of this series, the high level geometry lemmas are about area and the Ceva-Menelaus configurations.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF00283133
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 5
    Electronic Resource
    Electronic Resource
    Automated generation of readable proofs with geometric invariants (1996)
    Springer
    Journal of automated reasoning 17 (1996), S. 349-370 
    Details
    ISSN: 1573-0670
    Keywords: automated reasoning ; automated geometry theorem proving ; method based on angle ; forward chaining ; backward chaining
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract We present a set of rules based on full-angles as the basis of automated geometry theorem proving. We extend the idea of eliminating variables and points to the idea of eliminating lines. We also discuss how to combine the forward chaining and backward chaining to achieve higher efficiency. The prover based on the full-angle method has been used to produce short and elegant proofs for more than one hundred difficult geometry theorems. The proofs of many of those theorems produced by our previous area method are relatively long.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF00283134
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 6
    Electronic Resource
    Electronic Resource
    Automated reasoning in differential geometry and mechanics using the characteristic set method (1993)
    Springer
    Journal of automated reasoning 10 (1993), S. 161-172 
    Details
    ISSN: 1573-0670
    Keywords: Differential polynomial ; weak ascending chain ; W-perm ; Ritt-Wu's principle ; quasi zero set ; Ritt-Wu's decomposition algorithm
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract This is the first paper of a series of three papers under the same title. It presents an improved version of Ritt-Wu's decomposition algorithm which is the basis of our methods of mechanical theorem proving and mechanical formula derivation in differential geometry and elementary mechanics. We improve the original algorithm in two aspects. First, by using the weak ascending chain and W-perm, the sizes of the differential polynomials occurring in the decomposition can be reduced. Second, by using a special reduction procedure, the number of branches in the decomposition can be controlled effectively. The improved version significantly enhances the efficiency of the original algorithm.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF00881834
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 7
    Electronic Resource
    Electronic Resource
    Automated reasoning in differential geometry and mechanics using the characteristic set method (1993)
    Springer
    Journal of automated reasoning 10 (1993), S. 173-189 
    Details
    ISSN: 1573-0670
    Keywords: Mechanical theorem proving ; Wu's method ; Ritt-Wu's decomposition algorithm ; statement of equation type ; generally true ; universally true ; space curve theory ; elementary mechanics
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract We clarify the formulation problem of mechanical theorem proving in differential geometry and mechanics and propose two formulations. We present complete methods of mechanical theorem proving for the two formulations. We also introduce predicates and a language to translate geometry statements into differential polynomial equations. A program based on our methods has proved more than 100 nontrivial theorems in differential geometry and elementary mechanics including various classification theorems for space curves, Bertrand's Theorem, Newton's gravitational laws, etc.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF00881835
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 8
    Electronic Resource
    Electronic Resource
    A Deductive Database Approach to Automated Geometry Theorem Proving and Discovering (2000)
    Springer
    Journal of automated reasoning 25 (2000), S. 219-246 
    Details
    ISSN: 1573-0670
    Keywords: deductive database ; automated geometry theorem proving and discovering ; search strategies ; redundant deduction ; Skolemization ; structured database
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract We report our effort to build a geometry deductive database, which can be used to find the fixpoint for a geometric configuration. The system can find all the properties of the configuration that can be deduced using a fixed set of geometric rules. To control the size of the database, we propose the idea of a structured deductive database. Our experiments show that this technique could reduce the size of the database by one hundred times. We propose the data-based search strategy to improve the efficiency of forward chaining. We also make clear progress in the problems of how to select good geometric rules, how to add auxiliary points, and how to construct numerical diagrams as models automatically. The program is tested with 160 nontrivial geometry configurations. For these geometric configurations, the program not only finds most of their well-known properties but also often gives unexpected results, some of which are possibly new. Also, the proofs generated by the program are generally short and totally geometric.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1006171315513
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 9
    Electronic Resource
    Electronic Resource
    Automated production of traditional proofs in solid geometry (1995)
    Springer
    Journal of automated reasoning 14 (1995), S. 257-291 
    Details
    ISSN: 1573-0670
    Keywords: automated theorem proving ; Euclidean traditional proofs ; volume method ; constructive geometry statements
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract This paper presents a method of producing readable proofs for theorems in solid geometry. The method is for a class of constructive geometry statements about straight lines, planes, circles, and spheres. The key idea of the method is to eliminate points from the conclusion of a geometric statement using several (fixed) high-level basic propositions about the signed volumes of tetrahedrons and Pythagorean differences of triangles. We have implemented the algorithm, and more than 80 examples from solid geometry have been used to test the program. Our program is efficient and the proofs produced by it are generally short and readable.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF00881858
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 10
    Electronic Resource
    Electronic Resource
    Automated production of traditional proofs for theorems in Euclidean geometry I. The Hilbert intersection point theorems (1995)
    Springer
    Annals of mathematics and artificial intelligence 13 (1995), S. 109-137 
    Details
    ISSN: 1573-7470
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science , Mathematics
    Notes: Abstract We present a method which can produce traditional proofs for a class of constructive geometry statements in Euclidean geometry. The method is a mechanization of the traditional area method used by many geometers. The key idea of our method is to eliminate dependent (constructed) points in a geometry statement using a few basic geometry propositions about the area of triangles. The method has been implemented. Our program, calledEuclid, can produce traditional proofs of many hard geometry theorems such as Pappus' theorem, Pascal's theorem, Gauss point theorem, and the Pascal conic theorem. Currently, it has produced proofs of 110 nontrivial theoremsentirely automatically. The proofs produced byEuclid are elegant, short (often shorter than the proofs given by geometers) and understandable even to high school students. This method seems to be the first that can produce traditional proofs for hard geometry theorems automatically.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF01531326
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...