Polar: A Framework for Proof Refactoring

Dominik Dietrich; Iain Whiteside; David Aspinall

doi:10.1007/978-3-642-45221-5_52

Polar: A Framework for Proof Refactoring

Dominik Dietrich, Iain Whiteside, David Aspinall

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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.

Original language	English
Title of host publication	Logic for Programming, Artificial Intelligence, and Reasoning
Editors	Ken McMillan, Aart Middeldorp, Andrei Voronkov
Publisher	Springer
Pages	776-791
Number of pages	16
Volume	8312
ISBN (Electronic)	978-3-642-45221-5
ISBN (Print)	978-3-642-45220-8
DOIs	https://doi.org/10.1007/978-3-642-45221-5_52
Publication status	Published - 2013
Event	19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2013 - Stellenbosch, United Kingdom Duration: 14 Dec 2013 → 19 Dec 2013

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin Heidelberg
Volume	8312

Conference

Conference	19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2013
Country/Territory	United Kingdom
City	Stellenbosch
Period	14/12/13 → 19/12/13

Access to Document

10.1007/978-3-642-45221-5_52

Cite this

@inproceedings{e33b7ef96fd54f19bd20ae1c9f79369e,

title = "Polar: A Framework for Proof Refactoring",

abstract = "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.",

author = "Dominik Dietrich and Iain Whiteside and David Aspinall",

year = "2013",

doi = "10.1007/978-3-642-45221-5_52",

language = "English",

isbn = "978-3-642-45220-8",

volume = "8312",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "776--791",

editor = "Ken McMillan and Aart Middeldorp and Andrei Voronkov",

booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning",

address = "United Kingdom",

note = "19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2013 ; Conference date: 14-12-2013 Through 19-12-2013",

}

Dietrich, D, Whiteside, I & Aspinall, D 2013, Polar: A Framework for Proof Refactoring. in K McMillan, A Middeldorp & A Voronkov (eds), Logic for Programming, Artificial Intelligence, and Reasoning. vol. 8312, Lecture Notes in Computer Science, vol. 8312, Springer, pp. 776-791, 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2013, Stellenbosch, United Kingdom, 14/12/13. https://doi.org/10.1007/978-3-642-45221-5_52

Polar: A Framework for Proof Refactoring. / Dietrich, Dominik; Whiteside, Iain; Aspinall, David.
Logic for Programming, Artificial Intelligence, and Reasoning. ed. / Ken McMillan; Aart Middeldorp; Andrei Voronkov. Vol. 8312 Springer, 2013. p. 776-791 (Lecture Notes in Computer Science; Vol. 8312).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Polar: A Framework for Proof Refactoring

AU - Dietrich, Dominik

AU - Whiteside, Iain

AU - Aspinall, David

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84893948058&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-45221-5_52

DO - 10.1007/978-3-642-45221-5_52

M3 - Conference contribution

SN - 978-3-642-45220-8

VL - 8312

T3 - Lecture Notes in Computer Science

SP - 776

EP - 791

BT - Logic for Programming, Artificial Intelligence, and Reasoning

A2 - McMillan, Ken

A2 - Middeldorp, Aart

A2 - Voronkov, Andrei

PB - Springer

T2 - 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2013

Y2 - 14 December 2013 through 19 December 2013

ER -

Polar: A Framework for Proof Refactoring

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this