Imagen de Portada

A Deductive Refinement Calculus for Differential-Algebraic Programs

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Hellwig, Jonathan, Qian, Long, Platzer, André
Formato:	Preprint
Publicado:	2026
Materias:	Logic in Computer Science
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

A Real-Analytic Approach to Differential-Algebraic Dynamic Logic
por: Hellwig, Jonathan, et al.
Publicado: (2025)

Differential Elimination and Algebraic Invariants of Polynomial Dynamical Systems
por: Simmons, William, et al.
Publicado: (2023)

CESAR: Control Envelope Synthesis via Angelic Refinements
por: Kabra, Aditi, et al.
Publicado: (2023)

Uniform Substitution for Differential Refinement Logic
por: Prebet, Enguerrand, et al.
Publicado: (2024)

From Zonotopes to Proof Certificates: A Formal Pipeline for Safe Control Envelopes
por: Hellwig, Jonathan, et al.
Publicado: (2025)

Complete Dynamic Logic of Communicating Hybrid Programs
por: Brieger, Marvin, et al.
Publicado: (2024)

Approximate Axiomatization for Differentially-Defined Functions
por: Platzer, André, et al.
Publicado: (2025)

Practical Deductive Verification of OCaml Programs (Extended Version)
por: Pereira, Mário
Publicado: (2024)

Heterogeneous Dynamic Logic: Provability Modulo Program Theories
por: Teuber, Samuel, et al.
Publicado: (2025)

LLM-Powered Automatic Theorem Proving and Synthesis for Hybrid Systems and Game
por: Kabra, Aditi, et al.
Publicado: (2026)

Context, Judgement, Deduction
por: Coraglia, Greta, et al.
Publicado: (2021)

Deductive Systems for Logic Programs with Counting
por: Fandinno, Jorge, et al.
Publicado: (2025)

Cut-free Deductive System for Continuous Intuitionistic Logic
por: Geoffroy, Guillaume
Publicado: (2025)

Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements
por: Prebet, Enguerrand, et al.
Publicado: (2026)

Deductive Verification of Weak Memory Programs with View-based Protocols (extended version)
por: Şakar, Ömer, et al.
Publicado: (2026)

A Weakest Precondition Calculus for Programs and Linear Temporal Specifications
por: Ernst, Gidon
Publicado: (2026)

A Typed Lambda-Calculus for Establishing Trust in Probabilistic Programs
por: Genco, Francesco A., et al.
Publicado: (2023)

Provably Safe Neural Network Controllers via Differential Dynamic Logic
por: Teuber, Samuel, et al.
Publicado: (2024)

Complete and Terminating Tableau Calculus for Undirected Graph
por: Nishimura, Yuki, et al.
Publicado: (2024)

Structured Abductive-Deductive-Inductive Reasoning for LLMs via Algebraic Invariants
por: Gilda, Sankalp, et al.
Publicado: (2026)

AutoDeduct: A Tool for Automated Deductive Verification of C Code
por: Amilon, Jesper, et al.
Publicado: (2025)

An Algebraic Extension of Intuitionistic Linear Logic: The $L_!^S$-Calculus and Its Categorical Model
por: Díaz-Caro, Alejandro, et al.
Publicado: (2025)

A Cut-free Sequent Calculus for Basic Intuitionistic Dynamic Topological Logic
por: Tabatabai, Amirhossein Akbar, et al.
Publicado: (2025)

Small Decision Trees for MDPs with Deductive Synthesis
por: Andriushchenko, Roman, et al.
Publicado: (2025)

On Zeno-like Behaviors in the Event Calculus with Goal-directed Answer Set Programming
por: Vašíček, Ondřej, et al.
Publicado: (2026)

Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of Probabilistic Programming Languages
por: Barbarossa, Davide, et al.
Publicado: (2025)

The Flower Calculus
por: Donato, Pablo
Publicado: (2024)

Functional Array Programming in an Extended Pi-Calculus
por: Hüttel, Hans, et al.
Publicado: (2024)

Can Large Language Models Autoformalize Kinematics?
por: Kabra, Aditi, et al.
Publicado: (2025)

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

Rings and Boolean Algebras as Algebraic Theories
por: De Faveri, Arturo
Publicado: (2025)

The Tensor-Plus Calculus
por: Chardonnet, Kostia, et al.
Publicado: (2025)

Dynamic Automated Deduction by Contradiction Separation: The Standard Extension Algorithm
por: Xu, Yang, et al.
Publicado: (2025)

Two Cases of Deduction with Non-referring Descriptions
por: Raclavský, Jiří
Publicado: (2024)

Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL
por: Foster, Simon, et al.
Publicado: (2024)

A Rewriting Theory for Quantum Lambda-Calculus
por: Faggian, Claudia, et al.
Publicado: (2024)

A Sequent Calculus For Trace Formula Implication
por: Heidler, Niklas, et al.
Publicado: (2025)

Reasoning Around Paradox with Grounded Deduction
por: Ford, Bryan
Publicado: (2024)

Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT
por: Lommen, Nils, et al.
Publicado: (2024)

Groups and Inverse Semigroups in Lambda Calculus
por: Bucciarelli, Antonio, et al.
Publicado: (2026)