Using resolution for extending KL-ONE-type languages

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Using resolution for extending KL-ONE-type languages

Full text

Pdf (695 KB)

Source

Conference on Information and Knowledge Management archive
Proceedings of the fourth international conference on Information and knowledge management table of contents

Baltimore, Maryland, United States

Pages: 326 - 332

Year of Publication: 1995

ISBN:0-89791-812-6

Author

Tanel Tammet

Department of Computing Science, Chalmers University of Technology and University of Göteborg, S-41296 Göteborg, Sweden

Sponsors

SIGIR: ACM Special Interest Group on Information Retrieval
SIGLINK: Hypertext, Hypermedia, and Web
SIGWEB: ACM Special Interest Group on Hypertext, Hypermedia, and Web
NSF : National Science Foundation
UMBC : U of MD Baltimore County
AAAI : Am Assoc for Artifical Intelligence
SIGART: ACM Special Interest Group on Artificial Intelligence

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 29, Citation Count: 1

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/221270.221605 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.

	Borgida et al 89	Borgida, A., Brachmann, R.J., McGuinness, D.L., Resnick, L.A. CLASSIC: A Structural Data Model for Objects. Proceedings of the 4th National Conference of the AAAI, pp 34-37, Austin, Texas, 1984.
	Brachmann, Schmolze 85	Brachmann, R.J., Schmolze, J.G. An overview of the KL-ONE knowledge representation system. Cognitive Science 9(2), 1985, 171- 216.
	Chang, Lee 73	Chin-Liang Chang , Richard C. Lee , Richard Char-Tung Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, Inc., Orlando, FL, 1997
	Fermüller 91	Fermftller, G. Deciding Classes of Clause Sets by Resolution. Ph.D. thesis, Technical University of Vienna 1991.
	FLTZ 93	C. Fermuller , T. Tammet , N. Zamov , Alexander Leitsch, Resolution Methods for the Decision Problem, Springer-Verlag New York, Inc., Secaucus, NJ, 1993
	Gurevich 73	Gurevich, Y. Formuly s odnim ~ (formulas with one V). In izbrannye voprosy algebry i logiki (Selected Questions in Algebr# and Logics). N#uk#, Novosibirsk, 1973, pp. 97- 110.
	Hollunder, Nutt 90	Hollunder, B. Nutt, W. Subsumption Algorithms for Concept Languages. Research report RR-90-04, DFKI GmbH, Kaiserslautern, Germany, 1990.
	Joyner 76	William H. Joiner, Jr., Resolution Strategies as Decision Procedures, Journal of the ACM (JACM), v.23 n.3, p.398-417, July 1976 [doi>10.1145/321958.321960]
	Kaczmarek et al 86	Kaczmarek, T.S., Bates, R., Robins, G. Recent Developments in NIKL. Proceedings of the 5th National Conference of the AAAI, pp. 578-587, Philadelphia, Pa. 1986.
	Leitsch 90	Alexander Leitsch, Deciding Horn classes by hyperresolution, Proceedings of the third workshop on Computer science logic, p.225-241, July 1990, Kaiserslautern, Germany
	Maslov 68	Maslov, S.Ju. The inverse method for establishing deducibility for logical calculi. Trudy Mat. Inst. Steklov 98 (1968) 26-87-= Proc. Steldov. Inst. Math. 98 (1968) 25- 96, MR 40 #5416; 43 #4620.
	Nebel, von Luck 88	Nebel, B., yon Luck, K. Hybrid reasoning in BACK. In Z.W. Ras, L. Saitta (editors): Methodologies for Intelligent Systems, pp. 260- 269, North Holland, Amsterdam, Netherlands, 1988.
	Patel-Schneider 84	Patel- Schneider, P. Small can be beautiful in knowledge representation. Proceedings of the IEEE Workshop on Principles of Knowledge-based Systems, pp. 11-16, Denver, Colorado, 1984.
	Robinson 65	J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
	Schmidt-Schauss, Smolka 88	Schmidt-Schauss, M., Smolka, G. Attributive Concept Descriptions with Unions and Complements. SEKI report SR-88-21, FB Informatik, Universit~t Kaiserslautern, Germany, 1988.
	Slagle 74	James R. Slagle, Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity, Journal of the ACM (JACM), v.21 n.4, p.622-642, Oct. 1974 [doi>10.1145/321850.321859]
	Tammet 90	T. Tammet, The resolution program, able to decide some solvable classes, Proceedings of the international conference on Computer logic, p.300-312, March 1990, Tallinn, USSR
	Tammet 91	Tanel Tammet, Using Resolution for Deciding Solvable Classes and Building Finite Models, Baltic Computer Science, Selected Papers, p.33-64, January 1991
	Tammet 92	Tammet, T. Resolution methods for decision problems and finitemodel building. Ph.D thesis. Department of Computer Science, Chalmers University of Technology / University of GSteborg, 1992.
	Vilain 85	Vilain, M.B. The restricted language architecture of a hybrid representation system. In R.J. Bachmann, H.J. Levesque, R. Reiter (editors): Proceedings of the 9th IJ- CAI, pp. 547-551, Los Angeles, California, 1985.
	Zamov 72	Zamov, N.K., On a bound for the complexity of terms in the resolution method. Trudy Mat. Inst. Steklov 128 (1972), pp 5-13.
	Zamov 89	Zamov, N.K., Maslov's inverse method and decidable classes. Annals of Pure and Applied Logic 42 (1989), 165-194.