Interactive Proof Critics

Andrew Ireland, Michael Jackson, Gordon Reid

Research output: Contribution to journalArticle

Abstract

The key to a successful proof often lies within the analysis of failed proof attempts. Motivated by this observation we have developed and evaluated an interface to an inductive theorem prover which supports a collaborative style of failure analysis. Our work builds upon an automatic proof patching mechanism and extends the capabilities of an existing theorem proving interface. Our approach is multi-disciplinary, we draw upon work from both the automated theorem proving and human computer interaction communities.

Original languageEnglish
Pages (from-to)302-325
Number of pages24
JournalFormal Aspects of Computing
Volume11
Issue number3
Publication statusPublished - 1999

Keywords

  • Inductive proof
  • Proof patching
  • Proof planning
  • Theorem proving
  • User interfaces

Fingerprint Dive into the research topics of 'Interactive Proof Critics'. Together they form a unique fingerprint.

  • Cite this

    Ireland, A., Jackson, M., & Reid, G. (1999). Interactive Proof Critics. Formal Aspects of Computing, 11(3), 302-325.