Abstract
We introduce a calculus of stratified resolution, in which special attention is paid to clauses that “define” relations. If such clauses are discovered in the initial set of clauses, they are treated using the rule of definition unfolding, i.e. the rule that replaces defined relations by their definitions. Stratified resolution comes with a new, previously not studied, notion of redundancy: a clause to which definition unfolding has been applied can be removed from the search space. To prove completeness of stratified resolution with redundancies we use a novel technique of traces.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Apt, K.R., Blair, H.A.: Towards a theory of declarative knowledge. In: Minker, J. (ed.) Foundations of Deductive Databases and Logic Programming, pp. 89–148. Morgan Kaufmann, San Francisco (1988)
Bachmair, L., Ganzinger, H.: A theory of resolution. Research report MPI-I-97- 2-005, Max-Planck Institut für Informatik, Saarbrücken, Germany (1997); To appear in Handbook of Automated Reasoning, edited by A. Robinson and A. Voronkov
Bachmair, L., Ganzinger, H.: A theory of resolution. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning. Elsevier Science and MIT Press (2000)
Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation. Information and Computation 121, 172–192 (1995)
Van Gelder, A.: Negation as failure using tight derivations for general logic programs. In: Minker, J. (ed.) Deductive Databases and Logic Programming, pp. 149–177. Morgan Kaufmann, San Francisco (1988)
Kowalski, R.A., Kuehner, D.: Linear resolution with selection function. Artificial Intelligence 2, 227–260 (1971)
Lynch, C.: Oriented equational logic is complete. Journal of Symbolic Computations 23(1), 23–45 (1997)
Przymusinski, H.: On the declarative semantics of deductive databases and logic programs. In: Minker, J. (ed.) Foundations of Deductive Databases and Logic Programming, pp. 193–216. Morgan Kaufmann, San Francisco (1988)
Riazanov, A., Voronkov, A.: Vampire. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 292–296. Springer, Heidelberg (1999)
Voronkov, A.: How to optimize proof-search in modal logics: a new way of proving redundancy criteria for sequent calculi. Preprint 1, Department of Computer Science, University of Manchester (February 2000); To appear in LICS (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Degtyarev, A., Voronkov, A. (2000). Stratified Resolution. In: McAllester, D. (eds) Automated Deduction - CADE-17. CADE 2000. Lecture Notes in Computer Science(), vol 1831. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721959_28
Download citation
DOI: https://doi.org/10.1007/10721959_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67664-5
Online ISBN: 978-3-540-45101-3
eBook Packages: Springer Book Archive