Matings in matrices

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Matings in matrices

Full text

Pdf (753 KB)

Source

Communications of the ACM archive
Volume 26 , Issue 11 (November 1983) table of contents

Pages: 844 - 852

Year of Publication: 1983

ISSN:0001-0782

Author

Wolfgang Bibel

Technische Univ. Munchen, Munich, West Germany

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 10, Downloads (12 Months): 21, Citation Count: 6

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/182.183 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Peter B. Andrews, Theorem Proving via General Matings, Journal of the ACM (JACM), v.28 n.2, p.193-214, April 1981 [doi>10.1145/322248.322249]
	2	Peter B. Andrews, Transforming Matings into Natural Deduction Proofs, Proceedings of the 5th Conference on Automated Deduction, p.281-292, July 08-11, 1980
	3	Wolfgang Bibel, On Matrices with Connections, Journal of the ACM (JACM), v.28 n.4, p.633-645, Oct. 1981 [doi>10.1145/322276.322277]
	4	Bibel, W. A comparative study of several proof procedures. Artif. Intell. 18, (1982), 269-293.
	5	Bibel, W. The complete theoretical basis for the systematic proof method. Bericht ATP-6-XII-80, Institut ffir lnformatik, TUM (1980). Submitted to J. ACM.
	6	BibeL W. Computationally improved versions of Herbrand's theorem. In Stern, ed. Proc. of the Herbrand Colloquium, North Holland, Amsterdam, 1982), 11-28.
	7	Bibel, W. Automated theorem proving. Vieweg: Braunschweig, 1982.
	8	Bibel, W. Syntax-directed, semantics-supported program synthesis. Artif. Intell. 14, (1980), 243-261.
	9	Proceedings of the 5th Conference on Automated Deduction, July 1980
	10	Bledsoe, W.W. Non-resolution theorem proving. Artif. Intell 9, (1977), 1-35.
	11	Chin-Liang Chang , Richard C. Lee , Richard Char-Tung Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, Inc., Orlando, FL, 1997
	12	Gentzen, G. Untersuchunge fiber dos logische Schlieben I, Mathemat. Zeitschrift 39, (1935), 176-210.
	13	Herbrand, J. Recherches sur la Theorie de la Demonstration, Traveaux de la Societ6 des Sciences et des Lettres de Varsovie, Classe III sciences mathematiques et physiques, 33 (1930).
	14	Joyner, W., (ed.) 4th Workshop on Automated Deduction (Austin, Texas, 1979).
	15	Kalish, D., and Montague, R. Logic. New York: Harcourt Brace Jovanovich, 1964.
	16	Loveland, D.W. Automated theorem proving. Amsterdam: North Holland, 1978.
	17	Proceedings of the 6th Conference on Automated Deduction, June 1982
	18	N. J. Nilsson, Principles of artificial intelligence, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1980
	19	Robinson, J.A. Logic: form and function, Edinburgh University Press (1979).
	20	Siekmann, J. (ed.) GWAI-81, Informatik Fachberichte 47. Berlin: Springer, 1981.
	21	Larry Wos, Solving Open Questions with an Automated Theorem-Proving Program, Proceedings of the 6th Conference on Automated Deduction, p.1-31, June 07-09, 1982

CITED BY 7

	Neil V. Murray , Erik Rosenthal, Dissolution: making paths vanish, Journal of the ACM (JACM), v.40 n.3, p.504-535, July 1993
	W. Bibel , E. Eder, Decomposition of tautologies into regular formulas and strong completeness of connection-graph resolution, Journal of the ACM (JACM), v.44 n.2, p.320-344, March 1997
	Jens Otten , Wolfgang Bibel, leanCoP: lean connection-based theorem proving, Journal of Symbolic Computation, v.36 n.1-2, p.139-161, July 2003
	Zohar Manna , Richard Waldinger, Fundamentals of Deductive Program Synthesis, IEEE Transactions on Software Engineering, v.18 n.8, p.674-704, August 1992
	K. Hörwein, Structuring Resolution Proofs by Introducing New Lemmata, Journal of Automated Reasoning, v.19 n.2, p.173-203, October 1997
	Wolfgang Schonfeld, Prolog extensions based on tableau calculus, Proceedings of the 9th international joint conference on Artificial intelligence, p.730-732, August 18-23, 1985, Los Angeles, California
	Franz Guenthner , Hubert Lehmann , Wolfgang Schönfeld, A theory for the representation of knowledge, IBM Journal of Research and Development, v.30 n.1, p.39-56, Jan. 1986