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...
share
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
∙
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
∙
01/12/2018
A Tableaux Calculus for Reducing Proof Size
A tableau calculus is proposed, based on a compressed representation of ...
research
∙
06/02/2014
A Superposition Calculus for Abductive Reasoning
We present a modification of the superposition calculus that is meant to...
research
∙
01/16/2014
Decidability and Undecidability Results for Propositional Schemata
We define a logic of propositional formula schemata adding to the syntax...
research
∙
07/25/2011
Instantiation Schemes for Nested Theories
This paper investigates under which conditions instantiation-based proof...
research
∙
06/14/2011
Generating Schemata of Resolution Proofs
Two distinct algorithms are presented to extract (schemata of) resolutio...
research
∙
02/10/2011
Linear Temporal Logic and Propositional Schemata, Back and Forth (extended version)
This paper relates the well-known Linear Temporal Logic with the logic o...
research
∙
01/24/2010