A cognitive model of axiom formulation and reformulation with application to AI and software engineering

数学和科学理论建立在基础之上，而这些基础是为了创造一种工作范式而假定的。这些基础有时会发生变化。我们想调查基础从哪里来，它们是如何变化的，以及人工智能研究人员如何利用这些想法来创建更灵活的系统。例如，欧几里得提出了被认为描述物理世界的几何公理。这些是欧几里德几何中的概念、定理和证明所依据的基础。欧几里德几何后来被修改，摒弃了平行公设，形成了非欧几里德测角学，以及新的概念和定理。公理变化的另一个例子是希尔伯特对几何学的形式化：最初，他的公理包含隐藏的假设，这些假设很快就被发现并显化。弗雷格数论公理化中的悖论导致泽梅洛和弗伦克尔修改了他的一些公理，以防止问题集的构造。在一个不那么有名但同样值得注意的水平上，孩子们能够制定关于他们所处环境的数学规则，如传递性或算术的交换性，并在必要时修改这些规则。Lakoff和Nunez最近在认知科学方面的工作以及Lakatos在数学哲学方面的工作提出了可以做到这一点的方法。我们打算构建和评估这个过程的计算理论和模型，并探索我们的模型在人工智能和软件工程中的应用。这是一个雄心勃勃的项目，有可能汇集并深刻影响不同的领域，包括认知科学、自动数学推理、情境具体化代理以及人工智能问题解决和软件工程领域，这些领域将受益于更灵活的方法。开发一套自动化技术，能够将一个问题转化为不同的、更有趣的问题，可能会对这些领域产生巨大影响。特别是，我们的目标是探索我们的理论和模型在人工智能问题重写和软件规范需求中的应用。关于如何制定和重新制定约束、规范或目标的一般理论可能会导致一套通用的强大的人工智能新技术。

Mathematical and scientific theories rest on foundations which areassumed in order to create a paradigm within which to work. Thesefoundations sometimes shift. We want to investigate where foundationscome from, how they change, and how AI researchers can use these ideasto create more flexible systems. For instance, Euclid formulatedgeometric axioms which were thought to describe the physicalworld. These were the foundations on which concepts, theorems andproofs in Euclidean geometry rested. Euclidean geometry was latermodified by rejecting the parallel postulate, and non-Euclideangeometries were formed, along with new sets of concepts andtheorems. Another example of axiomatic change is in Hilbert'sformalisation of geometry: initially his axioms contained hiddenassumptions which were soon discovered and made explicit. Paradoxesfound in Frege's axiomatisation of number theory led to Zermelo andFraenkel modifying some of his axioms in order to prevent problem setsfrom being constructed. On a less celebrated, but equally remarkable,level children are able to formulate mathematical rules about theirenvironment such as transitivity or the commutativity of arithmetic,and to modify these rules if necessary. Recent work in cognitivescience by Lakoff and Nunez and in the philosophy of mathematics byLakatos suggests ways in which this may be done. We intend toconstruct and evaluate a computational theory and model of thisprocess and to explore the application of our model to AI and softwareengineering. This is an ambitious project, with the potential tobring together and deeply influence diverse fields including cognitivescience, automated mathematical reasoning, situated embodied agents,and AI problem solving and software engineering domains which wouldbenefit from a more flexible approach. Developing a set of automatedtechniques which are able to take a problem and change it into adifferent, more interesting problem could have great impact on thesedomains. In particular, we aim to explore the application of ourtheory and model to AI problem reformulation and softwarespecifications requirements. A general theory of how constraints,specifications or goals can be formulated and reformulated could leadto a communal set of powerful new AI techniques.