Abstract
We present a new approach to query answering in default logics. The basic idea is to treat default rules as classical implications along with some qualifying conditions restricting the use of such rules while query answering. We accomplish this by taking advantage of the conception of structure-oriented theorem proving provided by Bibel's connection method. We show that the structure-sensitive nature of the connection method allows for an elegant characterization of proofs in default logic. After introducing our basic method for query answering in default logics, we present a corresponding algorithm and describe its implementation. Both the algorithm and its implementation are obtained by slightly modifying an existing algorithm and an existing implementation of the standard connection method. In turn, we give a couple of refinements of the basic method that lead to conceptually different algorithms. The approach turns out to be extraordinarily qualified for implementations by means of existing automated theorem proving techniques. We substantiate this claim by presenting implementations of the various algorithms along with some experimental analysis.
Even though our method has a general nature, we introduce it in the first part of this paper with the example of constrained default logic. This default logic is tantamount to a variant due to Brewka, and it coincides with Reiter's default logic and a variant due to Łukaszewicz on a large fragment of default logic. Accordingly, our exposition applies to these instances of default logic without any modifications.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Baader, F. and Hollunder, B.: Embedding defaults into terminological knowledge representation formalisms, in B. Nebel, C. Rich, and W. Swartout (eds),Proc. 3rd Int. Conf. Principles of Knowledge Representation and Reasoning, Cambridge, MA, pp. 306–317 October 1992.
Besnard, P., Quiniou, R. and Quinton, P.: A theorem-prover for a decidable subset of default logic, inProc. AAAI Nat. Conf. Artificial Intelligence, 1983, pp. 27–30.
Bibel, W.:Automated Theorem Proving, 2nd edn, Vieweg, Braunschweig, 1987.
Brass, S.: Deduction with supernormal defaults, in P. Schmitt, G. Brewka and K. Jantke (eds),Nonmonotonic and Inductive Logic, Springer, Berlin, 1991, pp. 153–174.
Brewka, G.: Cumulative default logic: In defense of nonmonotonic inference rules,Artificial Intelligence 50(2) (1991), 183–205.
Brewka, G.:Nonmonotonic Reasoning: Logical Foundations of Commonsense, Cambridge University Press, Cambridge, 1991.
Brewka, G.: Adding priorities and specificity to default logic, in L. Pereira and D. Pearce (eds),European Workshop on Logics in Artificial Intelligence (JELIA'94), Springer, Berlin, 1994.
Cadoli, M., Eiter, T. and Gottlob, G.: Default logic as a query language, in J. Doyle, P. Torasso and E. Sandewall (eds),Proc. 4th Int. Conf. Principles of Knowledge Representation and Reasoning, 1994.
Cadoli, M. and Schaerf, M.: A survey on complexity results for non-monotonic logics,J. Logic Programming 17 (1993).
Delgrande, J. and Jackson, W.: Default logic revisited, in J. Allen, R. Fikes and E. Sandewall (eds),Proc. 2nd Int. Conf. Principles of Knowledge Representation and Reasoning, Morgan Kaufmann, 1991, pp. 118–127.
Delgrande, J., Schaub, T. and Jackson, W.: Alternative approaches to default logic,Artificial Intelligence 70 (1994), 167–237.
Dimopoulos, Y.: The computational value of joint consistency, in L. Pereira and D. Pearce (eds),European Workshop on Logics in Artificial Intelligence, Springer, Berlin, 1994, pp. 50–65.
Doyle, J.: A truth maintenance system,Artificial Intelligence 12 (1979), 231–272.
Eder, E.:Relative Complexities of First Order Calculi, Vieweg, Braunschweig, 1992.
Etherington, D.:Reasoning with Incomplete Information, Research Notes in Artificial Intelligence, Pitman/Morgan Kaufmann, London, 1988.
Etherington, D. and Reiter, R.: On inheritance hierarchies with exceptions, inProc. AAAI Nat. Conf. Artificial Intelligence, 1983, pp. 104–108.
Gelfond, M. and Lifschitz, V.: Logic programs with classical negation, inProc. Int. Conf. Logic Programming, 1990, pp. 579–597.
Gottlob, G.: Complexity results for nonmonotonic logics,J. Logic and Computation 2(3) (1992), 397–425.
Junker, U. and Konolige, K.: Computing the extensions of autoepistemic and default logic with a TMS, inProc. AAAI Nat. Conf. Artificial Intelligence, 1990.
Konolige, K.: On the relation between default and autoepistemic logic,Artificial Intelligence 35(2) (1988), 343–382.
Letz, R., Bayerl, S., Schumann, J. and Bibel, W.Setheo: A high-performance theorem prover,J. Automated Reasoning 8(2) (1992), 183–212.
Łukaszewicz, W.: Considerations on default logic-an alternative approach,Computational Intelligence 4 (1988), 1–16.
Mercer, R.: Using default logic to derive natural language suppositions, inProc. Canadian Soc. Computational Studies of Intelligence Conference, 1988, pp. 14–21.
Moore, R.: Semantical considerations on nonmonotonic logics,Artificial Intelligence 25 (1985), 75–94.
Neugebauer, G.: From horn clauses to first order logic: A graceful ascent, Technical Report AIDA-92-21, FG Intellektik, FB Informatik, TH Darmstadt, 1992.
Neugebauer, G. and Schaub, T.: A pool-based connection calculus, Technical Report AIDA-91-2, FG Intellektik, FB Informatik, TH Darmstadt, Alexanderstraße 10, D-64283 Darmstadt, Germany, January 1991.
Niemelä, I.: Decision procedure for autoepistemic logic, inProc. Conf. Automated Deduction, Argonne, 1988, pp. 675–684.
Niemelä, I.: A decision method for nonmonotonic reasoning based on autoepistemic reasoning, in J. Doyle, P. Torasso and E. Sandewall (eds),Proc. 4th Int. Conf. Principles of Knowledge Representation and Reasoning, Morgan Kaufmann, 1994, pp. 473–484.
Poole, D., Goebel, R. and Aleliunas, R.: Theorist: A logical reasoning system for defaults and diagnosis, in N. Cercone and G. McCalla (eds),The Knowledge Frontier: Essays in the Representation of Knowledge, Chapter 13, Springer, New York, 1987, pp. 331–352.
Reiter, R.: A logic for default reasoning,Artificial Intelligence 13(1–2) (1980), 81–132.
Reiter, R.: A theory of diagnosis from first principles,Artificial Intelligence 32(1) (1987), 57–96.
Risch, V.: Les Tableaux Analytiques au Service des Logiques de Defauts, PhD Thesis, Université Aix-Marseille II, G.I.A., Parc Scientifique et Technologique de Luminy, April 1993.
Rothschild, A.: Algorithmische Untersuchungen zu Defaultlogiken, Master Thesis, FG Intellektik, FB Informatik, TH Darmstadt, Alexanderstraße 10, D-64283 Darmstadt, 1993.
Schaub, T.: Assertional default theories: A semantical view, in J. Allen, R. Fikes and E. Sandewall (eds),Proc. 2nd Int. Conf. Principles of Knowledge Representation and Reasoning, Morgan Kaufmann, 1991, pp. 496–506.
Schaub, T.: On commitment and cumulativity in default logics, in R. Kruse and P. Siegel (eds),Proc. European Conf. Symbolic and Quantitative Approaches to Uncertainty, Springer, Berlin, 1991, pp. 304–309.
Schaub, T.: Considerations on Default Logics, PhD Thesis, Technische Hochshule Darmstadt, Alexanderstraße 10, D-64283 Darmstadt, Germany, November 1992.
Schaub, T.: On constrained default theories, in B. Neumann (ed.),Proc. European Conf. on Artificial Intelligence, Wiley, New York, 1992, pp. 304–308.
Schaub, T.: Variations of constrained default logic, in M. Clarke, R. Kruse and S. Moral (eds),Proc. European Conf. Symbolic and Quantitative Approaches to Reasoning and Uncertainty, Springer, Berlin, 1993, pp. 312–317.
Schaub, T.: Computing queries from prioritized default theories, in Z. Ras and M. Zemankova (eds),8th Int. Symp. Methodologies for Intelligent Systems, Springer, Berlin, 1994, pp. 584–593.
Schaub, T. and Thielscher, M.: A method for skeptical reasoning in constrained default logic, Technical Report, FG Intellektik, FB Informatik, TH Darmstadt, 1994.
Schwind, C.: A tableaux-based theorem prover for a decidable subset of default logic, in M. E. Stickel (ed.),CADE-10, Springer, Berlin, 1990.
Schwind, C. and Risch, V.: A tableaux-based characterization for default logic, in R. Kruse (ed.),Proc. European Conf. Symbolic and Quantitative Approaches to Uncertainty, Springer, Berlin, 1991, pp. 310–317.
Slaney, J. SCOTT: A model-guided theorem prover, inProc. Int. Joint Conf. on Artificial Intelligence, 1993, pp. 109–114.
Stickel, M.: A Prolog technology theorem prover,New Generation Computing 2 (1984), 371–383.
Thielscher, M. and Schaub, T.: Default reasoning by deductive planning,J. Automated Reasoning 15(1) (1995), 1–40.
Zhang, A. and Marek, W.: On the classification and existence of structures in default logic,Fundamenta Informaticae 8(4) (1990), 485–499.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Schaub, T. A new methodology for query answering in default logics via structure-oriented theorem proving. J Autom Reasoning 15, 95–165 (1995). https://doi.org/10.1007/BF00881832
Received:
Revised:
Issue Date:
DOI: https://doi.org/10.1007/BF00881832