Abstract
An enumerative approach to conjecture formulation is presented. Its basic steps include the generation of terms and formulas, and testing the formulas in a set of models. The main procedure and some experimental results are described.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Russell, S. and Norvig, P., Artificial Intelligence: A Modern Approach, Prentice Hall, Englewood Cliffs, New Jersey, USA, 1995.
Schumann, J.M.Ph., “DELTA-A bottom-up preprocessor for top-down theorem provers,” Proc. CADE-12, 774–777, 1994.
Slaney, J. et al. “Automated reasoning and exhaustive search: Quasigroup existence problems,” Computers and Math. with Applications 29(2): 115–132, 1995.
Wos, L., Automated Reasoning: 33 Basic Research Problems, Prentice Hall, Englewood Cliffs, New Jersey, USA, 1988.
Zhang, J., The Generation and Applications of Finite Models, PhD thesis, Institute of Software, Chinese Academy of Sciences, Beijing, China, 1994.
Zhang, J., “Constructing finite algebras with FALCON,” J. Automated Reasoning 17(1): 1–22, 1996.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhang, J. (1999). System Description: MCS: Model-Based Conjecture Searching. In: Automated Deduction — CADE-16. CADE 1999. Lecture Notes in Computer Science(), vol 1632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48660-7_37
Download citation
DOI: https://doi.org/10.1007/3-540-48660-7_37
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66222-8
Online ISBN: 978-3-540-48660-2
eBook Packages: Springer Book Archive