Princess

Theorem Proving in First-Order Logic modulo Linear Integer Arithmetic. Princess is a theorem prover for Presburger arithmetic with uninterpreted predicates. This means that Princess can reason about problems in integer arithmetic without multiplication (only multiplication with integer literals is allowed), augmented with predicates that can be axiomatised arbitrarily. Such problems can contain arbitrary quantifiers to express that some formula is supposed to hold for all or for some integers.


References in zbMATH (referenced in 15 articles )

Showing results 1 to 15 of 15.
Sorted by year (citations)

  1. Christ, Jürgen; Hoenicke, Jochen: Proof tree preserving tree interpolation (2016)
  2. Kroening, Daniel (ed.); Rybalchenko, Andrey (ed.): Preface: Special issue on interpolation (2016)
  3. Leroux, Jér^ome; Rümmer, Philipp; Subotić, Pavle: Guiding Craig interpolation with domain-specific abstractions (2016)
  4. Totla, Nishant; Wies, Thomas: Complete instantiation-based interpolation (2016)
  5. Bonacina, Maria Paola; Johansson, Moa: Interpolation systems for ground proofs in automated deduction: a survey (2015)
  6. Rümmer, Philipp; Hojjat, Hossein; Kuncak, Viktor: On recursion-free Horn clauses and Craig interpolation (2015)
  7. Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: An extension of lazy abstraction with interpolation for programs with arrays (2014)
  8. Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: Lazy abstraction with interpolants for arrays (2012)
  9. Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio: Quantifier-free interpolation of a theory of arrays (2012)
  10. Griggio, Alberto; Le, Thi Thieu Hoa; Sebastiani, Roberto: Efficient interpolant generation in satisfiability modulo linear integer arithmetic (2012)
  11. Hojjat, Hossein; Konečný, Filip; Garnier, Florent; Iosif, Radu; Kuncak, Viktor; Rümmer, Philipp: A verification toolkit for numerical transition systems. Tool paper (2012)
  12. Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas: Beyond quantifier-free interpolation in extensions of Presburger arithmetic (2011)
  13. Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas: An interpolating sequent calculus for quantifier-free Presburger arithmetic (2011)
  14. Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio: Rewriting-based quantifier-free interpolation for a theory of arrays (2011)
  15. Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio: A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints (2011)


Further publications can be found at: http://www.philipp.ruemmer.org/peer.shtml