
A SuperpositionBased Calculus for Quantum Diagrammatic Reasoning and Beyond
We introduce a class of rooted graphs which allows one to encode various...
read it

Quantum projective measurements and the CHSH inequality in Isabelle/HOL
We present a formalization in Isabelle/HOL of quantum projective measure...
read it

Unifying Decidable Entailments in Separation Logic with Inductive Definitions
The entailment problem φψ in Separation Logic <cit.>, between separated ...
read it

Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Established Systems
We define a class of Separation Logic formulae, whose entailment problem...
read it

Entailment Checking in Separation Logic with Inductive Definitions is 2EXPTIME hard
The entailment between separation logic formulae with inductive predicat...
read it

Ilinva: Using Abduction to Generate Loop Invariants
We describe a system to prove properties of programs. The key feature of...
read it

Formalizing the CoxRossRubinstein pricing of European derivatives in Isabelle/HOL
We formalize in the proof assistant Isabelle essential basic notions and...
read it

A Generic Framework for Implicate Generation Modulo Theories
The clausal logical consequences of a formula are called its implicates....
read it

The Complexity of Prenex Separation Logic with One Selector
We first show that infinite satisfiability can be reduced to finite sati...
read it

On the Expressive Completeness of BernaysSchönfinkelRamsey Separation Logic
This paper investigates the satisfiability problem for Separation Logic,...
read it

A Superposition Calculus for Abductive Reasoning
We present a modification of the superposition calculus that is meant to...
read it

Instantiation Schemes for Nested Theories
This paper investigates under which conditions instantiationbased proof...
read it

Solving Linear Constraints in Elementary Abelian pGroups of Symmetries
Symmetries occur naturally in CSP or SAT problems and are not very diffi...
read it
Mnacho Echenim
is this you? claim profile