Abstract
A resolution based proof procedure for order-sorted predicate logic is presented where sorts are represented by feature terms. Term unification is extended by feature unification. Soundness and completeness of the calculus presented are reduced to the soundness and completeness results for an order-sorted predicate calculus with a fixed sort lattice containing primitive sorts only.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Aït-Kaçi, H., A Lattice-Theoretic Approach to Computation Based on a Calculus of Partially-Ordered Type Structures, Ph.D. Thesis, Computer and Information Science, Univ. of Pennsylvania, Philadelphia, 1984.
Aït-Kaçi, H., Nasr, R., LOGIN: A Logic Programming Language with Built-In Inheritance, J. Logic Programming 3, 1986, 185–215.
Beierle, C., Dörre, J., Pletat, U., Schmitt, P. H., Studer, R., The Knowledge Representation Language LLILOG, LILOG-Report 41, IBM Germany, Stuttgart, 1988.
Beierle, C., Pletat, U., Feature Graphs and Abstract Data Types: A Unifiying Approach, LILOG Report 39, IBM Germany, Stuttgart, 1988. To appear in: Proc. COLING '88, Budapest, 1988.
Herzog, O., et al., LILOG-Linguistic and Logic Methods for the Computational Understanding of German, LILOG-Report 1b, IBM Germany,Stuttgart, 1986.
Johnson, M.E., Attribute-Value Logic and the Theory of Grammar, PhD Dissertation, Stanford University, 1987. To appear as CSLI Lecture Notes.
Karl Mark G. Raph: The Markgraf Karl Refutation Procedure, Internal Report, Memo-Seki-MK-84-01, Fachbereich Informatik, Universität Kaiserslautern, 1984.
Kasper, R.T., Rounds, W.C., A logical Semantics for Feature Structures, Proc. of the 24th Annual Meeting of the Association of Computational Linguistics, Columbia University, New York, 1986, 257–265.
Rollinger, C. R., Studer, R., Uszkoreit, H., Wachsmuth, I., Textunderstanding in LILOG — Sorts and Reference Objects, Proc. 2. Internationaler GI-Kongreß in München, Informatik-Fachberichte 155, Springer-Verlag, Heidelberg et al.,1987.
Schmidt-Schauss, M., Computational Aspects of an Order-Sorted Logic with Term Declaration, Dissertation, University of Kaiserslautern, 1988.
Shieber, S. M., An Introduction to Unification-Based Approaches to Grammar, CSLI Lecture Notes 4, Stanford University, California, 1986.
Smolka, G., A Feature Logic with Subsorts, LILOG-Report 33, IBM Germany, Stuttgart, 1988.
Uszkoreit, H., STUF: A Description of the Stuttgart Type Unification Formalism, LILOG-Report 16, IBM Germany, Stuttgart, 1987.
Walther, C., A Many-Sorted Calculus Based on Resolution and Paramodulation, in Research Notes in Artificial Intelligence, Pitman, London, and Morgan Kaufmann, Los Altos, Calif., 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag
About this paper
Cite this paper
Bläsius, K.H., Hedtstück, U. (1988). Resolution with feature unification. In: Börger, E., Büning, H.K., Richter, M.M. (eds) CSL '87. CSL 1987. Lecture Notes in Computer Science, vol 329. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50241-6_26
Download citation
DOI: https://doi.org/10.1007/3-540-50241-6_26
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-50241-8
Online ISBN: 978-3-540-45960-6
eBook Packages: Springer Book Archive