In this paper we propose a new application of Wu's mechanical theorem proving method to reconstruct polyhedra in 3-D space from their projection image. First we set up three groups of equations. The first group is of the geometric relations expressing that vertices are on a plane segment, on a line segment, and forming angle in 3-D space. The second is of those relations on image plane. And the rest is of the relations between the vertices in 3-D space and their correspondence on image plane. Next, we classify all the groups of equations into two sets, a set of hypotheses and a conjecture. We apply this method to seven cases of models. Then, we apply Wu's method to prove that the hypotheses follow the conjecture and obtain pseudodivided remainders of the conjectures, which represent relations of angles or lengths between 3-D space and their projected image. By this method we obtained new geometrical relations for seven cases of models. We also show that, in the region in image plane where corresponding spatial measures cannot reconstructed, leading coefficients of hypotheses polynomials approach to zero. If the vertex of an image angle is in such regions, we cannot calculate its spatial angle by direct manipulation of the hypothesis polynomials and the conjecture polynomial. But we show that by stability analysis of the pseudodivided remainder the spatial angles can be calculated even in those regions.
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Copy
Kyun KOH, Koichiro DEGUCHI, Iwao MORISHITA, "Reconstruction of Polyhedra by a Mechanical Theorem Proving Method" in IEICE TRANSACTIONS on Information,
vol. E76-D, no. 4, pp. 437-445, April 1993, doi: .
Abstract: In this paper we propose a new application of Wu's mechanical theorem proving method to reconstruct polyhedra in 3-D space from their projection image. First we set up three groups of equations. The first group is of the geometric relations expressing that vertices are on a plane segment, on a line segment, and forming angle in 3-D space. The second is of those relations on image plane. And the rest is of the relations between the vertices in 3-D space and their correspondence on image plane. Next, we classify all the groups of equations into two sets, a set of hypotheses and a conjecture. We apply this method to seven cases of models. Then, we apply Wu's method to prove that the hypotheses follow the conjecture and obtain pseudodivided remainders of the conjectures, which represent relations of angles or lengths between 3-D space and their projected image. By this method we obtained new geometrical relations for seven cases of models. We also show that, in the region in image plane where corresponding spatial measures cannot reconstructed, leading coefficients of hypotheses polynomials approach to zero. If the vertex of an image angle is in such regions, we cannot calculate its spatial angle by direct manipulation of the hypothesis polynomials and the conjecture polynomial. But we show that by stability analysis of the pseudodivided remainder the spatial angles can be calculated even in those regions.
URL: https://global.ieice.org/en_transactions/information/10.1587/e76-d_4_437/_p
Copy
@ARTICLE{e76-d_4_437,
author={Kyun KOH, Koichiro DEGUCHI, Iwao MORISHITA, },
journal={IEICE TRANSACTIONS on Information},
title={Reconstruction of Polyhedra by a Mechanical Theorem Proving Method},
year={1993},
volume={E76-D},
number={4},
pages={437-445},
abstract={In this paper we propose a new application of Wu's mechanical theorem proving method to reconstruct polyhedra in 3-D space from their projection image. First we set up three groups of equations. The first group is of the geometric relations expressing that vertices are on a plane segment, on a line segment, and forming angle in 3-D space. The second is of those relations on image plane. And the rest is of the relations between the vertices in 3-D space and their correspondence on image plane. Next, we classify all the groups of equations into two sets, a set of hypotheses and a conjecture. We apply this method to seven cases of models. Then, we apply Wu's method to prove that the hypotheses follow the conjecture and obtain pseudodivided remainders of the conjectures, which represent relations of angles or lengths between 3-D space and their projected image. By this method we obtained new geometrical relations for seven cases of models. We also show that, in the region in image plane where corresponding spatial measures cannot reconstructed, leading coefficients of hypotheses polynomials approach to zero. If the vertex of an image angle is in such regions, we cannot calculate its spatial angle by direct manipulation of the hypothesis polynomials and the conjecture polynomial. But we show that by stability analysis of the pseudodivided remainder the spatial angles can be calculated even in those regions.},
keywords={},
doi={},
ISSN={},
month={April},}
Copy
TY - JOUR
TI - Reconstruction of Polyhedra by a Mechanical Theorem Proving Method
T2 - IEICE TRANSACTIONS on Information
SP - 437
EP - 445
AU - Kyun KOH
AU - Koichiro DEGUCHI
AU - Iwao MORISHITA
PY - 1993
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E76-D
IS - 4
JA - IEICE TRANSACTIONS on Information
Y1 - April 1993
AB - In this paper we propose a new application of Wu's mechanical theorem proving method to reconstruct polyhedra in 3-D space from their projection image. First we set up three groups of equations. The first group is of the geometric relations expressing that vertices are on a plane segment, on a line segment, and forming angle in 3-D space. The second is of those relations on image plane. And the rest is of the relations between the vertices in 3-D space and their correspondence on image plane. Next, we classify all the groups of equations into two sets, a set of hypotheses and a conjecture. We apply this method to seven cases of models. Then, we apply Wu's method to prove that the hypotheses follow the conjecture and obtain pseudodivided remainders of the conjectures, which represent relations of angles or lengths between 3-D space and their projected image. By this method we obtained new geometrical relations for seven cases of models. We also show that, in the region in image plane where corresponding spatial measures cannot reconstructed, leading coefficients of hypotheses polynomials approach to zero. If the vertex of an image angle is in such regions, we cannot calculate its spatial angle by direct manipulation of the hypothesis polynomials and the conjecture polynomial. But we show that by stability analysis of the pseudodivided remainder the spatial angles can be calculated even in those regions.
ER -