Skip to main content
SpringerLink
Log in

TaMeD: A Tableau Method for Deduction Modulo

  • Conference paper
Automated Reasoning (IJCAR 2004)

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

Included in the following conference series:

Abstract

Deduction modulo is a formalism introduced to separate cleanly computations and deductions by reasoning modulo a congruence on propositions. A sequent calculus modulo has been defined by Dowek, Hardin and Kirchner as well as a resolution-based proof search method called Extended Narrowing And Resolution (ENAR), in which the congruences are handled through rewrite rules on terms and atomic propositions.

We define a tableau-based proof search method, called Tableau Method for Deduction modulo (TaMeD), for theorem proving modulo. We then give a syntactic proof of the completeness of the method with respect to provability in the sequent calculus modulo. Moreover, we follow in our proofs the same steps as the ENAR method in such a way that it allows to try and compare the characteristics of both methods.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Beckert, B.: Konzeption und Implementierung von Gleichheit für einen tableaubasierten Theorembeweiser. IKBS report 208, Science Center, Institute for Knowledge Based Systems, IBM Germany (1991)

    Google Scholar 

  2. Beckert, B.: Adding equality to semantic tableaux. In: Broda, K., D’Agostino, M., Goré, R., Johnson, R., Reeves, S. (eds.) Proceedings, 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Abingdon. TR-94/5, pp. 29–41. Imperial College, London (1994)

    Google Scholar 

  3. Beckert, B.: Rigid e-unification. In: Bibel, W., Schmidt, P.H. (eds.) Automated Deduction: A Basis for Applications. Foundations: Calculi and Methods, vol. I, Kluwer Academic Publishers, Dordrecht (1998)

    Google Scholar 

  4. Beckert, B., Hähnle, R.: An improved method for adding equality to free variable semantic tableaux. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 507–521. Springer, Heidelberg (1992)

    Google Scholar 

  5. Bonichon, R.: TaMeD: A tableau method for deduction modulo. To be published as a LIP6 report (2004)

    Google Scholar 

  6. Degtyarev, A., Voronkov, A.: The undecidability of simultaneous rigid eunification. Theoretical Computer Science 166(1-2), 291–300 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  7. Degtyarev, A., Voronkov, A.: What you always wanted to know about rigid e-unification. J. Autom. Reason. 20(1-2), 47–80 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  8. Degtyarev, A., Voronkov, A.: Equality reasoning in sequent-based calculi. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 10. Elsevier Science Publishers B.V, Amsterdam (2001)

    Google Scholar 

  9. Dowek, G., Hardin, T., Kirchner, C.: HOL-λσ: An intentional first-order expression of higher-order logic. In: RTA, pp. 317–331 (1999)

    Google Scholar 

  10. Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning (31), 33–72 (2003)

    Google Scholar 

  11. Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo, revised version. Rapport de recherce 4861, INRIA (2003)

    Google Scholar 

  12. Fitting, M.: First Order Logic and Automated Theorem Proving, 2nd edn. Springer, Heidelberg (1996)

    MATH  Google Scholar 

  13. Goubault-Larrecq, J., Mackie, I.: Proof Theory and Automated Deduction. Applied Logic Series. Kluwer Academic Publishers, Dordrecht (1997)

    MATH  Google Scholar 

  14. Kohlhase, M.: Higher-order automated theorem proving. In: Bibel, W., Schmidt, P.H. (eds.) Automated Deduction: A Basis for Applications. Foundations: Calculi and Methods, vol. I, Kluwer Academic Publishers, Dordrecht (1998)

    Google Scholar 

  15. Letz, R.: First-order tableau calculi. In: D’Agostino, M., Gabbay, D.M., Hähnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, Kluwer Academic Publishers, Dordrecht (2000)

    Google Scholar 

  16. Smullyan, R.: First Order Logic. Springer, Heidelberg (1968)

    MATH  Google Scholar 

  17. Stuber, J.: A model-based completeness proof of extended narrowing and resolution. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, p. 195. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LIP6,  

    Richard Bonichon

Authors
  1. Richard Bonichon
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Information Security Group, Dep. of Computer Science, ETH, Zurich, Switzerland

    David Basin

  2. LORIA & INRIA Lorraine UMR 7503,  

    Michaël Rusinowitch

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bonichon, R. (2004). TaMeD: A Tableau Method for Deduction Modulo. In: Basin, D., Rusinowitch, M. (eds) Automated Reasoning. IJCAR 2004. Lecture Notes in Computer Science(), vol 3097. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-25984-8_33

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-25984-8_33

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-22345-0

  • Online ISBN: 978-3-540-25984-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation