Keywords:-
Article Content:-
Abstract
In this paper, we present an experiment of complex effects of LRPO on the proof complexity in term orderings on algebraic structures. In experiment, we yield 10! lex patterns that are derived from the symbols that make up Boolean rings (+, −,×, #,∧, 0, 1, a, b, c). Also, the given clause algorithm is used to measure the proof complexity by counting the number of clauses generated. Curiously, the experimental results showed that the distribution the proof complexity was not unimodal, but bimodal. We discuss three possible reasons of bimodality of proof complexity in algebraic structures.
References:-
References
McCune, W.: 1994b, Otter 3.0 Reference Manual and Guide, Technical Report ANL-94/6 Technical report, Argonne National Laboratory, Argonne, Illinois.
William McCune, ”Experiments with Given-Clause Algorithm in Otter,”Journal of Automated Reasoning (JAR), March 1997
Gerard Huet, Jean-Marie Hullot, ”Lexicographic Path Orderings and Applications to Term Rewriting Systems,” Journal of Symbolic Computation, June 1982
Garrett Birkhoff, ”Boolean Rings and Their Applications,” Transactions of the American Mathematical Society, April 1935
Cook, S. A. (1971). ”The complexity of theorem-proving procedures.” Proceedings of the third annual ACM symposium on Theory of computing, pp. 151?158.
Buss, S. R. (1998). Handbook of Proof Theory. North-Holland. Dershowitz, N. (1987). ”Termination of rewriting.” Journal of SymbolicComputation, 3(1-2), 69?116.
Jouannaud, J.-P., and Lescanne, P. (1982). ”On multiset orderings.” Information Processing Letters, 15(2), 57?63.
Dershowitz, N. (1987). ”Termination of rewriting.” Journal of Symbolic
Halmos, P. R. (1963). Boolean algebras. Springer.
Huntington, E. V. (1904). ”Sets of independent postulates for the algebra of logic.” Transactions of the American Mathematical Society, 5(3), 288-309.
McCune, W. (1994). OTTER 3.0 Reference Manual and Guide. Argonne National Laboratory
Sutcliffe, G., and Suttner, C. (1998). ”The CADE ATP System Competition.” Automated Deduction?CADE-14, pp. 128?143. Springer.
Mitzenmacher, M. (2004). ”A brief history of generative models for power law and lognormal distributions.” Internet Mathematics, 1(2), 226?251.
Baader, F., and Nipkow, T. (1998). Term Rewriting and All That.Cambridge University Press.