TY - JOUR

T1 - Reconstruction of polyhedra by a mechanical theorem proving method

AU - Koh, Kyun

AU - Deguchi, Koichiro

AU - Morishita, Iwao

PY - 1993/4/1

Y1 - 1993/4/1

N2 - 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 pseudo-divided 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 calculated its spatial angle by direct manipulation of the hypothesis polynomials and the conjecture polynomial. But we show that by stability analysis of the pseudo-divided remainder the spatial angles can be calculated even in those regions.

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 pseudo-divided 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 calculated its spatial angle by direct manipulation of the hypothesis polynomials and the conjecture polynomial. But we show that by stability analysis of the pseudo-divided remainder the spatial angles can be calculated even in those regions.

UR - http://www.scopus.com/inward/record.url?scp=0027582940&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0027582940&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0027582940

VL - E76-D

SP - 437

EP - 445

JO - IEICE Transactions on Information and Systems

JF - IEICE Transactions on Information and Systems

SN - 0916-8532

IS - 4

ER -