Abstract
In this paper, the notions of polynomial–time model equivalent reduction and polynomial–space model equivalent reduction are introduced in order to investigate in a subtle way the expressive power of different theories. We compare according to these notions some classes of propositional formulas and quantified Boolean formulas. Our results show that classes of theories with the same complexity might have different representation strength under some conjectures which are widely believed to be true in computation complexity theory.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ben-Eliyahu, R., Dechter, R.: Default Logic, Propositional Logic and Constraints. In: Proceedings of the Ninth National Conference on Artificial Intelligence (AAAI 1991) (1991)
Cadoli, M., Donini, F.M., Schaerf, M.: Is Intractability of Nonmonotonic Reasoning a Real Drawback. Artificial intelligence 88(2), 215–251 (1996)
Clark, K.: Negation as failure. In: Gallaire, H., Minker, J. (eds.) Logic and Data Bases, pp. 293–322. Plenum Press, New York
Ebbinhaus, H.D., Flum, J.: Finite Model Theory. Springer, Heidelberg (1999)
Eiter, T., Gottlob, G.: On the Computational Cost of Disjunctive Logic Programming: Propositional Case. Annals of Mathematics and Artificial Intelligence 15, 289–323 (1995)
Fages, F.: Consistency of Clark’s Completion and Existence of Stable Models. Journal of Methods of Logic in Computer Science 1, 51–60 (1994)
Flögel, A.: Resolution für Quantifizierte Boole’sche Formeln, Disertation, Paderborn University (1993)
Greenlaw, R., Hoover, H.J., Ruzzo, W.L.: Limits to Parallep Computation: P-Completeness theory. Oxford University Press, Oxford (1995)
Gelfond, M., Lifschitz, V.: The Stable Model Semantics for Logic Programming. In: Proceedings of the 5th International Conference on Logic Programming, pp. 1070–1080. The MIT Press, Cambridge (1988)
Gelfond, M., Lifschitz, V.: Classical Negation in Logic Programs and Disjunctive Database. New Generation Computing 9, 365–385 (1991)
Gogic, G., Kautz, H., Papadimitriou, C., Selman, B.: The Comparative Liguistics of Knowledge Representation. In: Proceedings of IJCAI 1995, Montreal, Canada (1995)
Karpinski, M., Kleine Büning, H., Schmitt, P.H.: On the Computational Complexity of Quantified Horn Clauses. In: Börger, E., Kleine Büning, H., Richter, M.M. (eds.) CSL 1987. LNCS, vol. 329, pp. 129–137. Springer, Heidelberg (1988)
Kleine Büning, H., Lettmann, T.: Propositional Logic: Deduction and Algorithms. Cambridge University Press, Cambridge (1999)
Kleine Büning, H., Zhao, X.: Equivalence Models for Quantified Boolean Formulas. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 224–234. Springer, Heidelberg (2005)
Johnson, D.S.: A Catalog of Complexity Classes. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. A, pp. 67–161. Elsevier Science Publisher (North-Holland), Amsterdam (1990)
Lee, J., Lin, F.: Loop Formulas for Circumscription. In: AAAI 2004, pp. 281–286 (2004)
Lee, J., Lifschitz, V.: Loop Formulas for Disjunctive Logic Programs. In: Palamidessi, C. (ed.) ICLP 2003. LNCS, vol. 2916, pp. 451–465. Springer, Heidelberg (2003)
Lifschitz, V., Razborov, A.: Why Are There So Many Loop Formulas (2003) (Manuscription)
Lifschitz, V., Pearce, D., Valverde, A.: Strongly Equivalent Logic Programs. ACM Transactions on Computational Logic 2, 526–541 (2001)
Lin, F., Zhao, Y.: ASSAT: Computing Answer Sets of a Logic Program by SAT Solvers. Artifficial Intelligence 157, 115–137 (2004)
Konolige, K.: On the Relation between Default and Autoepistemic Logic. Artificial Intelligence 35(3), 343–382 (1988)
Marek, W., Truszczyński, M.: Nonmonotonic Logic. Springer, Heidelberg (1993)
Spira, P.M.: On Time Hardware Complexity Tradeoffs for Boolean Functions. In: Proceedings of the 4th Hawaii Symposium on System Science, Western Periodicals Company, North Hollywood, pp. 525–527 (1971)
Tseitin, G.S.: On the Complexity of Derivation in Propositional Calculus. In: Silenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, Part II, pp. 115–125 (1970)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhao, X., Büning, H.K. (2005). Model-Equivalent Reductions. In: Bacchus, F., Walsh, T. (eds) Theory and Applications of Satisfiability Testing. SAT 2005. Lecture Notes in Computer Science, vol 3569. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11499107_26
Download citation
DOI: https://doi.org/10.1007/11499107_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26276-3
Online ISBN: 978-3-540-31679-4
eBook Packages: Computer ScienceComputer Science (R0)