Dissolution

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Dissolution: making paths vanish

Full text

Pdf (1.98 MB)

Source

Journal of the ACM (JACM) archive
Volume 40 , Issue 3 (July 1993) table of contents

Pages: 504 - 535

Year of Publication: 1993

ISSN:0004-5411

Authors

Neil V. Murray	State University of New York at Albany, Albany, New York
Erik Rosenthal	University of New Haven, West Haven, Connecticut

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 37, Citation Count: 4

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/174130.174135 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	~BIBEL, W. Tautology testing with a generalized matrix reduction method. Theoret. Comput. ~Sci. 8 (1979), 31-44.
	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. Int. 18, 3 (1982), ~269 293.
	5	Wolfgang Bibel, Matings in matrices, Communications of the ACM, v.26 n.11, p.844-852, Nov. 1983 [doi>10.1145/182.183]
	6	Seth Chaiken , Neil V. Murray , Erik Rosenthal, An application of P4-free graphs in theorem-proving, Proceedings of the third international conference on Combinatorial mathematics, p.106-121, September 1989, New York City, New York, United States
	7	Stephen Cook , Robert Reckhow, On the lengths of proofs in the propositional calculus (Preliminary Version), Proceedings of the sixth annual ACM symposium on Theory of computing, p.135-148, April 30-May 02, 1974, Seattle, Washington, United States [doi>10.1145/800119.803893]
	8	Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
	9	N Eisinger, What you always wanted to know about clause graph resolution, Proc. of the 8th international conference on Automated deduction, p.316-336, August 1986, Oxford, United Kingdom
	10	Melvin Fitting , David Gries, First-order logic and automated theorem proving, Springer-Verlag New York, Inc., New York, NY, 1990
	11	~LAWRENCE, J., AND STARKEY, J. Experimental tests of resolution-based theorem proving ~strategies. CS-74-011. Computer Sci. Dept., Washington State Univ., Seattle, Wash., Apr. ~1974.
	12	~MCCUNE, W. Otter 1.0 user's guide. Technical Report ANL-88/44. Argonne National ~Laboratory, Argonne, IlL 1988.
	13	~MURRAY, N. V. Completely non-clausal theorem proving. Artlf. Int. 18, 1 (Jan. 1982), ~67 85.
	14	Neil V. Murray , Erik Rosenthal, Inference with path resolution and semantic graphs, Journal of the ACM (JACM), v.34 n.2, p.225-254, April 1987 [doi>10.1145/23005.23716]
	15	N. V. Murray , E. Rosenthal, Inferencing on an arbitrary set of links, Proceeding of the Second International Symposium on Methodologies for intelligent systems, p.416-423, December 1987, Charlotte, North Carolina, United States
	16	~MURRAY, N. V., AND ROSENTHAL, E. Path dissolution: A strongly complete rule of inference. ~In Proceedings of tile 6th National Conference on Artificial Intelligence (Seattle, Wash., July ~12-17). Morgan-Kaufmann, San Mateo, Calif., 1987, pp. 161-166.
	17	Neil V. Murray , Erik Rosenthal, Theory links: applications to automated theorem proving, Journal of Symbolic Computation, v.4 n.2, p.173-190, Oct. 1987 [doi>10.1016/S0747-7171(87)80064-0]
	18	~MURRAY, N. V., AND ROSENTHAL, E. On the relative merits of path dissolution and the ~method of analytic tableaux. Tech. Rep. TR 90-5. SUNY at Albany, Albany, N.Y., 1990.
	19	N. V. Murray , E. Rosenthal, Reexamining intractability of tableau methods, Proceedings of the international symposium on Symbolic and algebraic computation, p.52-59, August 20-24, 1990, Tokyo, Japan [doi>10.1145/96877.96894]
	20	F. Oppacher , E. Suen, HARP: a tableau-based theorem prover, Journal of Automated Reasoning, v.4 n.1, p.69-100, March 1988
	21	~PRAWlTZ, D. A Proof Procedure with Matrix Reduction. In Lecture Notes in Mathematics, vol. ~125. Springer-Verlag, New York, 1970, pp. 207-213.
	22	~SMULLYAN, R.M. First-Order Logic. Springer-Verlag, New York, 1968.
	23	M E Stickel, Automated deduction by theory resolution, Journal of Automated Reasoning, v.1 n.4, p.333-355, 1985
	24	L. Wallen, Generating connection calculi from tableau and sequent based proof systems, Artificial intelligence and its applications, John Wiley & Sons, Inc., New York, NY, 1987
	25	Hantao Zhang , Deepak Kapur, First-Order Theorem Proving Using Conditional Rewrite Rules, Proceedings of the 9th International Conference on Automated Deduction, p.1-20, May 23-26, 1988

CITED BY 4

	G. Aguilera , I. P. de Guzman , M. Ojeda-Aciego , A. Valverde, Reductions for non-clausal theorem proving, Theoretical Computer Science, v.266 n.1-2, p.81-112, 09/06/2001
	Anavai Ramesh , George Becker , Neil V. Murray, CNF and DNF Considered Harmful for Computing Prime Implicants/Implicates, Journal of Automated Reasoning, v.18 n.3, p.337-356, June 1997
	Anavai Ramesh , Bernhard Beckert , Reiner Hähnle , Neil V. Murray, Fast Subsumption Checks Using Anti-Links, Journal of Automated Reasoning, v.18 n.1, p.47-83, February 1997
	Meghyn Bienvenu, Prime implicate normal form for ALC concepts, Proceedings of the 23rd national conference on Artificial intelligence, p.412-417, July 13-17, 2008, Chicago, Illinois