Constructing finite algebras with FALCON

1. Bourely, C., Caferra, R., and Peltier, N.: A method for building models automatically: Experiments with an extension of OTTER, in Proc. 12th Int. Conf. on Automated Deduction (CADE-12), LNAI 814, Springer, 1994, pp. 72–86.

2. BurrisS. and LeeS.: Tarski's high school identities, Amer. Math. Monthly 100, (1993), 231–236.

   Google Scholar 

3. DavisM. and PutnamH.: A computing procedure for quantification theory, J. ACM 7 (1960), 201–215.

   Google Scholar 

4. Fujita, M., Slaney, J., and Bennett, F.: Automatic generation of some results in finite algebra, in Proc. 13th Int. Joint Conf. on Artificial Intelligence (IJCAI-93), 1993, pp. 52–57.

5. Hasegawa, R., et al.: MGTP: A parallel theorem prover based on lazy model generation, in Proc. 11th Int. Conf. on Automated Deduction (CADE-11), LNAI 607, Springer, 1992, pp. 776–780.

6. Kim. S. and Zhang, H.: ModGen: Theorem proving by model generation, in Proc. AAAI-94, Seattle, 1994, pp. 162–167.

7. LeeS.-J. and PlaistedD. A.: Problem solving by searching for models with a theorem prover, Artificial Intelligence 69 (1994), 205–233.

   Google Scholar 

8. MacHaleD.: A remark on Boolean rings, Mathematics Magazine 63 (1990), 248–249.

   Google Scholar 

9. McCuneW.: A Davis-Putnam Program and Its Application to Finite First-Order Model Search: Quasigroup Existence Problems, Tech. Memo ANL/MCS-TM-194, Argonne National Laboratory, Argonne, IL, 1994.

   Google Scholar 

10. Romanowska, A. B.: Private Communication, 1994.

11. RomanowskaA. B. and SmithJ. D. H.: Modal Theory: An Algebraic Approach to Order, Geometry, and Convexity, Heldermann Verlag, Berlin, 1985.

    Google Scholar 

12. Slaney, J.: FINDER: Finite Domain Enumerator. Version 3.0 Notes and Guide, Australian National University, 1993.

13. Slaney, J.: SCOTT: A model-guided theorem prover, in Proc. 13th Int. Joint Conf. on Artificial Intelligence (IJCAI-93), 1993, pp. 109–114.

14. SlaneyJ., FujitaM. and StickelM.: Automated reasoning and exhaustive search: Quasigroup existence problems, Computers and Mathematics with Applications 29(2) (1995), 115–132.

    Google Scholar 

15. Smith, J. D. H.: Private Communication, 1994.

16. Tammet, T.: Using resolution for deciding solvable classes and building finite models, Baltic Computer Science: Selected Papers, LNCS 502, Springer (1991), 33–64.

17. WinkerS.: Generation and verification of finite models and counterexamples using an automated theorem prover answering two open questions, J. ACM 29 (1982), 273–284.

    Google Scholar 

18. WosL.: The kernel strategy and its use for the study of combinatory logic, J. Automated Reasoning 10 (1993), 287–343.

    Google Scholar 

19. WosL.: Automated Reasoning: 33 Basic Research Problems, Prentice Hall, Englewood Cliffs, NJ, 1988.

    Google Scholar 

20. Zhang, H., and Stickel, M.: Implementing the Davis-Putnam Algorithm by Tries, Technical Report, University of Iowa, 1994.

21. Zhang, J.: Search for models of equational theories, in Proc. 3rd Int. Conf. for Young Computer Scientists (ICYCS-93), Beijing, 1993, pp. 2.60–63.

22. Zhang, J.: Problems on the generation of finite models, in Proc. 12th Int. Conf. on Automated Deduction (CADE-12), LNAI 814, Springer, 1994, pp. 753–757.

Download references