Discovery - University of Dundee - Online Publications

Library & Learning Centre

Automating change of representation for proofs in discrete mathematics

Automating change of representation for proofs in discrete mathematics

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

View graph of relations

Authors

  • Daniel Raggi (Lead / Corresponding author)
  • Alan Bundy
  • Gudmund Grov
  • Alison Pease

Research units

Info

Original languageEnglish
Title of host publicationIntelligent Computer Mathematics
Subtitle of host publicationInternational Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015 Proceedings
EditorsManfred Kerber, Jacques Carette, Cezary Kaliszyk, Florain Rabe, Volker Sorge
PublisherSpringer
Pages227-242
Number of pages16
VolumeLNAI 9150
ISBN (Electronic)978-3-319-20615-8
ISBN (Print)978-3-319-20614-1
DOIs
StatePublished - 23 Jun 2015
EventConference on Intelligent Computer Mathematics - Washington, DC, United States

Publication series

NameLecture Notes In Computer Science
PublisherSpringer
Volume9150
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceConference on Intelligent Computer Mathematics
Abbreviated titleCICM 2015
CountryUnited States
CityWashington, DC
Period13/07/1517/07/15
Internet address

Abstract

Representation determines how we can reason about a specific problem. Sometimes one representation helps us find a proof more easily than others. Most current automated reasoning tools focus on reasoning within one representation. There is, therefore, a need for the development of better tools to mechanise and automate formal and logically sound changes of representation.
In this paper we look at examples of representational transformations in discrete mathematics, and show how we have used Isabelle’s Transfer tool to automate the use of these transformations in proofs. We give a brief overview of a general theory of transformations that we consider appropriate for thinking about the matter, and we explain how it relates to the Transfer package. We show our progress towards developing a general tactic that incorporates the automatic search for representation within the proving process.

Documents

Library & Learning Centre

Contact | Accessibility | Policy