Abstract
For many reasoning tasks in Artificial Intelligence, it is much simpler (or even essential) to deal with ground inferences rather than with inferences comprising variables. The usual approach to guarantee ground inferences is to introduce means for enumerating the underlying Herbrand-universe so that during subsequent inferences variables become bound in turn to the respective Herbrand-terms. The inherent problem with such an approach is that it may cause a tremendous number of unnecessary backtracking steps due to heaps of incorrect variable instantiations. In this paper, we propose a new concept that refrains from backtracking by appeal to novel inference rules that allow for correcting previous variable bindings. We show that our approach is not only beneficial for classical proof systems but it is also well-suited for tasks in knowledge representation and reasoning. The major contribution of this paper lies actually in an application of our approach to a calculi conceived for reasoning with default logic.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
P. Baumgartner, P. Frohlich, U. Furbach, and W. Nejdl. Semantically guided theorem proving for diagnosis application. In Proceedings of the International Joint Conference on Artificial Intelligene. Morgan Kaufmann Publishers, 1997.
P. Besnard. An Introduction to Default Logic. Symbolic Computation-Artifical Intelligence. Springer Verlag, 1989.
S. Brüning. On Restricting the Generation of Clause Instances. In C. Bozşahin, U. Halici, K. Oflazer, and N. Yalabik, editors,3rd Turkish Symposium on Artificial Intelligence and Neural Networks, pages 277–286. Middle East Technical University, Ankara, Türkiye, 1994.
S. Ceri, G. Gottlob, and L. Tanca. Logic Programming and Databases. Springer, 1990.
C. Fermüller, A. Leitsch, T. Tammet, and N. Zamov. Resolution Methods for the Decision Problem, volume 679 of LNAI. Springer-Verlag, 1993.
R. Letz, S. Bayerl, J. Schumann, and W. Bibel. SETHEO: A high-performance theorem prover. Journal of Automated Reasoning, 8(2):183–212, 1992.
R. Letz, K. Mayr, and Ch. Goller. Controlled integrations of the cut rule into connection tableau calculi. Journal of Automated Reasoning, 13(3):297–338, 1994.
D. Loveland. A simplified format for the model elimination theorem-proving procedure. Journal of the ACM, 16(3):349–363, 1969.
K. M. Munch. A New Reduction Rule for the Connection Graph Proof Procedure. Journal of Automated Reasoning, 4:425–444, 1988.
P. Nicolas and T. Schaub. The XRay system: An implementation platform for local queryanswering in default logics. In A. Hunter and S. Parsons, editors, Applications of Uncertainty Formalisms in Information Systems, volume 1455 of Lecture Notes in Artificial Intelligence, pages 354–378. Springer Verlag, 1998.
D. Poole, R. Goebel, and R. Aleliunas. Theorist: A logical reasoning system for defaults and diagnosis. In N. Cercone and G. McCalla, editors, The Knowledge Frontier: Essays in the Representation of Knowledge, chapter 13, pages 331–352. Springer Verlag, New York, 1987.
R. Reiter. A logic for default reasoning. Artificial Intelligence, 13(1-2):81–132, 1980.
T. Schaub and S. Brüning. Prolog technology for default reasoning: Proof theory and compilation techniques. Artificial Intelligence, 109(1):1–75, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brüning, S., Schaub, T. (1999). Avoiding Non-Ground Variables. In: Hunter, A., Parsons, S. (eds) Symbolic and Quantitative Approaches to Reasoning and Uncertainty. ECSQARU 1999. Lecture Notes in Computer Science(), vol 1638. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48747-6_9
Download citation
DOI: https://doi.org/10.1007/3-540-48747-6_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66131-3
Online ISBN: 978-3-540-48747-0
eBook Packages: Springer Book Archive