Skip to main content
SpringerLink
Log in

Using Three-Valued Logic to Specify and Verify Algorithms of Computational Geometry

  • Conference paper
Formal Methods and Software Engineering (ICFEM 2005)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 3785))

Included in the following conference series:

Abstract

Many safety-critical systems deal with geometric objects. Reasoning about the correctness of such systems is mandatory and requires the use of basic definitions of geometry for the specification of these systems. Despite the intuitive meaning of such definitions, their formalisation is not at all straightforward: In particular, degeneracies lead to situations where none of the Boolean truth values adequately defines a geometric primitive. Therefore, we use a three-valued logic for the definition of geometric primitives to explicitly handle such degenerate cases. We have implemented a three-valued library of linear geometry in an interactive theorem prover for higher order logic which allows us to specify and verify entire algorithms of computational geometry.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bolc, L., Borowik, P.: Many-Valued logics. Springer, Heidelberg (1992)

    MATH  Google Scholar 

  2. Brandt, J., Schneider, K.: Dependable polygon-processing algorithms for safety-critical embedded systems. In: Yang, L.T., Amamiya, M., Liu, Z., Guo, M., Rammig, F.J. (eds.) EUC 2005. LNCS, vol. 3824, pp. 405–417. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  3. Brzozowski, J., Seger, C.-J.: Asynchronous Circuits. Springer, Heidelberg (1995)

    Google Scholar 

  4. Burnikel, C., Mehlhorn, K., Schirra, S.: On degeneracy in geometric computations. In: Symposium on Discrete Algorithms (SODA), Arlington, Virginia, USA, pp. 16–23. ACM Press, New York (1994)

    Google Scholar 

  5. Chou, S., Gao, X., Zhang, J.: Machine Proofs in Geometry. World Scientific, Singapore (1994)

    MATH  Google Scholar 

  6. de Berg, M., van Kreveld, M., Overmars, M., Schwarzkopf, O.: Computational Geometry. Springer, Heidelberg (2000)

    MATH  Google Scholar 

  7. Edelsbrunner, H., Mücke, E.: Simulation of simplicity: a technique to cope with degenerate cases in geometric algorithms. ACM Transactions on Graphics 9(1), 66–104 (1990)

    Article  MATH  Google Scholar 

  8. Eichelberger, E.: Hazard detection in combinational and sequential switching circuits. IBM Journal of Research and Development 9, 90–99 (1965)

    Article  MATH  Google Scholar 

  9. Foley, J., van Dam, A., Feiner, S., Hughes, J.: Computer Graphics: Principles and Practice. Addison Wesley, Reading (2000)

    Google Scholar 

  10. Gordon, M., Melham, T.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

  11. Kleene, S.: Introduction to Metamathematics. North Holland, Amsterdam (1952)

    MATH  Google Scholar 

  12. Knuth, D.: Axioms and Hulls. LNCS, vol. 606. Springer, Heidelberg (1992)

    MATH  Google Scholar 

  13. Malik, S.: Analysis of cycle combinational circuits. IEEE Transactions on Computer Aided Design 13(7), 950–956 (1994)

    Article  Google Scholar 

  14. Mehlhorn, K., Näher, S.: The LEDA Platform of Combinatorial and Geometric Computing. Cambridge University Press, Cambridge (1999)

    Google Scholar 

  15. Pichardie, D., Bertot, Y.: Formalizing convex hull algorithms. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 346–361. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  16. Reps, T., Sagiv, M., Wilhelm, R.: Static program analysis via 3-valued logic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 15–30. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  17. Schuele, T., Schneider, K.: Three-valued logic in bounded model checking. In: Formal Methods and Models for Codesign (MEMOCODE), Verona, Italy. IEEE Computer Society Press, Los Alamitos (2005)

    Google Scholar 

  18. Wu, W.-T.: On the decision problem and the mechanization of theorem proving in elementary geometry. Scientia Sinica 21, 157–179 (1978)

    Google Scholar 

  19. Yamamoto, M., Nishizaki, S., Hagiya, M.: Formalization of planar graphs. In: Schubert, E.T., Alves-Foss, J., Windley, P. (eds.) HUG 1995. LNCS, vol. 971, pp. 369–384. Springer, Heidelberg (1995)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Reactive Systems Group, Department of Computer Science, University of Kaiserslautern, P.O. Box 3049, 67653, Kaiserslautern, Germany

    Jens Brandt & Klaus Schneider

Authors
  1. Jens Brandt
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Klaus Schneider
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computer Science, The University of Manchester, M13 9PL, Manchester, United Kingdom

    Kung-Kiu Lau

  2. School of Computer Science, University of Manchester, M13 9PL, Manchester, UK

    Richard Banach

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Brandt, J., Schneider, K. (2005). Using Three-Valued Logic to Specify and Verify Algorithms of Computational Geometry. In: Lau, KK., Banach, R. (eds) Formal Methods and Software Engineering. ICFEM 2005. Lecture Notes in Computer Science, vol 3785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11576280_28

Download citation

  • DOI: https://doi.org/10.1007/11576280_28

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-29797-0

  • Online ISBN: 978-3-540-32250-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation