A graphical language for proof strategies

Gudmund Grov, Aleks Kissinger, Yuhui Lin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

13 Citations (Scopus)

Abstract

Complex automated proof strategies are often difficult to extract, visualise, modify, and debug. Traditional tactic languages, often based on stack-based goal propagation, make it easy to write proofs that obscure the flow of goals between tactics and are fragile to minor changes in input, proof structure or changes to tactics themselves. Here, we address this by introducing a graphical language called PSGraph for writing proof strategies. Strategies are constructed visually by "wiring together" collections of tactics and evaluated by propagating goal nodes through the diagram via graph rewriting. Tactic nodes can have many output wires, and use a filtering procedure based on goal-types (predicates describing the features of a goal) to decide where best to send newly-generated sub-goals. In addition to making the flow of goal information explicit, the graphical language can fulfil the role of many tacticals using visual idioms like branching, merging, and feedback loops. We argue that this language enables development of more robust proof strategies and provide several examples, along with a prototype implementation in Isabelle.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages324-339
Number of pages16
Volume8312 LNCS
DOIs
Publication statusPublished - 1 Dec 2013
Event19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - Stellenbosch, United Kingdom
Duration: 14 Dec 201319 Dec 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8312 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

Conference19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning
Abbreviated titleLPAR 2013
Country/TerritoryUnited Kingdom
CityStellenbosch
Period14/12/1319/12/13

ASJC Scopus subject areas

  • General Computer Science
  • Theoretical Computer Science

Fingerprint

Dive into the research topics of 'A graphical language for proof strategies'. Together they form a unique fingerprint.

Cite this