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

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

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. It is astonishing that humansare able to form mathematical concepts, to abstract mathematicalrules, to explore the space that these rules define, and to modify therules in the face of counterexamples or other problems. Recent workin cognitive science by Lakoff and Nunez and in the philosophy ofmathematics by Lakatos suggests ways in which this may be done. Weintend to construct and evaluate a computational theory and model ofthis process and to explore the application of our model to AI andsoftware engineering. This is an ambitious project, with thepotential to bring together and deeply influence diverse fieldsincluding cognitive science, automated mathematical reasoning,situated embodied agents, and AI problem solving 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 constraint satisfaction problems 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