Skip to main content
SpringerLink
Log in

Hierarchic Superposition Revisited

  • Chapter
  • First Online:
Description Logic, Theory Combination, and All That

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

Abstract

Many applications of automated deduction require reasoning in first-order logic modulo background theories, in particular some form of integer arithmetic. A major unsolved research challenge is to design theorem provers that are “reasonably complete” even in the presence of free function symbols ranging into a background theory sort. The hierarchic superposition calculus of Bachmair, Ganzinger, and Waldmann already supports such symbols, but, as we demonstrate, not optimally. This paper aims to rectify the situation by introducing a novel form of clause abstraction, a core component in the hierarchic superposition calculus for transforming clauses into a form needed for internal operation. We argue for the benefits of the resulting calculus and provide two new completeness results: one for the fragment where all background-sorted terms are ground and another one for a special case of linear (integer or rational) arithmetic as a background theory.

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.

    Without loss of generality we assume that there exists a distinct sort for every predicate.

  2. 2.

    This restriction to term-generated interpretations as models is possible since we are only concerned with refutational theorem proving, i. e., with the derivation of a contradiction.

  3. 3.

    To satisfy the technical requirement that all interpretations in \(\mathcal {B}\) are term-generated, we assume that in this case \(\varSigma _\mathrm {B}\) is suitably extended by an infinite set of constants (or by one constant and one unary function symbol) that are not used in any input formula or theory axiom.

  4. 4.

    If \(\varSigma = \varSigma _\mathrm {B}\), this definition coincides with the definition of satisfiability w.r.t. a class of interpretations that was given in Sect. 2. A set N of BG clauses is \(\mathcal {B}\)-satisfiable if and only if some interpretation of \(\mathcal {B}\) is a model of N.

  5. 5.

    In contrast to [5], we include \(\mathrm {GndTh}(\mathcal {B})\) in the definition of sufficient completeness. (This is independent of the abstraction method; it would also have been useful in [5].).

  6. 6.

    Note that J need not be a \(\mathcal {B}\)-interpretation.

  7. 7.

    Target terms are terms that need to be abstracted out; so for efficiency reasons, it is advantageous to keep the number of target terms as small as possible. We will show in Sect. 7 why domain elements may be treated differently from other non-variable terms. On the other hand, all the results in the following sections continue to hold if the restriction that q is not a domain element is dropped (i. e., if domain elements are abstracted out as well). We will make use of this fact in Sect. 11.

  8. 8.

    As in [5], it is possible to strengthen the maximality condition by requiring that there exists some simple ground substitution \(\psi \) such that \((s \not \approx t)\sigma \psi \) is maximal in \((s \not \approx t \,\vee \, C)\sigma \psi \) (and analogously for the other inference rules).

  9. 9.

    In contrast to [5], we include \(\mathrm {GndTh}(\mathcal {B})\) in the redundancy criterion. (This is independent of the abstraction method used; it would also have been useful in [5].).

  10. 10.

    Typically, \(\mathrm {E}_I\) contains two kinds of clauses, namely clauses that evaluate non-constant BG terms, such as \(2 + 3 \approx 5\), and clauses that map parameters to domain elements, such as \(\alpha \approx 4\).

  11. 11.

    In [21], it is required that every ground term that contains a (proper or improper) BG-sorted FG subterm must be larger than any (BG or FG) ground term that does not contain such a subterm.

  12. 12.

    Condition (i) of is obviously satisfied and condition (iii) there is condition (v) of . Instead of condition (ii), inferences are only \(\mathcal {B}\)-satisfiability preserving, which however does not endanger soundness.

  13. 13.

    A KBO with appropriate weights can be used for \(\succ _{\mathrm {fin}}\).

  14. 14.

    Any pair of terms s, t is related in all clauses of an equivalence class by either a literal \(s \approx t\), or \(s \not \approx t\), or \(s <_n t\) for some n, or \(t <_n s\) for some n, or no literal at all, so there are five possibilities per unordered pair of terms.

  15. 15.

    Beagle is available at https://bitbucket.org/peba123/beagle. The distribution includes the (Scala) source code and a ready-to-run Java jar-file.

  16. 16.

    http://tptp.org.

  17. 17.

    SWW583=2.p, SWW594=2.p, SWW607=2.p, SWW626=2.p, SWW653=2.p and SWW657=2.p.

  18. 18.

    At the time of this writing, there are only four provers (including Beagle) registered with the TPTP web infrastructure that can solve these problems. Hence the rating 0.75.

  19. 19.

    http://tptp.cs.miami.edu/~tptp/CASC/J9/.

References

  1. Althaus, E., Kruglov, E., Weidenbach, C.: Superposition modulo linear arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 84–99. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04222-5_5

    Chapter  Google Scholar 

  2. Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1), 4 (2009)

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  4. Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Handbook of Automated Reasoning. North Holland (2001)

    Google Scholar 

  5. Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput 5, 193–212 (1994)

    Article  MathSciNet  Google Scholar 

  6. Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_14

    Chapter  Google Scholar 

  7. Baumgartner, P., Bax, J., Waldmann, U.: Beagle – a hierarchic superposition theorem prover. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 367–377. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_25

    Chapter  Google Scholar 

  8. Baumgartner, P., Fuchs, A., Tinelli, C.: \(\cal{ME}\)(LIA) - model evolution with linear integer arithmetic constraints. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 258–273. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89439-1_19

    Chapter  Google Scholar 

  9. Baumgartner, P., Tinelli, C.: Model evolution with equality modulo built-in theories. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 85–100. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22438-6_9

    Chapter  Google Scholar 

  10. Baumgartner, P., Waldmann, U.: Hierarchic superposition: completeness without compactness. In: Košta, M., Sturm, T. (eds.), Fifth International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2013, pp. 8–12, Nanning, China (2013)

    Google Scholar 

  11. Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 39–57. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_3

    Chapter  Google Scholar 

  12. Baumgartner, P., Waldmann, U.: Hierarchic superposition revisited (2019). http://arxiv.org/abs/1904.03776

  13. Bonacina, M.P., Lynch, C., de Moura, L.M.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reason. 47(2), 161–189 (2011)

    Article  MathSciNet  Google Scholar 

  14. de Moura, L., Bjørner, N.: Engineering DPLL(T) + saturation. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 475–490. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71070-7_40

    Chapter  Google Scholar 

  15. Dickson, L.E.: Finiteness of the odd perfect and primitive abundant numbers with \(n\) distinct prime factors. Am. J. Math. 35(4), 413–422 (1913)

    Article  MathSciNet  Google Scholar 

  16. Ganzinger, H., Korovin, K.: Theory instantiation. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 497–511. Springer, Heidelberg (2006). https://doi.org/10.1007/11916277_34

    Chapter  Google Scholar 

  17. Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 167–182. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73595-3_12

    Chapter  Google Scholar 

  18. Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306–320. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_25

    Chapter  Google Scholar 

  19. Korovin, K., Voronkov, A.: Integrating linear arithmetic into superposition calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 223–237. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74915-8_19

    Chapter  Google Scholar 

  20. Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_1

    Chapter  Google Scholar 

  21. Kruglov, E.: Superposition modulo theory. Doctoral dissertation, Universität des Saarlandes, Saarbrücken, October 2013

    Google Scholar 

  22. Kruglov, E., Weidenbach, C.: Superposition decides the first-order logic fragment over ground theories. Math. Comput. Sci. 6, 427–456 (2012)

    Article  MathSciNet  Google Scholar 

  23. Nieuwenhuis, R.: First-order completion techniques. Technical report, Universidad Politécnica de Cataluña, Dept. Lenguajes y Sistemas Informáticos (1991)

    Google Scholar 

  24. Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006)

    Article  MathSciNet  Google Scholar 

  25. Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Handbook of Automated Reasoning, pp. 371–443. Elsevier and MIT Press (2001)

    Google Scholar 

  26. Rümmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 274–289. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89439-1_20

    Chapter  MATH  Google Scholar 

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

  28. Walther, C.: Many-sorted unification. J. ACM 35(1), 1–17 (1988)

    Article  MathSciNet  Google Scholar 

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

Author information

Authors and Affiliations

  1. Data61/CSIRO, ANU Computer Science and Information Technology (CSIT), Acton, Australia

    Peter Baumgartner

  2. Max-Planck-Institut für Informatik, Saarbrücken, Germany

    Uwe Waldmann

Authors
  1. Peter Baumgartner
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Uwe Waldmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Peter Baumgartner or Uwe Waldmann .

Editor information

Editors and Affiliations

  1. University of Bremen, Bremen, Germany

    Carsten Lutz

  2. University of Manchester, Manchester, UK

    Uli Sattler

  3. University of Iowa, Iowa City, IA, USA

    Cesare Tinelli

  4. TU Dresden, Dresden, Germany

    Anni-Yasmin Turhan

  5. University of Liverpool, Liverpool, UK

    Frank Wolter

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Baumgartner, P., Waldmann, U. (2019). Hierarchic Superposition Revisited. In: Lutz, C., Sattler, U., Tinelli, C., Turhan, AY., Wolter, F. (eds) Description Logic, Theory Combination, and All That. Lecture Notes in Computer Science(), vol 11560. Springer, Cham. https://doi.org/10.1007/978-3-030-22102-7_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-22102-7_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-22101-0

  • Online ISBN: 978-3-030-22102-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation