Abstract
In this part we consider several resolution-based calculi with order-sorted signatures. We investigate resolution, paramodulation and factoring, G. Plotkin's resolution with built-in equational theories, J. Morris' E-resolution and M. Stickels theory resolution. We show that the completeness results that hold in the unsorted case or in the case of simple signatures [Wa83] hold also in the presence of term delarations. The results concerning the fact that the functionally reflexive axioms are not needed for clause sets with equations are in general not liftable, as shown in an example.
In this part we assume that there are no ill-sorted terms and literals. Furthermore, we sometimes omit the adjective ‘well-sorted’, but always mean that every thing is well-sorted, in particular substitutions are well-sorted.
Preview
Unable to display preview. Download preview PDF.
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
(1989). Sorted resolution-based calculi. In: Schmidt-Schauß, M. (eds) Computational Aspects of an Order-Sorted Logic with Term Declarations. Lecture Notes in Computer Science, vol 395. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0024071
Download citation
DOI: https://doi.org/10.1007/BFb0024071
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-51705-4
Online ISBN: 978-3-540-46774-8
eBook Packages: Springer Book Archive