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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Brandt, J., & Schneider, K. (2005). Using three-valued logic to specify and verify algorithms of computational geometry. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3785 LNCS, pp. 405–420). Springer Verlag. https://doi.org/10.1007/11576280_28
Mendeley helps you to discover research relevant for your work.