Skip to main content
SpringerLink
Log in

A Proof Strategy Based on a Dual Representation

  • Conference paper
  • First Online:
Artificial Intelligence and Symbolic Computation (AISC 2000)

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

  • 331 Accesses

Abstract

In this paper we describe a first-order logic inference strategy based on information extracted from both conjunctive and disjunctive normal forms. We claim that the search problem for a proof can bene- fit from this further information, extending the heuristic possibilities of resolution and connection proof methods.

The authors express their thanks to the Brazilian research support agency “Funda- ção Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (Capes)” for the partial support of this work.

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. P.B. Andrews. Theorem proving via general matings. Journal of the ACM, 28(2):193–214, 1981.

    Article  MATH  Google Scholar 

  2. W. Bibel. Automated Theorem Proving. Vieweg Verlag, 1987.

    Google Scholar 

  3. W. Bibel and E. Eder. Methods and calculi for deduction. In Dov M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificil Intelligence and Logic Programing-Logical Foundations, volume 1, pages 67–182. Oxford University Press, 1993.

    Google Scholar 

  4. G. Bittencourt. In the quest of the missing link. In Proceedings of IJCAI 15, Nagoya, Japan, August 23-29, pages 310–315. Morgan Kaufmann (ISBN 1-55860-480-4), 1997.

    Google Scholar 

  5. G. Bittencourt. Concurrent inference through dual transformation. Logic Journal of the Interest Group in Pure and Applied Logics (IGPL), 6(6):795–834, 1998.

    MATH  MathSciNet  Google Scholar 

  6. G. Bittencourt and I. Tonin. A multi-agent approach to first-order logic. In Proceedings of 8th Portuguese Conference on Artificial Intelligence (EPIA'97), Coimbra, Portugal, October 6-9. Springer-Verlag, 1997.

    Google Scholar 

  7. C.-L. Chang and R.C.-T. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, Computer Science Classics, 1973.

    Google Scholar 

  8. A. C. P. L. da Costa and G. Bittencourt. From a concurrente agent architecture to a autonomous concurrente agent architecture. IJCAI'99 Third RoboCup Workshop, Stockolm, Sweden, July 31-August 1st 1999.

    Google Scholar 

  9. A.C.P.L. da Costa and G. Bittencourt. Dynamic social knowledge: A cooperation strategie for cognitive multi-agent systems. Third International Conference on Multi-Agent Systems (ICMAS'98), pages 415–416, Paris, France, July 2-7 1998. IEEE Computer Society.

    Google Scholar 

  10. E. Eder. Consolution and its relation to resolution. In Proceedings of IJCAI 12, 1991.

    Google Scholar 

  11. N. Eisinger and H.J. Ohlbach. Deduction systems based on resolution. In Dov M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificil Intelligence and Logic Programing-Logical Foundations, volume 1, pages 183–271. Oxford University Press, 1993.

    Google Scholar 

  12. M. Fitting. First-Order Logic and Automated Theorem Proving. Springer-Verlag, New York, 1990.

    Google Scholar 

  13. P. Jackson. Computing prime implicants. In Proceedings of the 10th International Conference on Automatic Deduction, Kaiserslautern, Germany, Springer-Verlag LNAI No. 449, pages 543–557, 1990.

    Google Scholar 

  14. A. Kean and G. Tsiknis. An incremental method for generating prime implicants/implicates. Journal of Symbolic Computation, 9:185–206, 1990.

    Article  MATH  MathSciNet  Google Scholar 

  15. W.V.O. Quine. The problem of simplifying truth functions. American Mathematics Monthly, 59:521–531, 1952.

    Article  MATH  MathSciNet  Google Scholar 

  16. W.V.O. Quine. On cores and prime implicants of truth functions. American Mathematics Monthly, 66:755–760, 1959.

    Article  MATH  MathSciNet  Google Scholar 

  17. J.A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23–41, January 1965.

    Article  MATH  Google Scholar 

  18. J.A. Robinson. Logic and logic programming. Communications of the ACM, 35(3):41–65, March, 1992.

    Article  Google Scholar 

  19. J.R. Slagle, C.L. Chang, and R.C.T. Lee. A new algorithm for generating prime implicants. IEEE Transactions on Computing, 19(4):304–310, 1970.

    Article  MATH  MathSciNet  Google Scholar 

  20. R.M. Smullyan. First Order Logic. Springer-Verlag, 1968.

    Google Scholar 

  21. R. Socher. Optimizing the clausal normal form transformation. Journal of Automated Reasoning, 7(3):325–336, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  22. A.C. Stylianou, G.R. Madey, and R.D. Smith. Selection criteria for expert system shells: A socio-technical framework. Communications of the ACM, 35(10):32–48, October 1992.

    Article  Google Scholar 

  23. P. Tison. Generalized consensus theory and application to the minimization of boolean functions. IEEE Transactions on Computing, 16(4):446–456, 1967.

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Departamento de Automação e Sistemas, Universidade Federal de Santa Catarina, 88040-900, Florianópolis - SC, Brazil

    Guilherme Bittencourt & Isabel Tonin

Authors
  1. Guilherme Bittencourt
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Isabel Tonin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University College London, Gower Street, WC1E 6BT, London, UK

    John A. Campbell

  2. Dept. Algebra, Fac. Educación, Universidad Complutense de Madrid, c/Rector Royo Villanova s/n, 28040, Madrid, Spain

    Eugenio Roanes-Lozano

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bittencourt, G., Tonin, I. (2001). A Proof Strategy Based on a Dual Representation. In: Campbell, J.A., Roanes-Lozano, E. (eds) Artificial Intelligence and Symbolic Computation. AISC 2000. Lecture Notes in Computer Science(), vol 1930. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44990-6_6

Download citation

  • DOI: https://doi.org/10.1007/3-540-44990-6_6

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42071-2

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation