Reasoned modelling critics: Turning failed proofs into modelling guidance

Andrew Ireland; Gudmund Grov; Maria Teresa Llano; Michael Butler

doi:10.1016/j.scico.2011.03.006

Reasoned modelling critics: Turning failed proofs into modelling guidance

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

School of Informatics

Research output: Contribution to journal › Article › peer-review

Abstract

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.

Original language	English
Pages (from-to)	293-309
Number of pages	17
Journal	Science of Computer Programming
Volume	78
Issue number	3
DOIs	https://doi.org/10.1016/j.scico.2011.03.006
Publication status	Published - 2013

Access to Document

10.1016/j.scico.2011.03.006

http://www.sciencedirect.com/science/article/pii/S016764231100092X

Integration and Interaction of multiple mathematical reasoning processes
Bundy, A. (Principal Investigator), Colton, S. (Sponsor), Aspinall, D. (Co-Investigator (External)), Dennis, L. (Co-Investigator (External)), Fleuriot, J. (Co-Investigator (External)), Georgieva, L. (Co-Investigator (External)), Ireland, A. (Co-Investigator (External)), Jackson, P. (Co-Investigator (External)) & Smaill, A. (Co-Investigator (External))
EPSRC
1/04/07 → 31/03/11
Project: Research

Cite this

@article{25668d02f3bd42e1a99253ff55763dd0,

title = "Reasoned modelling critics: Turning failed proofs into modelling guidance",

abstract = "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.",

author = "Andrew Ireland and Gudmund Grov and Llano, \{Maria Teresa\} and Michael Butler",

note = "Abstract State Machines, Alloy, B and Z - Selected Papers from ABZ 2010",

year = "2013",

doi = "10.1016/j.scico.2011.03.006",

language = "English",

volume = "78",

pages = "293--309",

journal = "Science of Computer Programming",

issn = "0167-6423",

publisher = "Elsevier",

number = "3",

}

TY - JOUR

T1 - Reasoned modelling critics: Turning failed proofs into modelling guidance

AU - Ireland, Andrew

AU - Grov, Gudmund

AU - Llano, Maria Teresa

AU - Butler, Michael

N1 - Abstract State Machines, Alloy, B and Z - Selected Papers from ABZ 2010

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

U2 - 10.1016/j.scico.2011.03.006

DO - 10.1016/j.scico.2011.03.006

M3 - Article

SN - 0167-6423

VL - 78

SP - 293

EP - 309

JO - Science of Computer Programming

JF - Science of Computer Programming

IS - 3

ER -

Reasoned modelling critics: Turning failed proofs into modelling guidance

Abstract

Access to Document

Fingerprint

Projects

Integration and Interaction of multiple mathematical reasoning processes

Cite this