IDEAS home Printed from https://ideas.repec.org/a/gam/jmathe/v11y2023i5p1079-d1076013.html
   My bibliography  Save this article

Formal Verification of a Topological Spatial Relations Model for Geographic Information Systems in Coq

Author

Listed:
  • Sheng Yan

    (Beijing Key Laboratory of Space-Ground Interconnection and Convergence, School of Electronic Engineering, Beijing University of Posts and Telecommunications, Beijing 100876, China)

  • Wensheng Yu

    (Beijing Key Laboratory of Space-Ground Interconnection and Convergence, School of Electronic Engineering, Beijing University of Posts and Telecommunications, Beijing 100876, China)

Abstract

Geographic information systems have undergone rapid growth for decades. Topology has provided valuable modeling tools in the development of this field. Formal verification ofthe model of topological spatial relations can provide a reliable guarantee for the correctness of geographic information systems. We present a proof of the topological spatial relations model that has been formally verified in the Coq proof assistant. After an introduction to the formalization of the axiomatic set theory of Morse–Kelley, the formal description of the elementary concepts and properties of general topology is developed. The topological spatial relations between two sets are described by using the concept of the intersection value. Finally, we formally proved the topological spatial relations between two sets which are restricted to the regularly closed and the planar spatial regions. All the proof details are strictly completed in Coq, which shows that the correctness of the theoretical model for geographic information systems can be checked by a computer. This paper provides a novel method to verify the correctness of the topological spatial relations model. This work can also contribute to the creation and validation of various geological models and software.

Suggested Citation

  • Sheng Yan & Wensheng Yu, 2023. "Formal Verification of a Topological Spatial Relations Model for Geographic Information Systems in Coq," Mathematics, MDPI, vol. 11(5), pages 1-18, February.
    • Handle: RePEc:gam:jmathe:v:11:y:2023:i:5:p:1079-:d:1076013
    as

    Download full text from publisher

    File URL: https://www.mdpi.com/2227-7390/11/5/1079/pdf
    Download Restriction: no
    File URL: https://www.mdpi.com/2227-7390/11/5/1079/
    Download Restriction: no
    ---><---

    References listed on IDEAS

    as
    1. Yaoshun Fu & Wensheng Yu, 2021. "Formalizing Calculus without Limit Theory in Coq," Mathematics, MDPI, vol. 9(12), pages 1-24, June.
    Full references (including those not matched with items on IDEAS)

    Citations

    Citations are extracted by the CitEc Project, subscribe to its RSS feed for this item.
    as


    Cited by:

    1. Siran Lei & Hao Guan & Jianguo Jiang & Yu Zou & Yongsheng Rao, 2023. "A Machine Proof System of Point Geometry Based on Coq," Mathematics, MDPI, vol. 11(12), pages 1-16, June.
    2. Chanjuan Liu & Ruining Zhang & Yu Zhang & Enqiang Zhu, 2023. "A Formal Representation for Intelligent Decision-Making in Games," Mathematics, MDPI, vol. 11(22), pages 1-11, November.

    Most related items

    These are the items that most often cite the same works as this one and are cited by the same works as this one.
    1. Siran Lei & Hao Guan & Jianguo Jiang & Yu Zou & Yongsheng Rao, 2023. "A Machine Proof System of Point Geometry Based on Coq," Mathematics, MDPI, vol. 11(12), pages 1-16, June.

    Corrections

    All material on this site has been provided by the respective publishers and authors. You can help correct errors and omissions. When requesting a correction, please mention this item's handle: RePEc:gam:jmathe:v:11:y:2023:i:5:p:1079-:d:1076013. See general information about how to correct material in RePEc.

    If you have authored this item and are not yet registered with RePEc, we encourage you to do it here. This allows to link your profile to this item. It also allows you to accept potential citations to this item that we are uncertain about.

    If CitEc recognized a bibliographic reference but did not link an item in RePEc to it, you can help with this form .

    If you know of missing items citing this one, you can help us creating those links by adding the relevant references in the same way as above, for each refering item. If you are a registered author of this item, you may also want to check the "citations" tab in your RePEc Author Service profile, as there may be some citations waiting for confirmation.

    For technical questions regarding this item, or to correct its authors, title, abstract, bibliographic or download information, contact: MDPI Indexing Manager (email available below). General contact details of provider: https://www.mdpi.com .

    Please note that corrections may take a couple of weeks to filter through the various RePEc services.

    IDEAS is a RePEc service. RePEc uses bibliographic data supplied by the respective publishers.