Author name cluster

Mnacho Echenim

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

7 papers

2 author rows

CSL Conference 2021 Conference Paper

Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment

Mnacho Echenim
Radu Iosif
Nicolas Peltier

We define a class of Separation Logic [Ishtiaq and O'Hearn, 2001; J. C. Reynolds, 2002] formulae, whose entailment problem given formulae ϕ, ψ₁, …, ψ_n, is every model of ϕ a model of some ψ_i? is 2-EXPTIME-complete. The formulae in this class are existentially quantified separating conjunctions involving predicate atoms, interpreted by the least sets of store-heap structures that satisfy a set of inductive rules, which is also part of the input to the entailment problem. Previous work [Iosif et al. , 2013; Jens Katelaan et al. , 2019; Jens Pagel and Florian Zuleger, 2020] consider established sets of rules, meaning that every existentially quantified variable in a rule must eventually be bound to an allocated location, i. e. from the domain of the heap. In particular, this guarantees that each structure has treewidth bounded by the size of the largest rule in the set. In contrast, here we show that establishment, although sufficient for decidability (alongside two other natural conditions), is not necessary, by providing a condition, called equational restrictedness, which applies syntactically to (dis-)equalities. The entailment problem is more general in this case, because equationally restricted rules define richer classes of structures, of unbounded treewidth. In this paper we show that (1) every established set of rules can be converted into an equationally restricted one and (2) the entailment problem is 2-EXPTIME-complete in the latter case, thus matching the complexity of entailments for established sets of rules [Jens Katelaan et al. , 2019; Jens Pagel and Florian Zuleger, 2020].

Details

LPAR Conference 2020 Conference Paper

Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard

Mnacho Echenim
Radu Iosif
Nicolas Peltier

The entailment between separation logic formulæ with inductive predicates, also known as sym- bolic heaps, has been shown to be decidable for a large class of inductive definitions [7]. Recently, a 2-EXPTIME algorithm was proposed [10, 14] and an EXPTIME-hard bound was established in [8]; however no precise lower bound is known. In this paper, we show that deciding entailment between predicate atoms is 2-EXPTIME-hard. The proof is based on a reduction from the membership problem for exponential-space bounded alternating Turing machines [5].

Details

IJCAI Conference 2018 Conference Paper

Prime Implicate Generation in Equational Logic (extended abstract)

Mnacho Echenim
Nicolas Peltier
Sophie Tourret

A procedure is proposed to efficiently generate sets of ground implicates of first-order formulas with equality. It is based on a tuning of the superposition calculus, enriched with rules that add new hypotheses on demand during the proof search. Experimental results are presented, showing that the proposed approach is more efficient than state-of-the-art systems.

PDF Details

JAIR Journal 2017 Journal Article

Prime Implicate Generation in Equational Logic

Mnacho Echenim
Nicolas Peltier
Sophie Tourret

We present an algorithm for the generation of prime implicates in equational logic, that is, of the most general consequences of formulæ containing equations and disequations between first-order terms. This algorithm is defined by a calculus that is proved to be correct and complete. We then focus on the case where the considered clause set is ground, i.e., contains no variables, and devise a specialized tree data structure that is designed to efficiently detect and delete redundant implicates. The corresponding algorithms are presented along with their termination and correctness proofs. Finally, an experimental evaluation of this prime implicate generation method is conducted in the ground case, including a comparison with state-of-the-art propositional and first-order prime implicate generation tools.

PDF Details DOI

IJCAI Conference 2013 Conference Paper

An Approach to Abductive Reasoning in Equational Logic

Mnacho Echenim
Nicolas Peltier
Sophie Tourret

Abduction has been extensively studied in propositional logic because of its many applications in artificial intelligence. However, its intrinsic complexity has been a limitation to the implementation of abductive reasoning tools in more expressive logics. We have devised such a tool in ground flat equational logic, in which literals are equations or disequations between constants. Our tool is based on the computation of prime implicates. It uses a relaxed paramodulation calculus, designed to generate all prime implicates of a formula, together with a carefully defined data structure storing the implicates and able to efficiently detect, and remove, redundancies. In addition to a detailed description of this method, we present an analysis of some experimental results.

PDF Details DOI

I&C Journal 2007 Journal Article

Permutative rewriting and unification

Thierry Boy de la Tour
Mnacho Echenim

Permutative rewriting provides a way of analyzing deduction modulo a theory defined by leaf-permutative equations. Our analysis naturally leads to the definition of the class of unify-stable axiom sets, in order to enforce a simple reduction strategy. We then give a uniform unification algorithm modulo theories E axiomatized this way. We prove that it computes complete sets of unifiers of simply exponential cardinality, and that the E-unification decision problem belongs to NP.

Details DOI

LPAR Conference 2003 Conference Paper

NP-Completeness Results for Deductive Problems on Stratified Terms

Thierry Boy de la Tour
Mnacho Echenim

In [1] Avenhaus and Plaisted proposed the notion of stratified terms, in order to represent concisely the sets of consequences of clauses under leaf permutative theories. These theories contain variable-permuting equations, so that the consequences appear as simple “permuted” variants of each other. Deducing directly with stratified terms can reduce exponentially the search space, but we show that the problems involved (e. g. unifiability) are NP -complete. We use computational group theory to show membership in NP, while NP -hardness is obtained through an interesting problem in group theory.

Details