Skip to main content
SpringerLink
Log in

A Tableaux Calculus for Reducing Proof Size

  • Conference paper
  • First Online:
Automated Reasoning (IJCAR 2018)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 10900))

Included in the following conference series:

Abstract

A tableau calculus is proposed, based on a compressed representation of clauses, where literals sharing a similar shape may be merged. The inferences applied on these literals are fused when possible, which can reduce the size of the proof. It is shown that the obtained proof procedure is sound, refutationally complete and can reduce the size of the tableau by an exponential factor. The approach is compatible with all usual refinements of tableaux.

M.P. Lettmann—Funded by FWF project W1255-N23.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    We recall that the cut rule consists in expanding a tableau by adding two branches with \(\lnot \phi \) and \(\phi \) respectively, where \(\phi \) is any formula (intuitively \(\phi \) can be viewed as a lemma). A cut is atomic if \(\phi \) is atomic.

  2. 2.

    Due to the limited number of pages, we omit proofs that are not necessary for the understanding of the method. A full version can be found in [10].

  3. 3.

    Note that both ordinary and abstraction variables are renamed.

  4. 4.

    Actually, due to the above conditions, the variables in \(\mathrm {dom}(\theta )\) only occur in the subtree of root \(\mu \), hence \(\theta \) only affects this subtree.

  5. 5.

    Connection tableaux can be seen as ordinary tableaux in which any application of the Expansion rule must be followed by the closure of a branch, using one of the newly added literals and the previous literal in the branch.

  6. 6.

    Hyper-tableaux may be viewed in our framework as ordinary tableaux in which the Expansion rule must be followed by the closure of all the newly added branches containing negative literals.

  7. 7.

    In a \(\varPi _2\)-cut, the cut formula is of the form \(\forall x\exists yA\) where A is a quantifier-free formula.

References

  1. Baumgartner, P.: Hyper tableau—the next generation. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 60–76. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-69778-0_14

    Chapter  Google Scholar 

  2. de Rijke, M.: In: D’Agostino, M., Gabbay, D.M., Hähnle, R., Posegga, J. (eds.) Handbook of Tableau Methods (2001). J. Logic, Lang. Inform. 10(4), 518–523

    Google Scholar 

  3. Eder, E.: Relative Complexities of First-Order Logic Calculi. Springer, Heidelberg (1990). https://doi.org/10.1007/978-3-322-84222-0

    Book  MATH  Google Scholar 

  4. Fitting, M.: First-Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer, New York (1990). https://doi.org/10.1007/978-1-4684-0357-2

    Book  MATH  Google Scholar 

  5. Giese, M.: Incremental closure of free variable tableaux. In: Goré, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 545–560. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45744-5_46

    Chapter  Google Scholar 

  6. Hähnle, R.: Tableaux and related methods. In Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, chap. 3, pp. 100–178. Elsevier Science (2001)

    Chapter  Google Scholar 

  7. Hansen, C.M., Antonsen, R., Giese, M., Waaler, A.: Incremental variable splitting. J. Symb. Comput. 47(9), 1046–1065 (2012)

    Article  MathSciNet  Google Scholar 

  8. Hetzl, S., Leitsch, A., Reis, G., Weller, D.: Algorithmic introduction of quantified cuts. Theoret. Comput. Sci. 549, 1–16 (2014)

    Article  MathSciNet  Google Scholar 

  9. Leitsch, A., Lettmann, M.P.: The problem of \(\Pi_{2}\)-cut-introduction. Theoret. Comput. Sci. 706, 83–116 (2018)

    Article  MathSciNet  Google Scholar 

  10. Lettmann, M.P., Peltier, N.: A tableaux calculus for reducing proof size. In: CoRR, abs/1801.04163 (2018)

    Google Scholar 

  11. Letz, R., Mayr, K., Goller, C.: Controlled integration of the cut rule into connection tableau calculi. J. Autom. Reason. 13(3), 297–337 (1994)

    Article  MathSciNet  Google Scholar 

  12. Letz, R., Stenz, G.: Model elimination and connection tableau procedures. In: Handbook of Automated Reasoning, pp. 2015–2112. Elsevier Science Publishers B. V., Amsterdam (2001)

    Chapter  Google Scholar 

  13. Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2. Elsevier and MIT Press (2001)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Logic and Computation, Technische Universität Wien, Vienna, Austria

    Michael Peter Lettmann

  2. Univ. Grenoble Alpes, CNRS, Grenoble INP, LIG, 38000, Grenoble, France

    Nicolas Peltier

Authors
  1. Michael Peter Lettmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nicolas Peltier
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Michael Peter Lettmann .

Editor information

Editors and Affiliations

  1. Université de Lorraine, Vandoeuvre-lès-Nancy, France

    Didier Galmiche

  2. Baden-Wuerttemberg Cooperative State University, Stuttgart, Germany

    Stephan Schulz

  3. University of Trento, Trento, Italy

    Roberto Sebastiani

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Lettmann, M.P., Peltier, N. (2018). A Tableaux Calculus for Reducing Proof Size. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds) Automated Reasoning. IJCAR 2018. Lecture Notes in Computer Science(), vol 10900. Springer, Cham. https://doi.org/10.1007/978-3-319-94205-6_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-94205-6_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-94204-9

  • Online ISBN: 978-3-319-94205-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation