Abstract
Approximate propositional logics provide a response to the intractability of classical inference for the modelling and construction of resource-bounded agents. They allow the degree of logical soundness (or completeness) to be balanced against the agent’s resource limitations.
We develop a logical semantics, based on a restriction to Finger’s logics of limited bivalence [5], and establish the adequacy of a clausal tableau based proof theory with respect to this semantics. This system is shown to characterise DPLL with restricted branching, providing a clear path for the adaptation of DPLL-based satisfiability solvers to approximate reasoning. Furthermore it provides insights into the traditional notion of problem hardness, as we show that the parameter set of these logics correspond to the strong backdoor for an unsatisfiable problem.
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.
Similar content being viewed by others
References
Cadoli, M.: Tractable Reasoning in Aritificial Intelligence. LNCS (LNAI), vol. 941. Springer, Heidelberg (1995)
Chopra, S., Parikh, R., Wassermann, R.: Approximate belief revision. In: Proc. of the Workshop on Language, Logic and Information, WoLLIC (2000)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. CACM 5(7), 394–397 (1962)
Finger, M.: Polynomial approximations of full propositional logic via limited bivalence. In: Proc. 9th European Conf. on Logics in AI, pp. 526–538 (2004)
Finger, M.: Towards polynomial approximations of full propositional logic. In: 17th Brazilian Symposium on AI, pp. 11–20 (2004)
Finger, M., Wassermann, R.: Tableaux for approximate reasoning. In: Proceedings of the IJCAI 2001 Workshop on Inconsistency in Data and Knowledge, Seattle, WA, USA, August 6-10, pp. 71–79 (2001)
Järvisalo, M., Junttila, T.A., Niemelä, I.: Unrestricted vs restricted cut in a tableau method for Boolean circuits. Annals of Math. and AI 44(4), 373–399 (2005)
Kilby, P., Slaney, J.K., Thiébaux, S., Walsh, T.: Backbones and backdoors in satisfiability. In: Proc. 20th Nat. Conf. on AI, pp. 1368–1373 (2005)
Li, C.M.: A constraint-based approach to narrow search trees for satisfiability. Information Processing Letters 71(2), 75–80 (1999)
Liberatore, P.: Complexity results on DPLL and resolution. ACM Trans. on Computational Logic 7(1), 84–107 (2006)
Mondadori, M.: Classical analytical deduction. Tech. rep., Annali dell’ Università di Ferrara, Nuova Serie, sezione III, Filosofia, Paper, n. 1 (1988)
Riani, J., Wassermann, R.: Using relevance to speed up inference. some empirical results. In: 17th Brazilian Symposium on AI, pp. 21–30 (2004)
Ruan, Y., Kautz, H.A., Horvitz, E.: The backdoor key: A path to understanding problem hardness. In: Proc. 19th Nat. Conf. on AI, pp. 124–130 (2004)
Szeider, S.: Backdoor sets for DLL subsolvers. J. of Automated Reasoning 35(1-3), 73–88 (2005)
Williams, R., Gomes, C.P., Selman, B.: Backdoors to typical case complexity. In: Proc. 18th Int. Joint Conf. on AI, pp. 1173–1178 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rajaratnam, D., Pagnucco, M. (2011). From Approximate Clausal Reasoning to Problem Hardness. In: Wang, D., Reynolds, M. (eds) AI 2011: Advances in Artificial Intelligence. AI 2011. Lecture Notes in Computer Science(), vol 7106. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25832-9_51
Download citation
DOI: https://doi.org/10.1007/978-3-642-25832-9_51
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-25831-2
Online ISBN: 978-3-642-25832-9
eBook Packages: Computer ScienceComputer Science (R0)