2000 character limit reached
A Conjecture for ATP Research
Published 15 Mar 2024 in cs.LO | (2403.10334v1)
Abstract: This note generalizes factorization for formulas with multiplicities and conjectures that the connection method along with this feature is computationally as powerful as resolution, also seen from a complexity point of view.
- W. Bibel. Automated Theorem Proving. Vieweg Verlag, Braunschweig, second edition, 1987. First ed. 1982.
- W. Bibel. Comparison of proof methods. In J. Otten and W. Bibel, editors, Proceedings of the 1st International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023), Prague, Czech Republic, September 18, 2023, volume 3613, pages 119–132. CEUR-WS.org, 2024. URN: urn:nbn:de:0074-3613-0.
- W. Bibel and E. Eder. Methods and calculi for deduction. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 1, chapter 3, pages 67–182. Oxford University Press, Oxford, 1993.
Paper Prompts
Sign up for free to create and run prompts on this paper using GPT-5.
Top Community Prompts
Collections
Sign up for free to add this paper to one or more collections.
