Cover Image

Quantifier Elimination and Craig Interpolation, Quantitatively

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Batz, Kevin, Katoen, Joost-Pieter, Orhan, Nora
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
by: Batz, Kevin, et al.
Published: (2025)

Towards Concurrent Quantitative Separation Logic
by: Fesefeldt, Ira, et al.
Published: (2022)

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
by: Klinkenberg, Lutz, et al.
Published: (2023)

Verifying Sampling Algorithms via Distributional Invariants
by: Zilken, Daniel, et al.
Published: (2025)

Unknown Biases and Timing Constraints in Timed Automata
by: Haase, Darion, et al.
Published: (2024)

Bidirectional Interpolation for the Lambda-Calculus -- Revisiting and Formalising Craig-Čubrić Interpolation
by: Bertrand, Meven Lennon, et al.
Published: (2026)

J-P: MDP. FP. PP.: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs (Technical Report)
by: Batz, Kevin, et al.
Published: (2024)

Model Checking Temporal Properties of Recursive Probabilistic Programs
by: Winkler, Tobias, et al.
Published: (2021)

Compositional Reasoning for Probabilistic Automata with Uncertainty
by: Mertens, Hannah, et al.
Published: (2026)

Generalized Parameter Lifting: Finer Abstractions for Parametric Markov Chains
by: Heck, Linus, et al.
Published: (2025)

Axe 'Em: Eliminating Spurious States with Induction Axioms
by: Elad, Neta, et al.
Published: (2024)

Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
by: Accattoli, Beniamino
Published: (2022)

Compositional Reasoning for Parametric Probabilistic Automata
by: Mertens, Hannah, et al.
Published: (2025)

Bayesian Inference in Quantum Programs
by: Gehnen, Christina, et al.
Published: (2025)

Craig Interpolation in Program Verification
by: Rümmer, Philipp
Published: (2026)

PolyQEnt: A Polynomial Quantified Entailment Solver
by: Chatterjee, Krishnendu, et al.
Published: (2024)

Universal Proof Theory: Semi-analytic Rules and Craig Interpolation
by: Tabatabai, Amirhossein Akbar, et al.
Published: (2018)

Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems
by: Ahrens, Emma, et al.
Published: (2025)

Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains
by: Mertens, Hannah, et al.
Published: (2024)

Zippy -- Generic White-Box Proof Search with Zippers
by: Kappelmann, Kevin
Published: (2025)

Craig Interpolation for Decidable First-Order Fragments
by: Cate, Balder ten, et al.
Published: (2023)

Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains
by: Spork, Timm, et al.
Published: (2025)

A Spectrum of Approximate Probabilistic Bisimulations
by: Spork, Timm, et al.
Published: (2024)

Verification of Robust Multi-Agent Systems
by: Berthon, Raphaël, et al.
Published: (2026)

Natural Strategic Ability in Stochastic Multi-Agent Systems
by: Berthon, Raphaël, et al.
Published: (2024)

The Lambda Calculus is Quantifiable
by: Maestracci, Valentin, et al.
Published: (2024)

Probabilistic Model Checking Taken by Storm
by: Volk, Matthias, et al.
Published: (2026)

Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)
by: Lichtner, Kilian, et al.
Published: (2025)

Craig-Lyndon Interpolation for the Logic of Here and There with a Variation of Mints' Sequent System
by: Wernhard, Christoph
Published: (2026)

Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets
by: Wu, Hao, et al.
Published: (2024)

SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits
by: Yu, Nengkun, et al.
Published: (2025)

Kleene algebra with commutativity conditions is undecidable
by: de Amorim, Arthur Azevedo, et al.
Published: (2024)

Interpolation and Quantifiers in Ortholattices
by: Guilloud, Simon, et al.
Published: (2025)

On Symbol Elimination and Uniform Interpolation in Theory Extensions
by: Sofronie-Stokkermans, Viorica
Published: (2025)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
by: Kaye, George
Published: (2025)

Impredicativity in Linear Dependent Type Theory
by: Speight, Sam, et al.
Published: (2026)

A Probabilistic Choreography Language for PRISM
by: Carbone, Marco, et al.
Published: (2025)

Denotational Semantics for Probabilistic and Concurrent Programs
by: Zilberstein, Noam, et al.
Published: (2025)

Positive Sharing and Abstract Machines
by: Accattoli, Beniamino, et al.
Published: (2025)

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
by: Grandury, Marcos, et al.
Published: (2025)