Interactive Proof Critics

Andrew Ireland, Michael Jackson, Gordon Reid

Research output: Contribution to journalArticlepeer-review

12 Citations (Scopus)


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
Issue number3
Publication statusPublished - 1999


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


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

Cite this