Proof of transitive closure property of directed acyclic graphs
| Autor: | Fares Fraij, Steve Roach |
|---|---|
| Rok vydání: | 2009 |
| Předmět: |
Property (philosophy)
Computer science String (computer science) Transitive closure ACL2 Directed acyclic graph Transitive reduction Graph Combinatorics TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Algorithm computer MathematicsofComputing_DISCRETEMATHEMATICS computer.programming_language |
| Zdroj: | Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications. |
| DOI: | 10.1145/1637837.1637849 |
| Popis: | This paper presents a formal correctness proof for some properties of restricted finite directed acyclic graphs (DAGs). A restricted graph has a single root and arbitrary siblings. The siblings are assigned integers, string values, or restricted DAGs. Leafs must be assigned string values. The main property is the transitive closure. Our restricted graphs and the properties are formalized in ACL2, and an ACL2 book has been prepared for reuse. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|