Skip to main content
SpringerLink
Log in

Efficient Encodings of First-Order Horn Formulas in Equational Logic

  • Conference paper
  • First Online:
Automated Reasoning (IJCAR 2018)

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

Included in the following conference series:

Abstract

We present several translations from first-order Horn formulas to equational logic. The goal of these translations is to allow equational theorem provers to efficiently reason about non-equational problems. Using these translations we were able to solve 37 problems of rating 1.0 (i.e. which had not previously been automatically solved) from the TPTP.

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

Notes

  1. 1.

    Really we mean \(\mathcal {M}_0^\sigma (s) \ne \mathcal {M}_0^\sigma (t)\), but we leave out the heavy notation in this proof.

  2. 2.

    Since we are working with clauses, free variables are universally quantified.

  3. 3.

    The arguments \(x_1,\ldots ,x_n\) help to unambiguously identify u and v. Without them, this interpretation of \(\textsf {fresh}_i\) would not make sense and the encoding would be unsound.

  4. 4.

    Also, no special support for tuples is needed in the theorem prover.

References

  1. Bachmair, L., Dershowitz, N.: Critical pair criteria for completion. J. Symb. Comput. 6(1), 1–18 (1988). https://doi.org/10.1016/S0747-7171(88)80018-X

    Article  MathSciNet  MATH  Google Scholar 

  2. Bachmair, L., Dershowitz, N.: Equational inference, canonical proofs, and proof orderings. J. ACM 41(2), 236–276 (1994)

    Article  MathSciNet  Google Scholar 

  3. Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Rewriting Techniques, pp. 1–30. Elsevier (1989)

    Google Scholar 

  4. Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4, 217–247 (1994)

    Article  MathSciNet  Google Scholar 

  5. Bonacina, M.P., Dershowitz, N.: Abstract canonical inference. ACM Trans. Comput. Logic 8(1) (2007). http://doi.acm.org/10.1145/1182613.1182619

    Article  MathSciNet  Google Scholar 

  6. Bonacina, M.P., Hsiang, J.: Towards a foundation of completion procedures as semidecision procedures. Theor. Comput. Sci. 146(1–2), 199–242 (1995)

    Article  MathSciNet  Google Scholar 

  7. Burris, S.: Discriminator varieties and symbolic computation. J. Symb. Comput. 13(2), 175–207 (1992). https://doi.org/10.1016/S0747-7171(08)80089-2

    Article  MathSciNet  MATH  Google Scholar 

  8. Claessen, K., Lillieström, A., Smallbone, N.: Sort it out with monotonicity. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 207–221. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22438-6_17

    Chapter  Google Scholar 

  9. Claessen, K., Sörensson, N.: New techniques that improve MACE-style finite model finding. In: Proceedings of the CADE-19 Workshop: Model Computation-Principles, Algorithms, Applications, pp. 11–27. Citeseer (2003)

    Google Scholar 

  10. Dershowitz, N.: A maximal-literal unit strategy for Horn clauses. In: Kaplan, S., Okada, M. (eds.) CTRS 1990. LNCS, vol. 516, pp. 14–25. Springer, Heidelberg (1991). https://doi.org/10.1007/3-540-54317-1_78

    Chapter  Google Scholar 

  11. Hsiang, J.: Rewrite method for theorem proving in first order theory with equality. J. Symb. Comput. 3, 133–151 (1987)

    Article  MathSciNet  Google Scholar 

  12. Kapur, D., Narendran, P.: An equational approach to theorem proving in first-order predicate calculus. SIGSOFT Softw. Eng. Notes 10(4), 63–66 (1985)

    Article  Google Scholar 

  13. Kounalis, E., Rusinowitch, M.: On word problems in Horn theories. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 527–537. Springer, Heidelberg (1988). https://doi.org/10.1007/BFb0012854

    Chapter  Google Scholar 

  14. Löchner, B., Hillenbrand, T.: A phytography of WALDMEISTER. AI Commun. 15(2, 3), 127–133 (2002)

    MATH  Google Scholar 

  15. Martin, U., Nipkow, T.: Ordered rewriting and confluence. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 366–380. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52885-7_100

    Chapter  Google Scholar 

  16. Mckenzie, R.: On spectra, and the negative solution of the decision problem for identities having a finite nontrivial model. J. Symb. Log. 40(2), 186–196 (1975). https://projecteuclid.org:443/euclid.jsl/1183739380

    Article  MathSciNet  Google Scholar 

  17. Nieuwenhuis, R., Orejas, F.: Clausal rewriting. In: Kaplan, S., Okada, M. (eds.) CTRS 1990. LNCS, vol. 516, pp. 246–258. Springer, Heidelberg (1991). https://doi.org/10.1007/3-540-54317-1_95

    Chapter  Google Scholar 

  18. Rusinowitch, M.: Theorem-proving with resolution and superposition. J. Symb. Comput. 11(1–2), 21–49 (1991)

    Article  MathSciNet  Google Scholar 

  19. Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 735–743. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-45221-5_49

    Chapter  Google Scholar 

  20. Smallbone, N.: Twee, an equational theorem prover (2017). http://nick8325.github.io/twee/

  21. Sutcliffe, G.: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483–502 (2017)

    Article  MathSciNet  Google Scholar 

  22. Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 140–145. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02959-2_10

    Chapter  Google Scholar 

Download references

Acknowledgements

This work was supported by the Swedish Research Council (VR) grant 2016-06204, Systematic testing of cyber-physical systems (SyTeC).

Author information

Authors and Affiliations

  1. Chalmers University of Technology, Gothenburg, Sweden

    Koen Claessen & Nicholas Smallbone

Authors
  1. Koen Claessen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nicholas Smallbone
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nicholas Smallbone .

Editor information

Editors and Affiliations

  1. Université de Lorraine, Vandoeuvre-lès-Nancy, France

    Didier Galmiche

  2. Baden-Wuerttemberg Cooperative State University, Stuttgart, Germany

    Stephan Schulz

  3. University of Trento, Trento, Italy

    Roberto Sebastiani

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Claessen, K., Smallbone, N. (2018). Efficient Encodings of First-Order Horn Formulas in Equational Logic. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds) Automated Reasoning. IJCAR 2018. Lecture Notes in Computer Science(), vol 10900. Springer, Cham. https://doi.org/10.1007/978-3-319-94205-6_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-94205-6_26

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-94204-9

  • Online ISBN: 978-3-319-94205-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation