swMATH ID: 21349
Software Authors: Zhang, J.
Description: Constructing finite algebras with FALCON. 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.
Homepage: https://link.springer.com/article/10.1007/BF00247667
Related Software: Mace4; ModGen; SATCHMO; FINDER; MiniSat; SCOTT; AGES; Maude; Prover9; z3; Yices; sem; RRL; MGTP; E-Darvin; SATO; Darwin; OTTER; TPTP; nauty
Cited in: 7 Publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
Constructing finite algebras with FALCON. Zbl 0877.68103
Zhang, Jian

Citations by Year