Reasoned modelling critics: Turning failed proofs into modelling guidance

Andrew Ireland, Gudmund Grov, Maria Teresa Llano Rodriguez, Michael Butler

Research output: Contribution to journalArticlepeer-review


The activities of formal modelling and reasoning are closely related. But while the rigour of building formal models brings significant benefits, formal reasoning remains a major barrier to the wider acceptance of formalism within design. Here we propose reasoned modelling critics - an approach which aims to abstract away from the complexities of low-level proof obligations, and provide high-level modelling guidance to designers when proofs fail. Inspired by proof planning critics, the technique combines proof-failure analysis with modelling heuristics. Here, we present the details of our proposal, implement them in a prototype and outline future plans. © 2011 Elsevier B.V. All rights reserved.

Original languageEnglish
Pages (from-to)293-309
JournalScience of Computer Programming
Issue number3
Publication statusPublished - 25 Apr 2011


  • Artificial intelligence
  • Automated reasoning
  • Formal methods
  • Formal modelling
  • Formal verification
  • Reasoned modelling


Dive into the research topics of 'Reasoned modelling critics: Turning failed proofs into modelling guidance'. Together they form a unique fingerprint.

Cite this