zbMATH — the first resource for mathematics

Polar: a framework for proof refactoring. (English) Zbl 1407.68434
McMillan, Ken (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14–19, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8312, 776-791 (2013).
Summary: We present a prototype refactoring framework based on graph rewriting and bidirectional transformations that is designed to be generic, extensible, and declarative. Our approach uses a language-independent graph meta-model to represent proof developments in a generic way. We use graph rewriting to enrich the meta-model with dependency information and to perform refactorings, which are written as declarative rewrite rules. Our framework, called Polar, is implemented in the GrGen rewriting engine.
For the entire collection see [Zbl 1277.68016].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q42 Grammars and rewriting systems
GrGen; Polar
Full Text: DOI