申請者氏名	Requested Supervising Professor
高橋　和子	Kazuko TAKAHASHI
研究題目	Title of the project
	Symbolic modeling of spatial theories and verification of their properties using theorem proving technique
博士研究員への要望・専門、経験等	Qualifications for Postdoctoral Fellow including academic and non-academic background, research fields and interests
	1. Background of mathematical logic. 2. Interests and experiences on at least one of the following research fields. - logic programming/functional programming - theorem proving (theory/tool) - spatial reasoning
研究計画	Details on research project
	Study on a symbolic representation for spatial data and their reasoning system, and give a formal proof of its correctness using mechanical a theorem prover. Specifically: 1. Constructing a symbolic model of a topological theory or a computational geometry, and giving a mechanical proof of the theorems holding on them. 2. Providing a representation and verification of the properties of qualitative spatial theory such as region connection calculus, point calculus, or PLCA developed in our laboratory. We describe their axioms and theorems, and give a formal verification using a proof assistant or a theorem prover such as Isabelle, Coq and so on. 3. Formalization of geometric property by a symbolic representation and giving their computational proof. The details are determined by a further discussion. Aims: 1. Giving a formal proof for spatial theory using theorem proving technique. 2. Exploration of a new application field of theorem proving. URL (In Japanese):  http://ist.ksc.kwansei.ac.jp/~ktaka/LABO/index.html
BACK to LIST