A Resolution Calculus with Shared Literals

• Autorzy: Peltier N.
• Języki publikacji: EN

Abstrakty

EN

We present a resolution calculus for first-order logic using a more concise formalism for representing sets of clauses. The idea is to represent the clause set at hand as a Directed Acyclic Graph, which allows one to share common literals instead of duplicating them, thus yielding a much more compact representation of the search space. We define inference rules operating on this language and we prove their soundness and refutational completeness. We also design simplification rules for pruning the search space. Finally we compare our technique with the usual resolution calculus and we prove (using the pigeonhole example) that our method can reduce the length of the proof by an exponential factor (in propositional logic).

Słowa kluczowe

EN

resolution; sharing; pigeonhole problem

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 76, nr 4
• Strony: 449--480
• Opis fizyczny: bibliogr. 20 poz.

Twórcy

autor

Peltier N.

• CNRS-Leibniz-IMAG Laboratory, 46 avenue Felix Viallet, 38031 Grenoble Cedex, France,

Bibliografia

• [1] Baader, F., Snyder, W.: Unification Theory, in: Handbook of Automated Reasoning (A. Robinson, A. Voronkov, Eds.), vol. I, chapter 8, Elsevier Science, 2001, 445-532.
• [2] Baaz,M., Leitsch, A.: Complexity of resolution proofs and function introduction, Annals of Pure and Applied Logic, 20, 1992, 181-215.
• [3] Barendregt, H., van Eekelen, M., Glauert, J., Kenneway, R., Plasmeijer, M. J., Sleep, M.: Term Graph Rewriting, PARLE'87, Springer, LNCS 259, 1987, 141-158.
• [4] Ben-Sasson, E., Galesi, N.: Space Complexity of Random Formulae in Resolution, Colloquium on Computational Complexity, 2001.
• [5] Boyer, R. S., Moore, J. S.: The Sharing of Structure in Theorem Proving Programs, in: Machine Intelligence 7 (B. Meltzer, D. Michie, Eds.), Edinburgh University Press, 1972, 101-116.
• [6] Chatalic, P., Simon, L.: Multiresolution for sat checking, Journal of Artificial Intelligence Tools, 10(4), 2001.
• [7] Cook, S., Reckhow, R.: The Relative Efficience of Propositional Proof Systems, The Journal of Symbolic Logic, 44(1), 1979, 36-50.
• [8] Davis, M., Putnam, H.: A Computing Procedure for Quantification Theory, Journal of the ACM, 7(3), July 1960, 201-215.
• [9] Eder, E.: Relative Complexities of First-Order Logic Calculi, Vieweg, 1990.
• [10] Egly, U.: On different concepts of function introduction, Computational Logic and Proof Theory, KGC 93, Springer, LNCS 713, 1993, 172-183.
• [11] Fitting, M.: First-Order Logic and Automated Theorem Proving, Texts and Monographs in Computer Science, Springer-Verlag, 1990.
• [12] Haken, A.: The Intractability of Resolution, Theoretical Computer Science, 39, 1985, 297-308.
• [13] Leitsch, A.: The resolution calculus, Springer. Texts in Theoretical Computer Science, 1997.
• [14] Lynch, C.: Paramodulation without Duplication, Proceedings of the Tenth Annual IEEE Symp. on Logic in Computer Science, LICS (D. Kozen, Ed.), IEEE Computer Society Press, June 1995, 167-177.
• [15] Meinel, C., Theobald, T.: Algorithms and Data Structures in VLSI Design: OBDD - Foundations and Application, Springer, 1998.
• [16] Motter, D. B., Markov, I. L.: A Compressed Breadth-First Search for Satisfiability, ALENEX, 2002, 29-42.
• [17] Peltier, N.: A Resolution Calculus for Shortening Proofs, Logic Journal of the Interest Group in Pure and Applied Logics, 13, 2005, 307-333.
• [18] Robinson, J. A.: A machine-oriented logic based on the resolution principle, J. Assoc. Comput. Mach., 12, 1965, 23-41.
• [19] Statman, R.: Lower Bounds on Herbrand's Theorem, Proc. AMS 75, 1979, 104-107.
• [20] Tseitin, G. S.: On the Complexity of Derivation in Propositional Calculus, in: Studies in Constructive Mathematics and Mathematical Logics (A. Slisenko, Ed.), 1968.