System description – generating models by SEM. (English) Zbl 1412.68268
McRobbie, M. A. (ed.) et al., Automated deduction – CADE-13. 13th international conference on automated deduction, New Brunswick, NJ, USA, July/August 1996. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1104, 308-312 (1996).
For the entire collection see [Zbl 1102.68317].
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03C13 | Model theory of finite structures |
References:
| [1] | Fujita, M., Slaney, J., and Bennett, F.; “Automatic generation of some results in finite algebra,” Proc. IJCAI-93, 52-57, Chambéry, France. |
| [2] | Jech, T., “OTTER experiments in a system of combinatory logic,” J. Automated Reasoning 14 (1995) 413-426. · Zbl 0822.03011 · doi:10.1007/BF00881715 |
| [3] | Kim, S., and Zhang, H., “ModGen: Theorem proving by model generation,” Proc. AAAI-94, 162-167, Seattle. |
| [4] | Kunen, K., “Single axioms for groups,” J. Automated Reasoning 9 (1992) 291-308. · Zbl 0794.20001 · doi:10.1007/BF00245293 |
| [5] | Manthey, R., and Bry, F., “SATCHMO: A theorem prover implemented in Prolog,” Proc. CADE-9 (1988) 415-434. · Zbl 0668.68104 |
| [6] | McCune, W., “A Davis-Putnam program and its application to finite first-order model search: Quasigroup existence problems,” Technical Report ANL/MCS-TM-194, Argonne National Laboratory (1994). |
| [7] | Slaney, J., “FINDER: Finite domain enumerator — system description,” Proc. CADE-12 (1994) 798-801. |
| [8] | Slaney, J., Fujita, M. and Stickel, M., “Automated reasoning and exhaustive search: Quasigroup existence problems,” Computers and Mathematics with Applications 29 (1995) 115-132. · Zbl 0827.20083 · doi:10.1016/0898-1221(94)00219-B |
| [9] | Zhang, H., and Stickel, M., “Implementing the Davis-Putnam algorithm by tries,” Technical Report, University of Iowa (1994). |
| [10] | Zhang, J., “Constructing finite algebras with FALCON,” accepted by J. Automated Reasoning. · Zbl 0877.68103 |
| [11] | Zhang, J. |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
