Skip to main content
SpringerLink
Log in

Disproving False Conjectures

  • Conference paper
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2003)

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

Abstract.

For automatic theorem provers it is as important to disprove false conjectures as it is to prove true ones, especially if it is not known ahead of time if a formula is derivable inside a particular inference system. Situations of this kind occur frequently in inductive theorem proving systems where failure is a common mode of operation. This paper describes an abstraction mechanism for first-order logic over an arbitrary but fixed term algebra to second-order monadic logic with 0 successor functions. The decidability of second-order monadic logic together with our notion of abstraction yields an elegant criterion that characterizes a subclass of unprovable conjectures.

Serge Autexier: This work was supported by the German Academic Exchange Service DAAD & the Deutsche Forschungsgemeinschaft (DFG) under grant Hu-737/1-2.

Carsten Schürmann: This work was supported in part by the National Science Foundation NSF under grants CCR-0133502 and INT-9909952.

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Andrews, P.B., Bishop, M., Brown, C.E.: System Description: TPS: A Theorem Proving System for Type Theory. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 164–169. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  2. Autexier, S., Hutter, D., Langenstein, B., Mantel, H., Rock, G., Schairer, A., Stephan, W., Vogt, R., Wolpers, A.: Vse: Formal methods meet industrial needs. International Journal on Software Tools for Technology Transfer, Special issue on Mechanized Theorem Proving for Technology. Springer (September 1998)

    Google Scholar 

  3. Autexier, S., Hutter, D., Mossakowski, T., Schairer, A.: The development graph manager MAYA. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, p. 495. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  4. Autexier, S., Schürmann, C.: Disproving False Conjectures. SEKI Technical Report SR-2003-06, CS Dep., Saarland University, Saarbrücken, Germany (2003)

    Google Scholar 

  5. Giunchiglia, F., Walsh, T.: A theory of abstraction. Artificial Intelligence 57(2-3), 323–389 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  6. Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the Association for Computing Machinery 40(1), 143–184 (1993)

    MATH  MathSciNet  Google Scholar 

  7. Hodgson, K., Slaney, J.: Development of a semantically guided theorem prover. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 443–447. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  8. Klarlund, N.: Mona & fido: The logic-automaton connection in practice. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol. 1414. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  9. Nadathur, G., Miller, D.: An overview of λProlog. In: Bowen, K.A., Kowalski, R.A. (eds.) Fifth International Logic Programming Conference, Seattle, Washington, August 1988, pp. 810–827. MIT Press, Cambridge (1988)

    Google Scholar 

  10. Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society 141, 1–35 (1969)

    Article  MATH  MathSciNet  Google Scholar 

  11. Schürmann, C., Autexier, S.: Towards proof planning for \({\it M}^{+}_{\omega}\). Electronic Notes in Theoretical Computer Science 70(2) (2002)

    Google Scholar 

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

    MATH  Google Scholar 

  13. Siekmann, J., et al.: Proof development with Ωmega. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 144–149. Springer, Heidelberg (2002)

    Google Scholar 

  14. Vardi, M.Y.: The complexity of relational query languages (extended abstract). In: Proceedings of the 14th Annual ACM Symposium on Theory of Computing, pp. 137–146 (1982)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. FR 6.2 Informatik, Saarland University,  

    Serge Autexier

  2. German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany

    Serge Autexier

  3. Yale University, New Haven, USA

    Carsten Schürmann

Authors
  1. Serge Autexier
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Carsten Schürmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Rice University, 77251-1892, Houston, TX, U.S.A.

    Moshe Y. Vardi

  2. University of Manchester, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Autexier, S., Schürmann, C. (2003). Disproving False Conjectures. In: Vardi, M.Y., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2003. Lecture Notes in Computer Science(), vol 2850. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39813-4_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-39813-4_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-20101-4

  • Online ISBN: 978-3-540-39813-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation