Reasoned modelling critics: Turning failed proofs into modelling guidance
Reasoned modelling critics: Turning failed proofs into modelling guidance
复制标题
理性的建模批评家：将失败的证明转化为建模指导
DOI：
10.1016/j.scico.2011.03.006
复制
发表时间：
2013
影响因子：
1.3
通讯作者：
Ireland A
中科院分区：
文献类型：
--
作者：
Ireland A
形式建模和推理活动密切相关。但是，虽然构建形式模型的严格性带来了显着的好处，但形式推理仍然是设计中更广泛地接受形式主义的主要障碍。在这里，我们提出了合理的建模批评家——一种旨在抽象出低级证明义务的复杂性的方法，并在证明失败时为设计者提供高级建模指导。受到证明规划批评家的启发，该技术将证明失败分析与建模启发法相结合。在这里，我们展示了我们提案的细节，在原型中实施它们并概述了未来的计划。
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.
登录
查看更多内容
将拉卡托斯式推理应用于人工智能领域
影响因子：
--
作者：
A. Pease;A. Smaill;S. Colton;Andrew Ireland;M. T. Llano;R. Ramezani;G. Grov;M. Guhe
通讯作者：
M. Guhe
使用显式计划来指导归纳证明
DOI：
--
发表时间：
1988
期刊：
CADE
影响因子：
--
作者：
A. Bundy
通讯作者：
A. Bundy
Rippling - 数学推理的元级指导
DOI：
10.1017/cbo9780511543326
发表时间：
2005
期刊：
Theor. Comput. Sci.
影响因子：
--
作者：
A. Bundy;D. Basin;D. Hutter;Andrew Ireland
通讯作者：
Andrew Ireland
DOI：
10.1007/978-3-540-45085-6_22
发表时间：
2003-07
期刊：
--
影响因子：
--
作者：
L. Dixon;Jacques D. Fleuriot
通讯作者：
L. Dixon;Jacques D. Fleuriot
在形式化方法中使用设计模式：事件 B 方法
DOI：
--
发表时间：
2008
期刊：
International Colloquium on Theoretical Aspects of Computing
影响因子：
--
作者：
J. Abrial;Son Hoang
通讯作者：
Son Hoang