Signed Dual Tableaux for Kleene Answer Set Programs

  • Patrick Doherty
  • Andrzej SzałasEmail author
Part of the Outstanding Contributions to Logic book series (OCTR, volume 17)


Dual tableaux were introduced by Rasiowa and Sikorski (1960) as a cut free deduction system for classical first-order logic. In the current paper, a sound and complete proof procedure based on dual tableaux is proposed for \({R}_3\), which is the standard Kleene logic augmented with a weak negation connective and an implication connective proposed, in another context, by Shepherdson (1989). \({R}_3\) is used as a basis for defining Kleene Answer Set Programs (\(\textsc {ASP}^{K}\)programs). The semantics for \(\textsc {ASP}^{K}\)programs is based on strongly supported models. Both entailment procedures and model generation procedures for normal and non-normal \(\textsc {ASP}^{K}\)programs are proposed based on the use of dual tableaux and a model filtering technique. The dual tableau proof procedure extended with a model filtering technique is shown to be sound and complete for \(\textsc {ASP}^{K}\)programs, both normal and non-normal. Since there is a direct relationship between answer sets for classical ASP programs and \({R}_3\) models for \(\textsc {ASP}^{K}\)programs, it can be shown that the sound and complete dual tableaux proof procedure with filtering for \(\textsc {ASP}^{K}\)programs is also sound and complete for classical normal ASP programs. For classical non-normal ASP programs, the proof procedure is only sound, since an alternative semantics for disjunction is used in \(\textsc {ASP}^{K}\).


Signed tableaux Signed dual tableaux Answer set programming Kleene three-valued logic Strongly supported model 


  1. Baral, C. (2003). Knowledge Representation, Reasoning, and Declarative Problem Solving. Cambridge: Cambridge University Press.Google Scholar
  2. Beth, E. W. (1955). Semantic entailment and formal derivability. Mededelingen van de Koninklijke Nederlandse Akademie van Wetenschappen, 18(13), 309–342. Reprinted in Hintikka (1969).Google Scholar
  3. Borkowski, L. (Ed.). (1970). Selected Works by Jan Łukasiewicz. Amsterdan: North-Holland.Google Scholar
  4. Bresolin, D., Golińska-Pilarek, J., & Orłowska, E. (2006). A relational dual tableaux for interval temporal logics. Journal of Applied Non-classical Logics, 16(3–4), 251–277.CrossRefGoogle Scholar
  5. Brewka, G., Eiter, T., & Truszczyński, M. (2011). Answer set programming at a glance. Communications of the ACM, 54(12), 92–103.CrossRefGoogle Scholar
  6. Brewka, G., Niemela, I., & Truszczyński, M. (2003). Answer set optimization. In G. Gottlob & T. Walsh (Eds.), IJCAI-03, Proceedings of the 18th International Joint Conference on Artificial Intelligence (pp. 867–872). Acapulco, Mexico: Morgan Kaufmann.Google Scholar
  7. Cantone, D., Nicolosi Asmundo, M., & Orłowska, E. (2011). Dual tableau-based decision procedures for relational logics with restricted composition operator. Journal of Applied Non-classical Logics, 21(2), 177–200.CrossRefGoogle Scholar
  8. Cantone, D., Nicolosi Asmundo, M., & Orłowska, E. (2014). A dual tableau-based decision procedure for a relational logic with the universal relation. In L. Giordano, V. Gliozzi, & G. Pozzato (Eds.), Proceedings of the 29th Italian Conference on Computational Logic (Vol. 1195, pp. 194–209). CEUR Workshop Proceedings. Torino, Italy: Scholar
  9. Chan, E. P. F. (1993). A possible world semantics for disjunctive databases. IEEE Transactions on Knowledge and Data Engineering, 5(2), 282–292.CrossRefGoogle Scholar
  10. D’Agostino, M., Gabbay, D. M., Hähnle, R., & Posegga, J. (Eds.). (1999). Handbook of Tableau Methods. Dordrecht-Boston-London: Springer Netherlands.Google Scholar
  11. Doherty, P. (1991). A constraint-based approach to proof procedures for multivalued logics. In M. De Glas & D. M. Gabbay (Eds.), Proceedings of the 1st World Conference on Fundamentals of Artificial Intelligence, WOCFAI. Paris, France: Springer.Google Scholar
  12. Doherty, P., Kvarnstrom, J., & Szałas, A. (2016). Iteratively-supported formulas and strongly supported models for Kleene answer set programs (extended abstract). In L. Michael & A. C. Kakas (Eds.), Proceedings of Logics in Artificial Intelligence – 15th European Conference, JELIA (Vol. 10021, pp. 536–542). Lecture Notes in Computer Science. Larnaca, Cyprus.CrossRefGoogle Scholar
  13. Doherty, P. & Szałas, A. (2015). Stability, supportedness, minimality and Kleene answer set programs. In T. Eiter, H. Strass, M. Truszczyński, & S. Woltran (Eds.), Advances in Knowledge Representation, Logic Programming, and Abstract Argumentation: Essays dedicated to Gerhard Brewka on the Occasion of his 60th Birthday (Vol. 9060, pp. 125–140). Lecture Notes in Computer Science. Berlin: Springer.CrossRefGoogle Scholar
  14. Doherty, P. & Szałas, A. (2016). An entailment procedure for kleene answer set programs. In C. Sombattheera, F. Stolzenburg, F. Lin, & A. C. Nayak (Eds.), Proceedings of Multi-disciplinary Trends in Artificial Intelligence – 10th International Workshop, MIWAI (Vol. 10053, pp. 24–37). Lecture Notes in Computer Science. Chiang Mai, Thailand: Springer.Google Scholar
  15. Eiter, T., Faber, W., Fink, M., & Woltran, S. (2007). Complexity results for answer set programming with bounded predicate arities and implications. Annals of Mathematics and Artificial Intelligence, 51(2–4), 123–165.CrossRefGoogle Scholar
  16. Eiter, T. & Gottlob, G. (1993). Complexity results for disjunctive logic programming and application to nonmonotonic logics. In D. Miller (Ed.), Logic Programming, Proceedings of the 1993 International Symposium (pp. 266–278). Vancouver, Canada: MIT Press.Google Scholar
  17. Ferraris, P. & Lifschitz, V. (2011). On the minimality of stable models. In M. Balduccini & T. C. Son (Eds.), Logic Programming, Knowledge Representation, and Nonmonotonic Reasoning: Essays Dedicated to Michael Gelfond on the Occasion of his 65th Birthday (Vol. 6565, pp. 64–73). Lecture Notes in Computer Science. Berlin: Springer.Google Scholar
  18. Gebser, M., Kaminski, R., Kaufmann, B., & Schaub, T. (2012). Answer Set Solving in Practice. Synthesis Lectures on Artificial Intelligence and Machine Learning. New York: Morgan and Claypool Publishers.CrossRefGoogle Scholar
  19. Gebser M. & Schaub, T. (2013). Tableau calculi for logic programs under answer set semantics. ACM Transactions on Computational Logic, 14(2), 15:1–15:40.CrossRefGoogle Scholar
  20. Gelfond, M. & Kahl, Y. (2014). Knowledge Representation, Reasoning, and the Design of Intelligent Agents: The Answer-set Programming Approach. Cambridge: Cambridge University Press.Google Scholar
  21. Gelfond, M. & Lifschitz, V. (1988). The stable model semantics for logic programming. In R. A. Kowalski & K. A. Bowen (Eds.), Logic Programming, Proceedings of the 5th International Conference and Symposium (Vol. 2, pp. 1070–1080). Seattle, USA: MIT Press.Google Scholar
  22. Gelfond, M. & Lifschitz, V. (1991). Classical negation in logic programs and disjunctive databases. New Generation Computing, 9(3/4), 365–386.CrossRefGoogle Scholar
  23. Gentzen, G. (1934). Untersuchungen über das logische Schließen I. Mathematische Zeitschrift, 39(2), 176–210.Google Scholar
  24. Gentzen, G. (1935). Untersuchungen über das logische Schließen II. Mathematische Zeitschrift, 39(3), 405–431.Google Scholar
  25. Golińska-Pilarek, J., Muñoz-Velasco, E., & Mora Bonilla, A. (2012). Relational dual tableau decision procedure for modal logic K. Logic Journal of the IGPL, 20(4), 747–756.CrossRefGoogle Scholar
  26. Golińska-Pilarek, J. & Orłowska, E. (2007). Tableaux and dual tableaux: Transformation of proofs. Studia Logica, 85(3), 291–310.CrossRefGoogle Scholar
  27. Golińska-Pilarek, J. & Orłowska E. (2008). Logics of similarity and their dual tableaux: A survey. In G. Della Riccia, D. Dubois, R. Kruse, & H. -J. Lenz (Eds.), Preferences and Similarities (Vol. 504, pp. 129–159). CISM Courses and Lectures. Wien-New York: Springer.CrossRefGoogle Scholar
  28. Golińska-Pilarek, J. & Orłowska, E., (2011). Dual tableau for monoidal triangular norm logic MTL. Fuzzy Sets and Systems, 162, 39–52.CrossRefGoogle Scholar
  29. Hähnle, R. (1991). Uniform notation of tableau rules for multiple-valued logics. In Proceedings of the 21st International Symposium on Multiple-Valued Logic, ISMVL 1991 (pp. 238–245). Victoria, Canada: IEEE Computer Society.Google Scholar
  30. Hähnle, R. (1999). Tableaux for many-valued logics. In M. D’Agostino, D. M. Gabbay, R. Hähnle, & J. Posegga (Eds.), Handbook of Tableau Methods (pp. 529–580). Dordrecht-Boston-London: Springer Netherlands.CrossRefGoogle Scholar
  31. Hintikka, J. (Ed.). (1969). The Philosophy of Mathematics. Oxford: Oxford University Press.Google Scholar
  32. Kanger, S. (1957). Provability in Logic. Stockholm: Almqvist & Wiksell.Google Scholar
  33. Kleene, S. C. (1938). On notation for ordinal numbers. Journal of Symbolic Logic, 3(4), 150–155.CrossRefGoogle Scholar
  34. Konikowska, B., Morgan, C., & Orłowska, E. (1998). A relational formalisation of arbitrary finite-valued logics. Logic Journal of the IGPL, 6(5), 755–774.CrossRefGoogle Scholar
  35. Konikowska, B. & Orłowska, E. (2001). A relational formalisation of a generic many-valued modal logic. In E. Orłowska & A. Szałas (Eds.), Relational Methods for Computer Science Applications (Vol. 65, pp. 183–202). Studies in Fuzziness and Soft Computing. Heidelberg: Springer-Physica Verlag.CrossRefGoogle Scholar
  36. Leone, N., Rullo, P., & Scarcello, F. (1997). Disjunctive stable models: Unfounded sets, fixpoint semantics, and computation. Information and Computation, 135(2), 69–112.CrossRefGoogle Scholar
  37. Lifschitz, V. (2010). Thirteen definitions of a stable model. In A. Blass, N. Dershowitz, & W. Reisig (Eds.), Fields of Logic and Computation, Essays Dedicated to Yuri Gurevich on the Occasion of his 70th Birthday (Vol. 6300, pp. 488–503). Lecture Notes in Computer Science. Berlin: Springer.CrossRefGoogle Scholar
  38. Lifschitz, V. & Razborov, A. A. (2006). Why are there so many loop formulas? ACM Transansactions on Computational Logic, 7(2), 261–268.CrossRefGoogle Scholar
  39. Łukasiewicz, J. (1920). O logice trójwartościowej (in Polish). Ruch Filozoficzny, 5, 170–171. English translation: Borkowski (1970, pp. 87–88).Google Scholar
  40. Małuszyński, J. & Szałas, A. (2010). Living with inconsistency and taming nonmonotonicity. In O. de Moor, G. Gottlob, T. Furche, & A. J. Sellers (Eds.), Datalog Reloaded – 1st International Workshop, Datalog. Revised Selected Papers (Vol. 6702, pp. 384–398). Lecture Notes in Computer Science. Oxford, UK: Springer.Google Scholar
  41. Orłowska, E. & Golińska-Pilarek, J. (2011). Dual Tableaux: Foundations, Methodology, Case Studies. Trends in Logic. Dordrecht-Heidelberg-London-New York: Springer.CrossRefGoogle Scholar
  42. Rasiowa, H. & Sikorski, R. (1960). On the Gentzen theorem. Fundamenta Mathematicae, 48, 57–69.CrossRefGoogle Scholar
  43. Sakama, C. & Inoue, K. (1994). An alternative approach to the semantics of disjunctive logic programs and deductive databases. Journal of Automated Reasoning, 13(1), 145–172.CrossRefGoogle Scholar
  44. Shepherdson, J. C. (1989). A sound and complete semantics for a version of negation as failure. Theoretical Computer Science, 65(3), 343–371.CrossRefGoogle Scholar
  45. Smullyan, R. (1968). First-order Logic. New York: Dover Publications.Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Department of Computer and Information ScienceLinköping UniversityLinköpingSweden
  2. 2.Institute of Informatics, University of WarsawWarsawPoland

Personalised recommendations