Upside-Down Transformation in SOL/Connection Tableaux and Its Application

  • Koji Iwanuma
  • Katsumi Inoue
  • Hidetomo Nabeshima
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3722)


In this paper, we study an upside-down transformation of a branch in SOL/Connection tableaux and show that SOL/Connection tableaux using the folding-up operation can always accomplish a size-preserving transformation for any branch in any tableau. This fact solves the exponentially-growing size problem caused both by the order- preserving reduction and by an incremental answer computation problem.


Model Elimination Automate Theorem Prove Automate Deduction Break Reduction Positive Literal 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Baumgartner, P., Furbach, U., Stolzenburg, F.: Computing answers with model elimination. Artificial Intelligence 90, 135–176 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Lee, C.T.: A completeness theorem and computer program for finding theorems derivable from given axioms. Ph.D. thesis, Department of Electrical Engineering and Computer Science, University of California, Berkeley, CA (1967)Google Scholar
  3. 3.
    Inoue, K.: Linear resolution for consequence finding. Artificial Intelligence 56, 301–353 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Inoue, K.: Automated abduction. In: Kakas, A.C., Sadri, F. (eds.) Computational Logic: Logic Programming and Beyond. LNCS (LNAI), vol. 2408, pp. 311–341. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  5. 5.
    Iwanuma, K., Inoue, K., Satoh, K.: Completeness of pruning methods for consequence finding procedure SOL. In: Baumgartner, P., Zhang, H. (eds.) Proceedings of the 3rd International Workshop on First-Order Theorem Proving, pp. 89–100 (2000)Google Scholar
  6. 6.
    Inoue, K., Iwanuma, K.: Speculative Computation Through Consequence-Finding in Multi-agent Environments. Ann. Math. Artif. Intell. 42(1-3) (2004)Google Scholar
  7. 7.
    Kunen, K.: The semantics of Answer Literals. J. Automated Reasoning 17, 83–95 (1996)zbMATHMathSciNetGoogle Scholar
  8. 8.
    Letz, R., Goller, C., Mayr, K.: Controlled integration of the cut rule into connection tableau calculi. Journal of Automated Reasoning 13, 297–338 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Letz, R.: Clausal tableaux. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction: A Basis for Applications, vol. 1, pp. 39–68. Kluwer, Dordrecht (1998)Google Scholar
  10. 10.
    Letz, R.: Using Mating for Pruning Connection Tableaux. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, pp. 381–396. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  11. 11.
    Loveland, D.W.: Automated Theorem Proving: A Logical Basis. North-Holland, Amsterdam (1978)zbMATHGoogle Scholar
  12. 12.
    Marquis, P.: Consequence finding algorithms. In: Gabbay, D.M., Smets, P. (eds.) Handbook for Defeasible Reasoning and Uncertain Management Systems, vol. 5, pp. 41–145. Kluwer Academic, Dordrecht (2000)Google Scholar
  13. 13.
    Spencer, B.: Avoiding Duplicate Proofs with the Foothold Refinement. Ann. Math. Artif. Intell. 12(1-2), 117–140 (1994)zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Koji Iwanuma
    • 1
  • Katsumi Inoue
    • 2
  • Hidetomo Nabeshima
    • 1
  1. 1.University of YamanashiYamanashiJapan
  2. 2.National Institute of InformaticsTokyoJapan

Personalised recommendations