Abstract
In this paper, we present a resolution calculus extended by the notion of symmetries. A new deduction rule named symmetry extension is introduced. Combining resolution deduction and symmetry extension yields a new extended resolution deduction concept called SR-deduction (resolution deduction with symmetries). By extending the given clause set by a clause derived by symmetry extension, exponentially shorter refutations may be obtained than by applying resolution to the given clause set.
This research was supported by the Federal Ministry for Research and Technology within the project TASSO under grant no. ITW 8900 C2.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Baaz and A. Leitsch. Complexity of Resolution Proofs and Function Introduction. Annals of Pure and Applied Logic, 57:181–215, 1992.
B. Benhamou and L. Sais. Theoretical Study of Symmetries in Propositional Calculus and Applications. In D. Kapur, editor, Proceedings of the Conference on Automated Deduction, pages 281–294, Berlin, 1992. Lecture Notes in Artificial Intelligence, Springer.
W. Bibel. Automated Theorem Proving. Vieweg, Braunschweig, second edition, 1987.
W. Bibel. Short Proofs of the Pigeonhole Formulas Based on the Connection Method. Journal of Automated Reasoning, 6:287–297, 1990.
W. W. Bledsoe. Splitting and Reduction Heuristics in Automatic Theorem Proving. Artificial Intelligence, 2:57–78, 1971.
C. L. Chang and R. C. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York, 1973.
U. Egly. A Simple Proof for the Pigeonhole Formulae. In B. Neumann, editor, Proceedings of the European Conference on Artificial Intelligence, pages 70–1. John Wiley & Sons, 1992.
U. Egly. Shortening Proofs by Quantifier Introduction. In A. Voronkov, editor, Proceedings of the International Conference on Logic Programming and Automated Reasoning, pages 148–159. Springer Verlag, 1992.
T. W. Hungerford. Algebra. Springer Verlag, 1974.
B. Krishnamurthy. Short Proofs for Tricky Formulas. Acta Informatica, 22(3):253–275, Aug. 1985.
A. Leitsch. On Different Concepts of Resolution. Zeitschrift f. math. Logik und Grundlagen d. Mathematik, 35:71–77, 1989.
D. W. Loveland. Automated Theorem Proving: A Logical Basis, volume 6 of Fundamental Studies in Computer Science. North-Holland Publishing Company, Amsterdem, New York, Oxford, 1978.
N. V. Murray and E. Rosenthal. Short Proofs of the Pigeonhole Formulas Using Path Dissolution. Technical report, Dept. of Computer Science, State Univ. of N.Y. at Albany, Albany N.Y. 12222, 1988.
U. Schöning. Graph Isomorphism is in the Low Hierarchy. In STACS, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Egly, U. (1993). A first order resolution calculus with symmetries. In: Voronkov, A. (eds) Logic Programming and Automated Reasoning. LPAR 1993. Lecture Notes in Computer Science, vol 698. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56944-8_46
Download citation
DOI: https://doi.org/10.1007/3-540-56944-8_46
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56944-2
Online ISBN: 978-3-540-47830-0
eBook Packages: Springer Book Archive