research
∙
06/21/2023
A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL
We present a formalization of several fundamental notions and results fr...
share
research
∙
05/15/2023
Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates
We establish various complexity results for the entailment problem betwe...
research
∙
07/06/2022
Unbiasing and robustifying implied volatility calibration in a cryptocurrency market with large bid-ask spreads and missing quotes
We design a novel calibration procedure that is designed to handle the s...
research
∙
06/19/2022
Two Results on Separation Logic With Theory Reasoning
Two results are presented concerning the entailment problem in Separatio...
research
∙
01/31/2022
A Proof Procedure For Separation Logic With Inductive Definitions and Theory Reasoning
A proof procedure, in the spirit of the sequent calculus, is proposed to...
research
∙
03/22/2021
A Superposition-Based Calculus for Quantum Diagrammatic Reasoning and Beyond
We introduce a class of rooted graphs which allows one to encode various...
research
∙
03/15/2021
Quantum projective measurements and the CHSH inequality in Isabelle/HOL
We present a formalization in Isabelle/HOL of quantum projective measure...
research
∙
12/28/2020
Unifying Decidable Entailments in Separation Logic with Inductive Definitions
The entailment problem φψ in Separation Logic <cit.>, between separated ...
research
∙
07/01/2020
Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Established Systems
We define a class of Separation Logic formulae, whose entailment problem...
research
∙
04/16/2020
Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard
The entailment between separation logic formulae with inductive predicat...
research
∙
06/26/2019
Ilinva: Using Abduction to Generate Loop Invariants
We describe a system to prove properties of programs. The key feature of...
research
∙
07/25/2018
Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL
We formalize in the proof assistant Isabelle essential basic notions and...
research
∙
07/12/2018
A Generic Framework for Implicate Generation Modulo Theories
The clausal logical consequences of a formula are called its implicates....
research
∙
04/10/2018
The Complexity of Prenex Separation Logic with One Selector
We first show that infinite satisfiability can be reduced to finite sati...
research
∙
02/01/2018
On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic
This paper investigates the satisfiability problem for Separation Logic,...
research
∙
06/02/2014
A Superposition Calculus for Abductive Reasoning
We present a modification of the superposition calculus that is meant to...
research
∙
07/25/2011
Instantiation Schemes for Nested Theories
This paper investigates under which conditions instantiation-based proof...
research
∙
07/22/2011