Automated Deduction in Geometry

Name: Automated Deduction in Geometry | 8th International Workshop, ADG 2010, Munich, Germany, July 22-24, 2010, Revised Papers
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

8th International Workshop, ADG 2010, Munich, Germany, July 22-24, 2010, Revised Papers

Pascal Schreck Julien Narboux Jürgen Richter-Gebert(Herausgeber*in)

Springer (Verlag)

Erschienen am 10. November 2011

X, 259 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-25070-5 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Intro
Title
Preface
Organization
Table of Contents
Cancellation Patterns in Automatic Geometric Theorem Proving
Introduction
Definitions: Theorems and Proving Techniques
The Binomial Proving Method
How to Represent a Theorem?
The Ceva-Menelaus Proving Method
Modeling Theorems by Ceva-Menelaus Constructions
Fractions, Groups and Graphs
The Base Graph
Triangles in Ceva-Menelaus Proofs Are Triangles in
Biquadratic Fractions Are Quadrangles in
Chains of Quadrangles
Equivalence!
How to Derive a Ceva-Menelaus Proof from a Binomial Proof
From a Ceva-Menelaus Proof to a Binomial Proof
Conclusion
References
Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL
Introduction
On Nonstandard Analysis in Isabelle
Nonstandard Numbers
Two New Relations on the Hyperreals
The Harthong-Reeb System
From HR to the (Limited) Hyperreals and Back
Arithmetizing and Mechanizing Euler's Method
Formally Verifying an Arithmetization at the Scale
Interpreting the Arithmetization at the Scale
A Verified Arithmetization of the Straight Line
Discussion
Conclusion and Further Work
References
A Formalization of Grassmann-Cayley Algebra in Coq and Its Application to Theorem Proving in Projective Geometry
Introduction
Formal Grassmann-Cayley Algebra
The Underlying Vector Space
The Join Product
The Meet Product
Data-Structures
Representing the Vector Space Kn
Representing the Algebra Gn
Join Product
Meet Product
Duality
Theorem Proving in Projective Geometry
Modeling the Geometry of Incidence
Automating Proofs
Conclusion
References
Automatic Calculation of Plane Loci Using Gr\"{o}bner Bases and Integration into a Dynamic Geometry System
Introduction
Calculating Loci with Gröbner Bases
The Algorithm
Example
Integration of Locus Computation in JSXGraph
JSXGraph
Calculating Loci with JSXGraph
An Idea for Speed Improvements
Conclusion
References
Proof Documents for Automated Origami Theorem Proving
Introduction
Motivation
State of the Art of Origami Theorem Proving
Reasoning about Origami
Algorithm of Origami Construction and Proving
A Simple Example of Construction
Fold Principle
Program of Construction
Program of Proving
Method of Proving
Overview
Need for Proof Document
Local Geometrical Inference
Transformation to Logical Formula
Elimination of Unnecessary Predicates
Forming Equivalence and Collinear Relations
Algebraic Manipulation
Proof Document
Structure of Proof Document
Program, Prover Computation and Result Sections
Geometrical Reasoning Section
Algebraic Transformation Section
Conclusion
References
The Midpoint Locus of a Triangle in a Corner
Introduction
Setting up the Problem
Approximating the Locus with a Graphic-Numeric Method
Solving Algebraically
Visualizing the Algebraic Surface
The Rest of the Boundary
Inverse Problems
Summary and Open Questions
Appendix: Mathematica Code
References
Some Lemmas to Hopefully Enable Search Methods to Find Short and Human Readable Proofs for Incidence Theorems of Projective Geometry
Introduction
Chasles, Pascal, Brianchon
Desargue's Theorem
Desargue's in Cevian Case
The 3 Chords Theorem
The Dual of 3 Chords Theorem
The 3 Circles Theorem
The 4 Circles Theorem
Automatization
Conclusion
References
What Is a Line ?
Introduction: What Is a Line ?
Pappus Geometry: A Summary
Three Times Constrained Conics
Conditions, or Vector-Based Constraints for Conics
Examples of Non Naive Lines
Circles through One Fixed Point
Orthogonal Circles
Poincaré Half Circles Are Lines
Other Circles
Some Parabolas Are Lines
Conics through Three Fixed Points Are Lines
Playing with Some Theorems
Proof of the Three Circles Theorem
The Four Circles Theorem
A Butterfly Theorem
What Is a Point ?
Variants: A Zoo of Planes
Conclusion
References
On One Method of Proving Inequalities in Automated Way
Introduction
Basic Method
Parametrization of n-gons
Proving Inequalities by Introduction of Auxiliary Polynomials
Concluding Remarks
References
Thousands of Geometric Problems for Geometric Theorem Provers (TGTP)
Introduction
TGTP
Realm
The Web Interface
The List of Problems
Queries
Performance Information
Common File Format for Conjectures
Future Work
Conclusions
References
An Investigation of Hilbert's Implicit Reasoning through Proof Discovery in Idle-Time
Introduction
Declarative Formalisation
HOL Light
Incidence Reasoning
Incidence Rules
Incidence and Pasch's Axiom
Idle-Time Discovery
Overview of the System
Analysing Hilbert's Proofs
Theorem 4
Theorem 5
Conclusion and Further Work
References
A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs
Introduction
Background
ArgoCLP Proof Procedures
Basic Proof Procedure
Improved Proof Procedure
Techniques That Do Not Preserve Completeness
ArgoCLP Implementation
Applications
Related Work
Conclusions and Further Work
References
Automated Generation of Readable Proofs for Constructive Geometry Statements with the Mass Point Method
Introduction
Mass Point Geometry
Mass Point Geometry Preliminaries
Basic Propositions of Mass Point Geometry
Mass Point Method
Introductory Examples
The Hilbert Intersection Point Statesments
The Algorithm and Its Features
Implementing the Algorithm MPM in Maple
Running Examples
Further Discussion
The Complex Mass Point Geometry
The Basic Idea
The Properties of the Complex Mass Point Geometry
Complex Mass Point Method
Introductory Examples
Some Features
The Linear Constructive Geometry Statements
The Algorithm Complex Mass Point Method
Implementing the Algorithm CMPM in Maple
Running Examples
Experimental Results and Conclusions
Experimental Results
Conclusions and Future Work
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken