An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.

An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.

Бусад хувилбаруудыг харуулах (1)

Craig interpolation has become a versatile tool in formal verification, used for instance to generate program assertions that serve as candidates for loop invariants. In this paper, we consider Craig interpolation for quantifier-free Presburger arithmetic (QFPA). Until recently, quantifier eliminati...

Бүрэн тодорхойлолт

Номзүйн дэлгэрэнгүй
Үндсэн зохиолчид:	Brillout, A, Kroening, D, Rümmer, P, Wahl, T
Формат:	Journal article
Хэл сонгох:	English
Хэвлэсэн:	2011

Ижил төстэй зүйлс

An interpolating sequent calculus for quantifier-free Presburger arithmetic
-н: Brillout, A, зэрэг
Хэвлэсэн: (2011)

Beyond quantifier-free interpolation in extensions of presburger arithmetic
-н: Brillout, A, зэрэг
Хэвлэсэн: (2011)

Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-Complete
-н: Kuncak, Viktor
Хэвлэсэн: (2007)

Quantifier elimination for counting extensions of Presburger arithmetic
-н: Chistikov, D, зэрэг
Хэвлэсэн: (2022)

Abstraction−based Satisfiability Solving of Presburger Arithmetic
-н: Kroening, D, зэрэг
Хэвлэсэн: (2004)

The complexity of Presburger arithmetic with power or powers
-н: Benedikt, M, зэрэг
Хэвлэсэн: (2023)

On the decidability of Presburger arithmetic expanded with powers
-н: Karimov, T, зэрэг
Хэвлэсэн: (2025)

Super-exponential Complexity of Presburger Arithmetic
-н: Fischer, Michael J., зэрэг
Хэвлэсэн: (2023)

Algebra and sequent calculus for epistemic actions
-н: Baltag, A, зэрэг
Хэвлэсэн: (2005)

A Cut−Free Sequent Calculus for Algebraic Dynamic Epistemic Logic
-н: Dyckhoff, R, зэрэг
Хэвлэсэн: (2010)

Implementation of a cut−free sequent calculus for logics with adjoint modalities
-н: Kriener, M, зэрэг
Хэвлэсэн: (2009)

An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic
-н: Kuncak, Viktor, зэрэг
Хэвлэсэн: (2005)

Extensions of Presburger arithmetic and model checking one-counter automata
-н: Lechner, A
Хэвлэсэн: (2016)

Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures
-н: Tiu, A, зэрэг
Хэвлэсэн: (2012)

A labelled sequent calculus for BBI : proof theory and proof search
-н: Hóu, Zhé, зэрэг
Хэвлэсэн: (2020)

Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests
-н: Haase, C, зэрэг
Хэвлэсэн: (2019)

Stoic sequent logic and proof theory
-н: Bobzien, S
Хэвлэсэн: (2019)

Enrichments of Boolean algebras by Presburger predicates
-н: Derakhshan, J, зэрэг
Хэвлэсэн: (2017)

The GHZ/W−calculus contains rational arithmetic
-н: Coecke, B, зэрэг
Хэвлэсэн: (2011)

The GHZ/W−calculus contains rational arithmetic
-н: Coecke, B, зэрэг
Хэвлэсэн: (2010)

Mutation-based test case generation for simulink models
-н: Brillout, A, зэрэг
Хэвлэсэн: (2010)

Preface: Special Issue on Interpolation
-н: Kroening, D, зэрэг
Хэвлэсэн: (2016)

Interpolant Strength
-н: D'Silva, V, зэрэг
Хэвлэсэн: (2010)

Lifting Propositional Interpolants to the Word−Level
-н: Kroening, D, зэрэг
Хэвлэсэн: (2007)

Stochastic And Modified Sequent Peak Algorithm For Reservoir Planning Analysis Considering Performance Indices
-н: Oskoui, Issa Saket
Хэвлэсэн: (2016)

Restructuring Resolution Refutations for Interpolation
-н: D'Silva, V, зэрэг
Хэвлэсэн: (2008)

Coverage in interpolation-based model checking
-н: Chockler, H, зэрэг
Хэвлэсэн: (2010)

Model theory of finite-by-Presburger Abelian groups and finite extensions of $p$-adic fields
-н: Derakhshan, J, зэрэг
Хэвлэсэн: (2016)

Multilevel interpolation of divergence-free vector fields
-н: Gillow, K, зэрэг
Хэвлэсэн: (2016)

An interpolating decision procedure for transitive relations with uninterpreted functions
-н: Kroening, D, зэрэг
Хэвлэсэн: (2009)

An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions
-н: Kroening, D, зэрэг
Хэвлэсэн: (2010)

Numerical calculus: approximations, interpolation, finite differences, numerical integration and curve fitting
-н: 316473 Milne, William Edmund
Хэвлэсэн: (1949)

Approximation Refinement for Interpolation−Based Model Checking
-н: D'Silva, V, зэрэг
Хэвлэсэн: (2008)

Approximation Refinement for Interpolation−Based Model Checking
-н: D'Silva, V, зэрэг
Хэвлэсэн: (2008)

Computing mutation coverage in interpolation-based model checking
-н: Chockler, H, зэрэг
Хэвлэсэн: (2012)

Deciding Bit−Vector Arithmetic with Abstraction
-н: Bryant, R, зэрэг
Хэвлэсэн: (2007)

Quantifying the consistency and rheology of liquid foods using fractional calculus
-н: Engmann, Jan, зэрэг
Хэвлэсэн: (2018)

Automatic analysis of DMA races using model checking and k-induction.
-н: Donaldson, A, зэрэг
Хэвлэсэн: (2011)

Automatic analysis of DMA races using model checking and k-induction
-н: Donaldson, A, зэрэг
Хэвлэсэн: (2011)

Arithmetic /
-н: 435610 Godfrey, Charles, 1873-1934, зэрэг
Хэвлэсэн: (1927)