Inference Systems for Logical Algorithms | SpringerLink
Skip to main content
Springer Nature Link
Log in

Inference Systems for Logical Algorithms

  • Conference paper
FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2005)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3821))

Abstract

Logical algorithms are defined in terms of individual computation steps that are based on logical inferences. We present a uniform framework for formalizing logical algorithms based on inference systems. We present inference systems for algorithms such as resolution, the Davis–Putnam–Logemann–Loveland procedure, equivalence and congruence closure, and satisfiability modulo theories. The paper is intended as an introduction to the use of inference systems for studying logical algorithms.

This research was supported NSF Grants CCR-ITR-0326540 and CCR-ITR-0325808.

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.

Similar content being viewed by others

References

  1. Bledsoe, W.W.: Non-resolution theorem proving. Artificial Intelligence 9, 1–36 (1977)

    Article  MATH  MathSciNet  Google Scholar 

  2. Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, New York (1979)

    MATH  Google Scholar 

  3. Bachmair, L., Tiwari, A., Vigneron, L.: Abstract congruence closure. Journal of Automated Reasoning 31(2), 129–168 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  4. Buchberger, B.: A theoretical basis for the reduction of polynomials to canonical forms. ACM SIGSAM Bulletin 10(3), 19–29 (1976)

    Article  MathSciNet  Google Scholar 

  5. Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Englewood Cliffs (1986)

    Google Scholar 

  6. Cohen, J.: A view of the origins and development of prolog. Communications of the ACM 31(1), 26–36 (1988)

    Article  Google Scholar 

  7. Davis, M.: A computer program for Presburger’s algorithm. In: Summaries of Talks Presented at the Summer Institute for Symbolic Logic (1957); Reprinted in Siekmann and Wrightson [SW83], pp. 41–48

    Google Scholar 

  8. de Bruijn, N.G.: A survey of the project Automath. In: To, H.B. (ed.) Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 589–606. Academic Press, London (1980)

    Google Scholar 

  9. Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM 5(7), 394–397 (1983); Reprinted in Siekmann and Wrightson [SW83], pp. 267–270 (1983)

    Article  MathSciNet  Google Scholar 

  10. de Moura, L., Rueß, H., Shankar, N.: Justifying equality. In: Proceedings of PDPAR 2004 (2004)

    Google Scholar 

  11. Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7, 201–215 (1960)

    Article  MATH  MathSciNet  Google Scholar 

  12. Davis, M., Putnam, H.: A computing procedure for quantification theory. JACM 7(3), 201–215 (1960)

    Article  MATH  MathSciNet  Google Scholar 

  13. Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpressions problem. Journal of the ACM 27(4), 758–771 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  14. Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

  15. Gordon, M., Milner, R., Wadsworth, C.: Edinburgh LCF: A Mechanized Logic of Computation. In: Gordon, M., Wadsworth, C.P., Milner, R. (eds.) Edinburgh LCF. LNCS, vol. 78, Springer, Heidelberg (1979)

    Google Scholar 

  16. Ganzinger, H., Rueß, H., Shankar, N.: Modularity and refinement in inference systems. Technical Report CSL-SRI-04-02, SRI International, Computer Science Laboratory, 333 Ravenswood Ave, Menlo Park, CA, 94025 (January 2004), (revised August 2004)

    Google Scholar 

  17. Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265–269. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  18. Kapur, D.: hostak’s congruence closure as completion. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 23–37. Springer, Heidelberg (1997)

    Google Scholar 

  19. Knuth, D.E., Bendix, P.: imple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebras, pp. 263–297. Pergamon Press, Oxford (1970)

    Google Scholar 

  20. Kleene, S.C.: Introduction to Metamathematics. North-Holland, Amsterdam (1952)

    MATH  Google Scholar 

  21. Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. In: Advances in Formal Methods., vol. 3, Kluwer, Dordrecht (2000)

    Google Scholar 

  22. Kozen, D.: Complexity of finitely presented algebras. In: Conference Record of the Ninth Annual ACM Symposium on Theory of Computing, Boulder, Colorado, May 2–4, pp. 164–177 (1977)

    Google Scholar 

  23. Luo, Z., Pollack, R.: The LEGO proof development system: A user’s manual. Technical Report ECS-LFCS-92-211, University of Edinburgh (1992)

    Google Scholar 

  24. McCarthy, J.: Computer programs for checking mathematical proofs. In Recursive Function Theory. In: Proceedings of a Symposium in Pure Mathematics, vol. V, pp. 219–227. American Mathematical Society, Providence (1962)

    Google Scholar 

  25. McCune, W.W.: Solution of the Robbins problem, Available from ftp://info.mcs.anl.gov/pub/Otter/www-misc/robbins-jar-submitted.ps.gz (1997)

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

    Article  MATH  Google Scholar 

  27. Nieuwenhuis, R., Oliveras, A.: Proof-Producing Congruence Closure. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 453–468. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  28. Newell, A., Shaw, J.C., Simon, H.A.: Empirical explorations with the logic theory machine: A case study in heuristics. In: Proc. West. Joint Comp. Conf., pp. 218–239 (1957), Reprinted in Siekmann and Wrightson [SW83], pp. 49–73 (1983)

    Google Scholar 

  29. Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS, vol. 828. Springer, Heidelberg (1994)

    MATH  Google Scholar 

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

    Article  MATH  Google Scholar 

  31. Robinson, J.A.: Automatic deduction with hyper-resolution. International Journal of Computational Mathematics 1, 227–234 (1965)

    MATH  Google Scholar 

  32. Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier Science, Amsterdam (2001)

    MATH  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  34. Shostak, R.E.: A practical decision procedure for arithmetic with function symbols. Journal of the ACM 26(2), 351–360 (1979)

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  36. Sutcliffe, G., Suttner, C.B.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning 21(2), 177–203 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  37. Siekmann, J., Wrightson, G. (eds.): Automation of Reasoning: Classical Papers on Computational Logic. Springer, Heidelberg (1983)

    Google Scholar 

  38. Coq Development Team. The Coq proof assistant reference manual, version 8.0. Technical report, INRIA, Rocquencourt, France (January 2005)

    Google Scholar 

  39. Wos, L., Robinson, G.A., Carson, D.: Efficiency and completeness of the set of support strategy in theorem proving. Journal of the ACM 12(4), 536–541 (1965)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Laboratory, SRI International, Menlo Park, CA, 94025, USA

    Natarajan Shankar

Authors
  1. Natarajan Shankar
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. National Institute of Advanced Studies, Indian Institute of Science Campus, 560012, Bangalore, India

    Sundar Sarukkai

  2. Department of Comp. Sc. & Engg., Indian Institute of Technology Delhi, 110016, New Delhi, India

    Sandeep Sen

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Shankar, N. (2005). Inference Systems for Logical Algorithms. In: Sarukkai, S., Sen, S. (eds) FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2005. Lecture Notes in Computer Science, vol 3821. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11590156_4

Download citation

  • DOI: https://doi.org/10.1007/11590156_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-30495-1

  • Online ISBN: 978-3-540-32419-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation