Skip to main content
Top

2018 | OriginalPaper | Chapter

Efficient Encodings of First-Order Horn Formulas in Equational Logic

Authors : Koen Claessen, Nicholas Smallbone

Published in: Automated Reasoning

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
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
Since we are working with clauses, free variables are universally quantified.
 
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
Also, no special support for tuples is needed in the theorem prover.
 
Literature
2.
go back to reference Bachmair, L., Dershowitz, N.: Equational inference, canonical proofs, and proof orderings. J. ACM 41(2), 236–276 (1994)MathSciNetCrossRef Bachmair, L., Dershowitz, N.: Equational inference, canonical proofs, and proof orderings. J. ACM 41(2), 236–276 (1994)MathSciNetCrossRef
3.
go back to reference Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Rewriting Techniques, pp. 1–30. Elsevier (1989) Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Rewriting Techniques, pp. 1–30. Elsevier (1989)
4.
go back to reference Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4, 217–247 (1994)MathSciNetCrossRef Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4, 217–247 (1994)MathSciNetCrossRef
6.
go back to reference Bonacina, M.P., Hsiang, J.: Towards a foundation of completion procedures as semidecision procedures. Theor. Comput. Sci. 146(1–2), 199–242 (1995)MathSciNetCrossRef Bonacina, M.P., Hsiang, J.: Towards a foundation of completion procedures as semidecision procedures. Theor. Comput. Sci. 146(1–2), 199–242 (1995)MathSciNetCrossRef
9.
go back to reference 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) 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)
11.
go back to reference Hsiang, J.: Rewrite method for theorem proving in first order theory with equality. J. Symb. Comput. 3, 133–151 (1987)MathSciNetCrossRef Hsiang, J.: Rewrite method for theorem proving in first order theory with equality. J. Symb. Comput. 3, 133–151 (1987)MathSciNetCrossRef
12.
go back to reference Kapur, D., Narendran, P.: An equational approach to theorem proving in first-order predicate calculus. SIGSOFT Softw. Eng. Notes 10(4), 63–66 (1985)CrossRef Kapur, D., Narendran, P.: An equational approach to theorem proving in first-order predicate calculus. SIGSOFT Softw. Eng. Notes 10(4), 63–66 (1985)CrossRef
14.
go back to reference Löchner, B., Hillenbrand, T.: A phytography of WALDMEISTER. AI Commun. 15(2, 3), 127–133 (2002)MATH Löchner, B., Hillenbrand, T.: A phytography of WALDMEISTER. AI Commun. 15(2, 3), 127–133 (2002)MATH
18.
21.
go back to reference 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)MathSciNetCrossRef 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)MathSciNetCrossRef
Metadata
Title
Efficient Encodings of First-Order Horn Formulas in Equational Logic
Authors
Koen Claessen
Nicholas Smallbone
Copyright Year
2018
DOI
https://doi.org/10.1007/978-3-319-94205-6_26

Premium Partner