[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

On quasitautologies

  • Contributed Papers
  • Conference paper
  • First Online:
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 1997)

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

  • 112 Accesses

Abstract

Quasitautologies are formulas valid solely by the properties of identity and of propositional connectives. In connection with Herbrand's theorem the quasitautologies are central to the automated theorem proving with identity. It is a matter of folklore in logic that the predicate of being a quasitautology is decidable. We present a finitary proof of this fact by a powerful method of transformation of tableaux with identity rules. This should shed some light on the subtleties of tableaux with identity. We have extended this method in a separate paper to a much harder finitary proof of the conservativity of Skolem axioms. The question of why we should prefer finitary over model-theoretic proofs occurs frequently in logic. The answer is always simple: we obtain more information from a finitary proof than from a model-theoretic one. In our case, we get that quasitautologies can be proved by tableaux with a subterm property.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J. Barwise. An introduction to first-order logic. In J. Barwise, editor, Handbook of Mathematical Logic, pages 5–46. North-Holland, 1977.

    Google Scholar 

  2. G. S. Boolos and R. C. Jeffrey. Computability and Logic. Cambridge University Press, second edition, 1980.

    Google Scholar 

  3. S. R. Buss. An introduction to proof theory. To appear in Handbook of Proof Theory (ed. S. Buss), 1996.

    Google Scholar 

  4. D. Cyrluk, P. Lincoln, and N. Shankar. On Shostak's decision procedure for combinations of theories. In M. A. McRobbie and J. K. Slaney, editors, Proceedings of CADE-13, number 1104 in LNAI, pages 463–477. Springer Verlag, 1996.

    Google Scholar 

  5. A. Degtyarev, Y. Gurevich, and A. Voronkov. Herbrand's theorem and equational reasoning: Problems and solutions. In Bulletin of the European Association for Theoretical Computer Science, volume 60, October 1996. The ”Logic in Computer Science” column.

    Google Scholar 

  6. A. Degtyarev and A. Voronkov. Simultaneous rigid E-unification is undecidable. UPMAIL Technical Report 105, Uppsala University, Computing Science Department, May 1995.

    Google Scholar 

  7. A. Degtyarev and A. Voronkov. The undecidability of simultaneous rigid E-unification. Theoretical Computer Science, 166:291–300, 1996.

    Google Scholar 

  8. P. Hájek and P. Pudlák. Metamathematics of First-Order Arithmetic. Springer Verlag, 1993.

    Google Scholar 

  9. J. Komara and P. J. Voda. Syntactic reduction of predicate tableaux to propositional tableaux. In P. Baumgartner, R. Haehnle, and J. Posegga, editors, Proceedings of TABLEAUX '95, number 918 in LNAI, pages 231–246. Springer Verlag, 1995.

    Google Scholar 

  10. J. Komara and P. J. Voda. On Skolem axioms. Technical report, Institute of Informatics, Faculty of Mathematics and Physics, Comenius University, Bratislava, November 1996.

    Google Scholar 

  11. G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245–257, 1979.

    Google Scholar 

  12. G. Nelson and D. C. Oppen. Fast decision procedures based on congruence closure. Journal of the ACM, 27(2):356–364, 1980.

    Google Scholar 

  13. J. R. Shoenfield. Mathematical Logic. Addison-Wesley, 1967.

    Google Scholar 

  14. R. E. Shostak. An algorithm for reasoning about equality. Communications of the ACM, 21(7):583–585, July 1978.

    Google Scholar 

  15. R. E. Shostak. Deciding combinations of theories. Journal of the ACM, 31(1):1–12, January 1984.

    Google Scholar 

  16. R. Smullyan. First Order Logic. Springer Verlag, 1968.

    Google Scholar 

  17. G. Takeuti. Proof Theory. North-Holland, 1975.

    Google Scholar 

  18. P. J. Voda and J. Komara. On Herbrand skeletons. Technical report, Institute of Informatics, Faculty of Mathematics and Physics, Comenius University, Bratislava, July 1995. Revised January 1996. Submitted for publication.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Informatics, Faculty of Mathematics and Physics, Comenius University, Mlynská dolina, 842 15, Bratislava, Slovakia

    Ján Komara & Paul J. Voda

Authors
  1. Ján Komara
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Paul J. Voda
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Didier Galmiche

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Komara, J., Voda, P.J. (1997). On quasitautologies. In: Galmiche, D. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1997. Lecture Notes in Computer Science, vol 1227. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027417

Download citation

  • DOI: https://doi.org/10.1007/BFb0027417

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-62920-7

  • Online ISBN: 978-3-540-69046-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation