Replication Package for Article: FPL: Fast Presburger Arithmetic through Transprecision

2021 ◽  
Author(s):  
Arjun Pitchanathan ◽  
Christian Ulmann ◽  
Michel Weber ◽  
Torsten Hoefler ◽  
Tobias Grosser
Keyword(s):  
Presburger Arithmetic

scholarly journals Periodic behavior in families of numerical and affine semigroups via parametric Presburger arithmetic

2021 ◽  
Vol 102 (2) ◽  
pp. 340-356
Author(s):  
Tristram Bogart ◽  
John Goodrick ◽  
Kevin Woods
Keyword(s):  
Periodic Behavior ◽  
Presburger Arithmetic ◽  
Affine Semigroups

Completeness of Presburger Arithmetic

2020 ◽  
pp. 137-149
Author(s):  
Lorenz Halbeisen ◽  
Regula Krapf
Keyword(s):  
Presburger Arithmetic

scholarly journals Short Presburger Arithmetic Is Hard

2019 ◽  
pp. STOC17-1-STOC17-30
Author(s):  
Danny Nguyen ◽  
Igor Pak
Keyword(s):  
Presburger Arithmetic

scholarly journals An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic

2010 ◽  
pp. 384-399 ◽  
Author(s):  
Angelo Brillout ◽  
Daniel Kroening ◽  
Philipp Rümmer ◽  
Thomas Wahl
Keyword(s):  
Sequent Calculus ◽  
Presburger Arithmetic

scholarly journals PRESBURGER ARITHMETIC, RATIONAL GENERATING FUNCTIONS, AND QUASI-POLYNOMIALS

2015 ◽  
Vol 80 (2) ◽  
pp. 433-449 ◽  
Author(s):  
KEVIN WOODS
Keyword(s):  
Generating Functions ◽  
Counting Function ◽  
Order Theory ◽  
Characteristic Functions ◽  
Presburger Arithmetic ◽  
First Order ◽  
First Order Theory ◽  
Rational Generating Function ◽  
Rational Generating Functions

AbstractPresburger arithmetic is the first-order theory of the natural numbers with addition (but no multiplication). We characterize sets that can be defined by a Presburger formula as exactly the sets whose characteristic functions can be represented by rational generating functions; a geometric characterization of such sets is also given. In addition, ifp= (p1, . . . ,pn) are a subset of the free variables in a Presburger formula, we can define a counting functiong(p) to be the number of solutions to the formula, for a givenp. We show that every counting function obtained in this way may be represented as, equivalently, either a piecewise quasi-polynomial or a rational generating function. Finally, we translate known computational complexity results into this setting and discuss open directions.

Sign in / Sign up

Export Citation Format

Share Document