Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance

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 – a technique 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 and outline future plans.

• Type: Conference
• Year: 2010
• Where: ASM
• Authors: Andrew Ireland, Gudmund Grov, Michael Butler
• Keywords: ASM 2010, Formal Modelling, Formal Reasoning, Low-level Proof Obligations, Microbiology