Academic Journal
Using Three-Valued Logic to Specify and Verify Algorithms Of Computational Geometry
| العنوان: | Using Three-Valued Logic to Specify and Verify Algorithms Of Computational Geometry |
|---|---|
| المؤلفون: | Jens Brandt, Klaus Schneider |
| المساهمون: | The Pennsylvania State University CiteSeerX Archives |
| المصدر: | http://rsg.informatik.uni-kl.de/publications/data/BrSc05.pdf. |
| سنة النشر: | 2005 |
| المجموعة: | CiteSeerX |
| الوصف: | 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. |
| نوع الوثيقة: | text |
| وصف الملف: | application/pdf |
| اللغة: | English |
| Relation: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.60.7220; http://rsg.informatik.uni-kl.de/publications/data/BrSc05.pdf |
| الاتاحة: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.60.7220 http://rsg.informatik.uni-kl.de/publications/data/BrSc05.pdf |
| Rights: | Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
| رقم الانضمام: | edsbas.E13A689F |
| قاعدة البيانات: | BASE |
| الوصف غير متاح. |