constructing finite algebras with falcon
Data(s) |
1996
|
---|---|
Resumo |
The generation of models and counterexamples is an important form of reasoning. In this paper, we give a formal account of a system, called FALCON, for constructing finite algebras from given equational axioms. The abstract algorithms, as well as some implementation details and sample applications, are presented. The generation of finite models is viewed as a constraint satisfaction problem, with ground instances of the axioms as constraints. One feature of the system is that it employs a very simple technique, called the least number heuristic, to eliminate isomorphic (partial) models, thus reducing the size of the search space. The correctness of the heuristic is proved. Some experimental data are given to show the performance and applications of the system. |
Identificador | |
Idioma(s) |
英语 |
Fonte |
Zhang Jian.constructing finite algebras with falcon,Journal of Automated Reasoning,1996,17(1):1-22 |
Palavras-Chave | #model generation #finite algebras #constraint satisfaction #least number heuristic |
Tipo |
期刊论文 |