A reflection−based proof tactic for lattices in Coq
This paper presents a new proof tactic that decides equalities and inequalities between terms over lattices. It uses a decision procedure that is a variation on Whitman’s algorithm and is implemented using a technique known as proof by reflection. We will paint the essence of the approach in broad...
| Հիմնական հեղինակներ: | , |
|---|---|
| Այլ հեղինակներ: | |
| Ձևաչափ: | Գիրք |
| Հրապարակվել է: |
2009
|